z3 sat solving

src/main/scala/de/tum/workflows/toz3/InvariantChecker.scala

@@ -34,7 +34,7 @@ object InvariantChecker extends LazyLogging {
 
     val s = ctx.mkSolver(t)
 
-    s.add(toZ3.translate(f, ctx))
+    s.add(Z3.translate(f, ctx))
 
     // Send to z3
     val c = s.check()
@@ -110,7 +110,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 ++= toZ3.printModel(solver.getModel()).lines.map("  " + _).mkString("\n")
+          msg ++= Z3.printModel(solver.getModel()).lines.map("  " + _).mkString("\n")
         } else if (res == Status.UNKNOWN) {
           msg ++= s"Z3 result: $res (${solver.getReasonUnknown()})\n"
         }

src/main/scala/de/tum/workflows/toz3/toz3.scala → src/main/scala/de/tum/workflows/toz3/Z3.scala

@@ -9,7 +9,7 @@ import java.util.concurrent.atomic.AtomicInteger
 import java.util.HashMap
 import com.typesafe.scalalogging.LazyLogging
 
-object toZ3 extends LazyLogging {
+object Z3 extends LazyLogging {
 
   type VarCtx = Map[Var, (Option[Int], Expr, Sort)]
 
@@ -269,8 +269,14 @@ object toZ3 extends LazyLogging {
     }
 
     sb ++= "Evaluations:\n"
-    val sorted = model.getFuncDecls().sortBy(_.getName.toString())
-    for (f <- sorted) {
+    val sortedConsts = model.getConstDecls().sortBy(_.getName.toString())
+    for (f <- sortedConsts) {
+      val interp = model.getConstInterp(f)
+      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)

src/main/scala/de/tum/workflows/toz3/Z3QFree.scala

+package de.tum.workflows.toz3;
+
+import de.tum.workflows.foltl.FOLTL
+import de.tum.workflows.foltl.FOLTL._
+import de.tum.workflows.foltl.FormulaFunctions._
+
+import com.microsoft.z3._;
+import java.util.concurrent.atomic.AtomicInteger
+import java.util.HashMap
+import com.typesafe.scalalogging.LazyLogging
+
+object Z3QFree extends LazyLogging {
+
+  def toZ3(ctx: Context, f: Formula): 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) => {
+        logger.error("Trying to encode function symbols into QFree SAT")
+        ctx.mkFalse()
+      }
+
+      case op:TemporalFormula => {
+        logger.error("Trying to encode temporal operators into QFree SAT")
+        ctx.mkFalse()
+      }
+
+      case q:FOLTL.Quantifier => {
+        logger.error("Trying to encode quantifiers into QFree SAT")
+        ctx.mkFalse()
+      }
+
+      case And(f1, f2) => {
+        val e1 = toZ3(ctx, f1)
+        val e2 = toZ3(ctx, f2)
+        ctx.mkAnd(e1, e2)
+      }
+
+      case Eq(f1, f2) => {
+        val e1 = toZ3(ctx, f1)
+        val e2 = toZ3(ctx, f2)
+        ctx.mkEq(e1, e2)
+      }
+
+      case Or(f1, f2) => {
+        val e1 = toZ3(ctx, f1)
+        val e2 = toZ3(ctx, f2)
+        ctx.mkOr(e1, e2)
+      }
+
+      case Implies(f1, f2) => {
+        val e1 = toZ3(ctx, f1)
+        val e2 = toZ3(ctx, f2)
+        ctx.mkImplies(e1, e2)
+      }
+
+      case Neg(f1) => {
+        val e = toZ3(ctx, f1)
+        ctx.mkNot(e)
+      }
+
+      case True => {
+        ctx.mkTrue()
+      }
+      case False => {
+        ctx.mkFalse()
+      }
+      
+      case Var(x,t) => {
+        ctx.mkBoolConst(x)
+      }
+    }
+  }
+
+  def translate(f: Formula, ctx: Context) = {
+    //    logger.info(s"Using formula:\n$f")
+    val expr = toZ3(ctx, f)
+    //    logger.info(s"Built Z3 expression:\n$expr")
+    expr
+  }
+}

src/test/scala/Test.scala

@@ -3,7 +3,7 @@ import de.tum.workflows.foltl.FOLTL
 import com.microsoft.z3.Context
 import java.util.HashMap
 import com.microsoft.z3.Status
-import de.tum.workflows.toz3.toZ3
+import de.tum.workflows.toz3.Z3
 import org.omg.CORBA.TIMEOUT
 
 import de.tum.workflows.Implicits._

src/test/scala/de/tum/workflows/ltl/tests/Z3QFreeTest.scala

+package de.tum.workflows.ltl.tests
+
+import org.scalatest.BeforeAndAfterEach
+import com.typesafe.scalalogging.LazyLogging
+import org.scalatest.Matchers._
+import org.scalatest.Inspectors._
+import com.microsoft.z3.Solver
+import java.util.HashMap
+import org.scalatest.FlatSpec
+import com.microsoft.z3.Context
+import de.tum.workflows.Implicits._
+import de.tum.workflows.foltl.FOLTL._
+import de.tum.workflows.toz3.Z3QFree
+import com.microsoft.z3.Status
+import de.tum.workflows.toz3.Z3
+
+  class Z3QFreeTest extends FlatSpec with LazyLogging with BeforeAndAfterEach {
+
+  var ctx: Context = null
+  var s: Solver = null
+
+  val TIMEOUT = 30000 // in milliseconds
+
+  override def beforeEach() = {
+    val cfg = new HashMap[String, String]()
+    cfg.put("timeout", TIMEOUT.toString())
+
+    val ctx = new Context(cfg)
+
+    val qe = ctx.mkTactic("qe")
+    val default = ctx.mkTactic("smt")
+    val t = ctx.andThen(qe, default)
+
+    val s = ctx.mkSolver(t)
+
+    this.ctx = ctx
+    this.s = s
+  }
+  
+  def check(s: Solver, res: Status) = {
+    val c = s.check()
+    if (c == Status.UNKNOWN) {
+      println(s"Z3 status unknown: ${s.getReasonUnknown()}")
+    }
+    
+    c should be (res)
+    if (res == Status.SATISFIABLE) {
+      println(s"Z3 model:\n${Z3.printModel(s.getModel())}")
+    }
+  }
+  
+  "Z3QFree" should "check small things SAT" in {
+    val easyForm = And("a", "b")
+
+    s.add(Z3QFree.translate(easyForm, ctx))
+    check(s, Status.SATISFIABLE)
+  }
+  
+  it should "check small things UNSAT" in {
+    val easyForm = And("a", Neg("a"))
+
+    s.add(Z3QFree.translate(easyForm, ctx))
+    check(s, Status.UNSATISFIABLE)
+  }
+  
+  it should "check longer things SAT" in {
+    val easyForm = Or(And("a", "b"), And("c",Or("d","e")))
+
+    s.add(Z3QFree.translate(easyForm, ctx))
+    check(s, Status.SATISFIABLE)
+  }
+}

src/test/scala/de/tum/workflows/ltl/tests/Z3Test.scala

@@ -72,7 +72,7 @@ class Z3Test extends FlatSpec with LazyLogging with BeforeAndAfterEach {
       a -> (None, ctx.mkConst(a.name, s), s)
     }
 
-    s.add(toZ3.translate(quantfree, ctx, varctx))
+    s.add(Z3.translate(quantfree, ctx, varctx))
     s
   }
 
@@ -94,14 +94,14 @@ class Z3Test extends FlatSpec with LazyLogging with BeforeAndAfterEach {
   "Z3" should "check Globally" in {
     val easyForm = Globally(And(Fun("p", List()), Globally(Fun("p", List()))))
 
-    s.add(toZ3.translate(easyForm, ctx))
+    s.add(Z3.translate(easyForm, ctx))
     check(s, Status.SATISFIABLE)
   }
 
   it should "check small things" in {
     val easyForm = Forall(List("x", "s"), Neg(Fun("R", List("x", "s"))))
 
-    s.add(toZ3.translate(easyForm, ctx))
+    s.add(Z3.translate(easyForm, ctx))
     check(s, Status.SATISFIABLE)
   }
 
@@ -110,7 +110,7 @@ class Z3Test extends FlatSpec with LazyLogging with BeforeAndAfterEach {
     val f = Globally(Forall(List("x"), Fun("p", "x")))
     println(f)
 
-    s.add(toZ3.translate(f, ctx))
+    s.add(Z3.translate(f, ctx))
     check(s, Status.SATISFIABLE)
   }
 
@@ -119,7 +119,7 @@ class Z3Test extends FlatSpec with LazyLogging with BeforeAndAfterEach {
     val f = Globally(Forall(List("x"), And(Fun("p", "x"), Next(Neg(Forall("y", Globally(Next(Fun("p", "y")))))))))
     println(f)
 
-    s.add(toZ3.translate(f, ctx))
+    s.add(Z3.translate(f, ctx))
     check(s, Status.UNSATISFIABLE)
   }
 
@@ -128,7 +128,7 @@ class Z3Test extends FlatSpec with LazyLogging with BeforeAndAfterEach {
     val f = Until(Fun("p", List()), Forall("y", Fun("q", "y")))
     println(f)
 
-    s.add(toZ3.translate(f, ctx))
+    s.add(Z3.translate(f, ctx))
     check(s, Status.SATISFIABLE)
   }
 
@@ -138,7 +138,7 @@ class Z3Test extends FlatSpec with LazyLogging with BeforeAndAfterEach {
       Until(Fun("p", "x"), Next(Forall("y", Finally(Next(Fun("q", "y")))))))))
     println(f)
 
-    s.add(toZ3.translate(f, ctx))
+    s.add(Z3.translate(f, ctx))
     check(s, Status.SATISFIABLE) // Z3 does not finish
   }
 
@@ -151,7 +151,7 @@ class Z3Test extends FlatSpec with LazyLogging with BeforeAndAfterEach {
       Next(Globally(Neg(Fun("p", "x")))))))
     println(f)
 
-    s.add(toZ3.translate(f, ctx))
+    s.add(Z3.translate(f, ctx))
     // check(s,c,Status.SATISFIABLE) // only on infinite domains
     check(s, Status.UNSATISFIABLE) // only on finite domains
   }
@@ -167,7 +167,7 @@ class Z3Test extends FlatSpec with LazyLogging with BeforeAndAfterEach {
           Globally(Neg(Fun("p", "x")))))))))))
     println(f)
 
-    s.add(toZ3.translate(f, ctx))
+    s.add(Z3.translate(f, ctx))
     // check(s,c,Status.SATISFIABLE) // only on infinite domains
     check(s, Status.UNSATISFIABLE) // only on finite domains
   }
@@ -181,7 +181,7 @@ class Z3Test extends FlatSpec with LazyLogging with BeforeAndAfterEach {
         And(Neg(Fun("p", "x")), Fun("p", "y")))))))
     println(f)
 
-    s.add(toZ3.translate(f, ctx))
+    s.add(Z3.translate(f, ctx))
     // check(s,c,Status.SATISFIABLE) // only on infinite domains
     check(s, Status.UNSATISFIABLE) // only on finite domains
     // println(s.getModel())