Commit b410e6bf authored by Christian Müller's avatar Christian Müller
Browse files

castdown

parent cd075ba9
import com.microsoft.z3.Context;
import com.microsoft.z3.Quantifier;
import com.microsoft.z3.Sort;
import com.microsoft.z3.Symbol;
import java.util.HashMap;
public class BrokenDowncastMWE {
public static void main(String[] args) {
var cfg = new HashMap<String, String>();
var ctx = new Context(cfg);
var simp = ctx.mkTactic("tseitin-cnf");
var goal = ctx.mkGoal(false, false, false);
var names = new Symbol[1];
names[0] = ctx.mkSymbol("x");
var sorts = new Sort[1];
sorts[0] = ctx.mkUninterpretedSort("T");
var fundecl = ctx.mkFuncDecl("fun", sorts, ctx.getBoolSort());
var boundvar = ctx.mkBound(0, sorts[0]);
var application = fundecl.apply(boundvar);
var expr = ctx.mkForall(sorts, names, application, 0, null, null, null, null);
goal.add(expr);
var ar = simp.apply(goal);
var sub = ar.getSubgoals();
var resultexpr = sub[0].AsBoolExpr();
System.out.println(expr);
System.out.println(expr.isQuantifier());
System.out.println(expr.getClass().getName());
System.out.println(resultexpr);
System.out.println(resultexpr.isQuantifier());
System.out.println(resultexpr.getClass().getName());
((Quantifier) resultexpr).getBody();
}
}
......@@ -98,7 +98,7 @@ object Utils extends LazyLogging {
s"""Name: $name
Description: $desc
Invariant:
${inv.pretty().lines.map(s => " " + s).mkString("\n")}
${inv.pretty.lines.map(s => " " + s).mkString("\n")}
Model: $model
Result: ${if (!res) "not " else ""}inductive
WF size: $wfsize
......
......@@ -6,7 +6,7 @@ import de.tum.workflows.foltl.FOLTL._
import de.tum.workflows.blocks.Workflow._
import com.typesafe.scalalogging.LazyLogging
object WorkflowParser extends RegexParsers with LazyLogging {
object WorkflowParser extends RegexParsers with PackratParsers with LazyLogging {
def addChoicePredicates(blocks: List[Block]) = {
var i = -1; // start at 0
......@@ -125,17 +125,22 @@ object WorkflowParser extends RegexParsers with LazyLogging {
def ff = "False" ^^^ False
def AND = "(" ~> (repsep(TERM, "∧") | repsep(TERM, "&&")) <~ ")" ^^ (ts => And.make(ts))
def OR = "(" ~> (repsep(TERM, "∨") | repsep(TERM, "||")) <~ ")" ^^ (ts => Or.make(ts))
def NEG = ("¬" | "!") ~ SIMPLETERM ^^ { case _ ~ t => Neg(t) }
def NEG = ("¬" | "!") ~ SIMPLETERM ^^ { case _ ~ t => Neg(t) }
def IMPLIES = "(" ~> TERM ~ "⟹" ~ (TERM <~ ")") ^^ { case t1 ~ _ ~ t2 => Implies(t1, t2) }
// temporals
def GLOBALLY = ("G" | "☐") ~> TERM ^^ (t => Globally(t))
def FINALLY = ("F" | "♢") ~> TERM ^^ (t => Finally(t))
def TUPLE = "(" ~> repsep(TYPEDVAR, ",") <~ ")"
def FUN = VAR ~ TUPLE ^^ { case f ~ tup => Fun(f.name, tup) }
def SIMPLETERM = (tt | ff | FUN )
def TERM:Parser[Formula] = (SIMPLETERM | GLOBALLY | FINALLY | AND | OR | NEG )
def EXISTS = "∃" ~> (repsep(TYPEDVAR, ",") <~ ("."?)) ~ TERM ^^ { case vs ~ t => Exists(vs, t) }
def FORALL = "∀" ~> (repsep(TYPEDVAR, ",") <~ ("."?)) ~ TERM ^^ { case vs ~ t => Forall(vs, t) }
def QUANTIFIER = EXISTS | FORALL
def SIMPLETERM = (tt | ff | FUN)
lazy val TERM:PackratParser[Formula] = (AND | OR | IMPLIES | NEG | SIMPLETERM | GLOBALLY | FINALLY | QUANTIFIER)
def ADD = TERM ~ ("→" | "->") ~ VAR ~ "+=" ~ TUPLE ^^ { case guard ~ _ ~ fun ~ _ ~ tup => Add(guard, fun.name, tup) }
def REM = TERM ~ ("→" | "->") ~ VAR ~ "-=" ~ TUPLE ^^ { case guard ~ _ ~ fun ~ _ ~ tup => Remove(guard, fun.name, tup) }
......
......@@ -35,9 +35,15 @@ object FOLTL {
case _ => this.toString()
}
// single arrow is for maps
def -->(f2: Formula) = Implies(this, f2)
def (f2: Formula) = Implies(this, f2)
def land(f2: Formula) = And(this, f2)
def /\(f2: Formula) = And(this, f2)
def (f2: Formula) = And(this, f2)
def lor(f2: Formula) = And(this, f2)
def (f2: Formula) = Or(this, f2)
def \/(f2: Formula) = Or(this, f2)
// TODO: better line breaking
lazy val pretty: String = {
......@@ -276,7 +282,14 @@ object FOLTL {
val opname = "→"
val make = Implies.apply
}
object Implies {
def make(terms: List[Formula]) = {
BinOp.makeL(Implies.apply, terms, True)
}
def make(terms: Formula*) = {
BinOp.makeL(Implies.apply, terms, True)
}
}
case class Neg(t: Formula) extends UnOp {
val make = Neg.apply
val opname = "¬"
......
......@@ -178,7 +178,7 @@ object InvariantChecker extends LazyLogging {
msg ++= s"Possibly unsafe: Block may not uphold invariant:\n\n${e.label}\n\n"
if (res == Status.SATISFIABLE) {
msg ++= "Satisfying model:\n"
msg ++= Z3LTL.printModel(solver.getModel()).lines.map(" " + _).mkString("\n")
msg ++= Z3FOEncoding.printModel(solver.getModel()).lines.map(" " + _).mkString("\n")
} else if (res == Status.UNKNOWN) {
msg ++= s"Z3 result: $res (${solver.getReasonUnknown()})\n"
}
......
package de.tum.workflows.toz3
import com.microsoft.z3.{Expr, Sort}
import com.typesafe.scalalogging.LazyLogging
import java.util
import de.tum.workflows.foltl.{FOLTL, FOTransformers, FormulaFunctions}
import de.tum.workflows.foltl.FOLTL._
import com.microsoft.z3._
import de.tum.workflows.Utils
import de.tum.workflows.toz3.Z3QFree.{TIMEOUT, logger}
object Z3BSFO extends LazyLogging {
......@@ -18,7 +15,7 @@ object Z3BSFO extends LazyLogging {
val (time, res) = Utils.time {
// Set up Z3
val cfg = new util.HashMap[String, String]()
cfg.put("timeout", TIMEOUT.toString())
cfg.put("timeout", Z3FOEncoding.TIMEOUT.toString())
val ctx = new Context(cfg)
val params = ctx.mkParams()
params.add("mbqi", true)
......@@ -35,17 +32,17 @@ object Z3BSFO extends LazyLogging {
}
// neg is now in E*A*, so can be solved by bounded instantiation
s.add(translate(neg, ctx))
s.add(Z3FOEncoding.translate(neg, ctx))
// Send to z3
val c = s.check()
if (c == Status.UNKNOWN) {
logger.warn(s"Z3-BSFO: Status unknown - ${s.getReasonUnknown()}")
}
// if (c == Status.SATISFIABLE) {
// logger.info(s"Z3 status satisfiable")
// logger.info(s"${s.getModel()}")
// }
// if (c == Status.SATISFIABLE) {
// logger.info(s"Z3 status satisfiable")
// logger.info(s"${s.getModel()}")
// }
(c, s)
}
// Logging only calls that take longer than a second
......@@ -55,238 +52,62 @@ object Z3BSFO extends LazyLogging {
res
}
type VarCtx = Map[Var, (Option[Int], Expr, Sort)]
var counter = 0
// TODO: how to not make this static?
val fun_ctx = new util.HashMap[String, FuncDecl]()
def buildVarCtx(ctx: Context, var_ctx: VarCtx, vars: List[Var]): VarCtx = {
val indices = (vars.size - 1) to 0 by -1
val newexprs = (for ((v, i) <- vars.zip(indices)) yield {
// count = count - 1;
val sort = if (v.typ.equals("Int")) {
ctx.getIntSort()
} else if (v.typ.equals("Bool")) {
ctx.getBoolSort()
} else {
ctx.mkUninterpretedSort(v.typ) // TODO: finite domain? sort size?
}
v -> (Some(i), ctx.mkBound(i, sort), sort)
}) toMap
// if the index is defined, increment, otherwise use the expr (which is a constant f.e.)
val oldvars = (for ((v, (i, e, s)) <- var_ctx) yield {
if (i.isDefined) {
val newi = i.get + vars.size
val newbound = ctx.mkBound(newi, s)
v -> (Some(newi), newbound, s)
} else {
v -> (i, e, s)
}
})
newexprs ++ oldvars
}
def toBoolZ3(ctx: Context, f: Formula, var_ctx: VarCtx): BoolExpr = {
// texpr is an expression e with the form given by the following grammar:
// e ::= 0 | t | succ(e)
// tvar is Some(t) if e contains t or None otherwise
f match {
case Fun(name, ind, params) => {
val pi = if (ind.isDefined) "_" + ind.get else ""
val indexedname = name + pi
var fdecl = fun_ctx.get(indexedname)
if (fdecl == null) {
val pi = if (ind.isDefined) "_" + ind.get else ""
val sorts = params.map(x => var_ctx(x)._3)
fdecl = ctx.mkFuncDecl(indexedname, sorts.toArray, ctx.getBoolSort())
fun_ctx.put(indexedname, fdecl)
}
// all variables should be quantified, so they should be part of var_ctx
// TODO: support constants/free variables
val all_args = params.map(x => var_ctx(x)._2)
fdecl.apply(all_args: _*).asInstanceOf[BoolExpr]
}
case Exists(vars, f1) => {
val names: Array[Symbol] = vars.map(v => ctx.mkSymbol(v.name)).toArray
val newctx = buildVarCtx(ctx, var_ctx, vars)
val sorts = vars.map(newctx(_)._3).toArray
val e1 = toBoolZ3(ctx, f1, newctx)
ctx.mkExists(sorts, names, e1, 0, null, null, null, null)
}
case Forall(vars, f1) => {
val names: Array[Symbol] = vars.map(v => ctx.mkSymbol(v.name)).toArray
val newctx = buildVarCtx(ctx, var_ctx, vars)
val sorts = vars.map(newctx(_)._3).toArray
val e1 = toBoolZ3(ctx, f1, newctx)
ctx.mkForall(sorts, names, e1, 0, null, null, null, null)
}
case And(f1, f2) => {
val e1 = toBoolZ3(ctx, f1, var_ctx)
val e2 = toBoolZ3(ctx, f2, var_ctx)
ctx.mkAnd(e1, e2)
}
case Eq(f1, f2) => {
val e1 = toSortedZ3(ctx, f1, var_ctx)
val e2 = toSortedZ3(ctx, f2, var_ctx)
ctx.mkEq(e1, e2)
}
case Or(f1, f2) => {
val e1 = toBoolZ3(ctx, f1, var_ctx)
val e2 = toBoolZ3(ctx, f2, var_ctx)
ctx.mkOr(e1, e2)
}
case Implies(f1, f2) => {
val e1 = toBoolZ3(ctx, f1, var_ctx)
val e2 = toBoolZ3(ctx, f2, var_ctx)
ctx.mkImplies(e1, e2)
}
case Neg(f1) => {
val e = toBoolZ3(ctx, f1, var_ctx)
ctx.mkNot(e)
}
case True => {
ctx.mkTrue()
}
case False => {
ctx.mkFalse()
}
}
def simplifyBS(f: Formula) = {
val cfg = new util.HashMap[String, String]()
cfg.put("timeout", Z3FOEncoding.TIMEOUT.toString())
val ctx = new Context(cfg)
val simp = ctx.mkTactic("ctx-solver-simplify")
// val simp = ctx.mkTactic("simplify")
val params = ctx.mkParams()
// mkGoal (produce models, produce unsat cores, produce proofs)
val goal = ctx.mkGoal(false, false, false)
val z3expr = Z3FOEncoding.translate(f, ctx)
goal.add(z3expr)
val ar = simp.apply(goal)
val sub = ar.getSubgoals()
val mapped = if (sub.isEmpty) {
True
} else if (sub.size > 1) {
logger.error("Simplification Error: Returned several goals")
False
} else {
val form = sub.head.AsBoolExpr()
Z3FOEncoding.mapback(form)
// Z3FOEncoding.mapback(z3expr)
}
mapped
}
def toSortedZ3(ctx: Context, f: Formula, var_ctx: VarCtx): Expr = {
f match {
case v:Var => {
var_ctx(v)._2
}
case _ => {
toBoolZ3(ctx, f, var_ctx)
}
}
}
def translate(f: Formula, ctx: Context) = {
// logger.info(s"Using formula:\n$f")
if (f.freeVars.nonEmpty) {
logger.error(s"Cannot check - formula contains free variables ${f.freeVars}")
}
fun_ctx.clear()
val expr = toBoolZ3(ctx, f, Map())
// logger.info(s"Built Z3 expression:\n$expr")
expr
}
def translate(f: Formula, ctx: Context, varctx: VarCtx) = {
// logger.info(s"Using formula:\n${f.pretty()}")
if (f.freeVars.nonEmpty) {
logger.error(s"Cannot check - formula contains free variables ${f.freeVars}")
}
fun_ctx.clear()
val expr = toBoolZ3(ctx, f, varctx)
// logger.info(s"Built Z3 expression:\n$expr")
expr
def toCNF(f: Formula) = {
val cfg = new util.HashMap[String, String]()
cfg.put("timeout", Z3FOEncoding.TIMEOUT.toString())
val ctx = new Context(cfg)
val simp = ctx.mkTactic("tseitin-cnf")
// val simp = ctx.mkTactic("simplify")
val params = ctx.mkParams()
// mkGoal (produce models, produce unsat cores, produce proofs)
val goal = ctx.mkGoal(false, false, false)
val z3expr = Z3FOEncoding.translate(f, ctx)
goal.add(z3expr)
val ar = simp.apply(goal)
val sub = ar.getSubgoals()
val mapped = if (sub.isEmpty) {
True
} else if (sub.size > 1) {
logger.error("Z3BSFO-CNF: Returned several goals")
False
} else {
val form = sub.head.AsBoolExpr()
Z3FOEncoding.mapback(form)
// Z3FOEncoding.mapback(z3expr)
}
//
// def printModel(model: Model) = {
//
// val sb = new StringBuilder()
//
// // val consts = model.getConstDecls()
// //
// // val vals = consts.map(_.apply())
// // val typedvals = vals.groupBy(_.getSort)
// //
// // sb ++= "Universe:\n"
// // for ((k, v) <- typedvals) {
// // sb ++= s"Type $k: ${v.mkString(",")}\n"
// // }
//
// sb ++= "Relations:\n"
// val sortedConsts = model.getConstDecls().sortBy(_.getName.toString())
//
// val (l1, l2) = sortedConsts.partition(s => {
// s.getName.toString() match {
// case FunFromVar(_) => true
// case _ => false
// }
// })
//
// val funs = l1.map(s => {
// val interp = model.getConstInterp(s)
// (FunFromVar.unapply(s.getName.toString).get, interp.toString)
// }) toList
//
// val grouped = funs.groupBy(f => (f._1.name, f._1.ind))
//
// // sort by name, path
// val entries = grouped.iterator.toList.sortBy(_._1)
// for (g <- entries) {
// sb ++= g._1._1 + "(" + g._1._2 + "):\n"// name
//
// // sort by value, variables
// val tuples = g._2 sortBy(e => (e._2, e._1.params.mkString(",") ))
// for ((fun, v) <- tuples) {
// sb ++= fun.params.mkString("(",",",")") + " = " + v + "\n"
// }
// sb ++= "\n"
// }
//
// sb ++= "\nNon-Relations:\n"
//
// // Rest of the consts
// for (f <- l2) {
// val interp = model.getConstInterp(f)
//
// val name = f.getName.toString match {
// case FunFromVar(fun) => fun
// case _ => f.getName.toString
// }
//
// sb ++= f.getName + " = " + interp.toString() + "\n"
// }
//
// val sortedFuns = model.getFuncDecls().sortBy(_.getName.toString())
// for (f <- sortedFuns) {
// sb ++= f.getName + f.getDomain.mkString("(",", ",")") + "\n"
//
// val interp = model.getFuncInterp(f)
// val entries = interp.getEntries
// for (e <- entries) {
// val args = for (arg <- e.getArgs.toList) yield {
// arg.getSort + " " + arg
// }
// sb ++= f.getName + args.mkString("(", ", ", ")") + " = " + e.getValue() + "\n"
// }
//
// val emptyargs = List.fill(f.getArity)("_")
// sb ++= f.getName + emptyargs.mkString("(", ", ", ")") + " = " + interp.getElse() + "\n\n"
// }
// sb.toString()
// }
// }
mapped
}
}
package de.tum.workflows.toz3
import java.util
import com.microsoft.z3.{BoolExpr, Context, Expr, FuncDecl, Model, Sort, Symbol}
import com.typesafe.scalalogging.LazyLogging
import de.tum.workflows.foltl.FOLTL._
object Z3FOEncoding extends LazyLogging {
val TIMEOUT = 60000 // in milliseconds
def translate(f: Formula, ctx: Context) = {
// logger.info(s"Using formula:\n$f")
// TODO: allow constants
if (f.freeVars.nonEmpty) {
logger.error(s"Cannot check - formula contains free variables ${f.freeVars}")
}
fun_ctx.clear()
val expr = toBoolZ3(ctx, f, Map())
// logger.info(s"Built Z3 expression:\n$expr")
expr
}
def translate(f: Formula, ctx: Context, varctx: VarCtx) = {
// logger.info(s"Using formula:\n${f.pretty()}")
if (f.freeVars.nonEmpty) {
logger.error(s"Cannot check - formula contains free variables ${f.freeVars}")
}
fun_ctx.clear()
val expr = toBoolZ3(ctx, f, varctx)
// logger.info(s"Built Z3 expression:\n$expr")
expr
}
def toBoolZ3(ctx: Context, f: Formula, var_ctx: VarCtx): BoolExpr = {
f match {
case Fun(name, ind, params) => {
val pi = if (ind.isDefined) "_" + ind.get else ""
val indexedname = name + pi
var fdecl = fun_ctx.get(indexedname)
if (fdecl == null) {
val pi = if (ind.isDefined) "_" + ind.get else ""
val sorts = params.map(x => var_ctx(x)._3)
fdecl = ctx.mkFuncDecl(indexedname, sorts.toArray, ctx.getBoolSort())
fun_ctx.put(indexedname, fdecl)
}
// all variables should be quantified, so they should be part of var_ctx
// TODO: support constants/free variables
val all_args = params.map(x => var_ctx(x)._2)
fdecl.apply(all_args: _*).asInstanceOf[BoolExpr]
}
case Exists(vars, f1) => {
val names: Array[Symbol] = vars.map(v => ctx.mkSymbol(v.name)).toArray
val newctx = buildVarCtx(ctx, var_ctx, vars)
val sorts = vars.map(newctx(_)._3).toArray
val e1 = toBoolZ3(ctx, f1, newctx)
ctx.mkExists(sorts, names, e1, 0, null, null, null, null)
}
case Forall(vars, f1) => {
val names: Array[Symbol] = vars.map(v => ctx.mkSymbol(v.name)).toArray
val newctx = buildVarCtx(ctx, var_ctx, vars)
val sorts = vars.map(newctx(_)._3).toArray
val e1 = toBoolZ3(ctx, f1, newctx)
ctx.mkForall(sorts, names, e1, 0, null, null, null, null)
}
case And(f1, f2) => {
val e1 = toBoolZ3(ctx, f1, var_ctx)
val e2 = toBoolZ3(ctx, f2, var_ctx)
ctx.mkAnd(e1, e2)
}
case Eq(f1, f2) => {
val e1 = toSortedZ3(ctx, f1, var_ctx)
val e2 = toSortedZ3(ctx, f2, var_ctx)
ctx.mkEq(e1, e2)
}
case Or(f1, f2) => {
val e1 = toBoolZ3(ctx, f1, var_ctx)
val e2 = toBoolZ3(ctx, f2, var_ctx)
ctx.mkOr(e1, e2)
}
case Implies(f1, f2) => {
val e1 = toBoolZ3(ctx, f1, var_ctx)
val e2 = toBoolZ3(ctx, f2, var_ctx)
ctx.mkImplies(e1, e2)
}
case Neg(f1) => {
val e = toBoolZ3(ctx, f1, var_ctx)
ctx.mkNot(e)
}