New tests to test the new API with new unrolling

src/main/scala/leon/solvers/z3/FairZ3Solver.scala

@@ -833,40 +833,43 @@ class FairZ3Solver(context : LeonContext) extends Solver(context) with AbstractZ
 
               if(Settings.pruneBranches) {
                 for(ex <- blockingSet) ex match {
-                  case Not(Variable(b)) => {
+                  case Not(Variable(b)) =>
                     solver.push
                     solver.assertCnstr(toZ3Formula(Variable(b)).get)
                     solver.check match {
-                      case Some(false) => {
+                      case Some(false) =>
                         //println("We had ~" + b + " in the blocking set. We now know it should stay there forever.")
                         solver.pop(1)
                         solver.assertCnstr(toZ3Formula(Not(Variable(b))).get)
                         fixedForEver = fixedForEver + ex
-                      }
-                      case _ => solver.pop(1)
+
+                      case _ =>
+                        solver.pop(1)
                     }
-                  }
-                  case Variable(b) => {
+
+                  case Variable(b) =>
                     solver.push
                     solver.assertCnstr(toZ3Formula(Not(Variable(b))).get)
                     solver.check match {
-                      case Some(false) => {
+                      case Some(false) =>
                         //println("We had " + b + " in the blocking set. We now know it should stay there forever.")
                         solver.pop(1)
                         solver.assertCnstr(toZ3Formula(Variable(b)).get)
                         fixedForEver = fixedForEver + ex
-                      }
-                      case _ => solver.pop(1)
+
+                      case _ =>
+                        solver.pop(1)
                     }
-                  }
-                  case _ => scala.sys.error("Should not have happened.")
+
+                  case _ =>
+                    scala.sys.error("Should not have happened.")
                 }
+
                 if(fixedForEver.size > 0) {
                   reporter.info("- Pruned out " + fixedForEver.size + " branches.")
                 }
               }
 
-
               blockingSet = blockingSet -- toRelease
 
               val toReleaseAsPairs : Set[(Identifier,Boolean)] = (toRelease -- fixedForEver).map(b => b match {

src/test/scala/leon/test/solvers/z3/BugWithEmptySetNewAPI.scala

+package leon.test.solvers.z3
+
+import leon.LeonContext
+import leon.SilentReporter
+
+import leon.purescala.Common._
+import leon.purescala.Definitions._
+import leon.purescala.Trees._
+import leon.purescala.TreeOps._
+import leon.purescala.TypeTrees._
+
+import leon.solvers.Solver
+import leon.solvers.z3.{AbstractZ3Solver, UninterpretedZ3Solver}
+
+import org.scalatest.FunSuite
+
+class BugWithEmptySetNewAPI extends FunSuite {
+  private val emptyProgram = Program(FreshIdentifier("empty"), ObjectDef(FreshIdentifier("empty"), Nil, Nil))
+
+  test("No distinction between Set() and Set.empty") {
+    val tInt = Int32Type
+    val tIntSet = SetType(Int32Type)
+
+    val e1 = EmptySet(tInt).setType(tIntSet)
+    assert(e1.getType === tIntSet)
+
+    val e2 = FiniteSet(Nil).setType(tIntSet)
+    assert(e2.getType === tIntSet)
+
+    val s0 = FiniteSet(Seq(IntLiteral(0))).setType(tIntSet)
+
+    val f1 = Equals(e1, e2)
+
+    val silentContext = LeonContext(reporter = new SilentReporter)
+    val solver : AbstractZ3Solver = new UninterpretedZ3Solver(silentContext)
+    solver.setProgram(emptyProgram)
+    solver.restartZ3
+
+
+    val subSolver = solver.getNewSolver
+
+    subSolver.push()
+    subSolver.assertCnstr(Not(f1))
+
+
+    assert(subSolver.check === Some(false),
+           "Z3 should prove the equivalence between Ø and {}.")
+
+    subSolver.pop(1)
+
+    val f2 = Equals(e1, SetDifference(e1, s0))
+
+    subSolver.push()
+    subSolver.assertCnstr(Not(f2))
+
+    assert(subSolver.check === Some(false),
+           """Z3 should prove Ø = Ø \ {0}""")
+
+
+    subSolver.pop(1)
+
+    val f3 = Equals(e2, SetDifference(e2, s0))
+
+    subSolver.push()
+    subSolver.assertCnstr(Not(f3))
+
+    assert(subSolver.check === Some(false),
+           """Z3 should prove {} = {} \ {0}""")
+  } 
+}

src/test/scala/leon/test/solvers/z3/FairZ3SolverTestsNewAPI.scala

+package leon.test.solvers.z3
+
+import leon.LeonContext
+import leon.SilentReporter
+
+import leon.purescala.Common._
+import leon.purescala.Definitions._
+import leon.purescala.Trees._
+import leon.purescala.TreeOps._
+import leon.purescala.TypeTrees._
+
+import leon.solvers.Solver
+import leon.solvers.z3.FairZ3Solver
+
+import org.scalatest.FunSuite
+
+class FairZ3SolverTestsNewAPI extends FunSuite {
+  private var testCounter : Int = 0
+  private def solverCheck(solver : Solver, expr : Expr, expected : Option[Boolean], msg : String) = {
+    testCounter += 1
+
+    test("Solver test #" + testCounter) {
+      val sub = solver.getNewSolver
+
+      sub.assertCnstr(Not(expr))
+
+      assert(sub.check === expected.map(!_), msg)
+    }
+  }
+
+  private def assertValid(solver : Solver, expr : Expr) = solverCheck(
+    solver, expr, Some(true),
+    "Solver should prove the formula " + expr + " valid."
+  )
+
+  private def assertInvalid(solver : Solver, expr : Expr) = solverCheck(
+    solver, expr, Some(false),
+    "Solver should prove the formula " + expr + " invalid."
+  )
+
+  private def assertUnknown(solver : Solver, expr : Expr) = solverCheck(
+    solver, expr, None,
+    "Solver should not be able to decide the formula " + expr + "."
+  )
+
+  private val silentContext = LeonContext(reporter = new SilentReporter)
+
+  // def f(fx : Int) : Int = fx + 1
+  private val fx   : Identifier = FreshIdentifier("x").setType(Int32Type)
+  private val fDef : FunDef = new FunDef(FreshIdentifier("f"), Int32Type, VarDecl(fx, Int32Type) :: Nil)
+  fDef.body = Some(Plus(Variable(fx), IntLiteral(1)))
+
+  private val minimalProgram = Program(
+    FreshIdentifier("Minimal"), 
+    ObjectDef(FreshIdentifier("Minimal"), Seq(
+      fDef
+    ), Seq.empty)
+  )
+
+  private val x : Expr = Variable(FreshIdentifier("x").setType(Int32Type))
+  private val y : Expr = Variable(FreshIdentifier("y").setType(Int32Type))
+  private def f(e : Expr) : Expr = FunctionInvocation(fDef, e :: Nil)
+
+  private val solver = new FairZ3Solver(silentContext)
+  solver.setProgram(minimalProgram)
+  solver.restartZ3
+
+  private val tautology1 : Expr = BooleanLiteral(true)
+  assertValid(solver, tautology1)
+
+  private val tautology2 : Expr = Equals(Plus(x, x), Times(IntLiteral(2), x))
+  assertValid(solver, tautology2)
+
+  // This one contains a function invocation but is valid regardless of its
+  // interpretation, so should be proved anyway.
+  private val tautology3 : Expr = Implies(
+    Not(Equals(f(x), f(y))),
+    Not(Equals(x, y))
+  )
+  assertValid(solver, tautology3)
+
+  private val wrong1 : Expr = BooleanLiteral(false)
+  assertInvalid(solver, wrong1)
+
+  private val wrong2 : Expr = Equals(Plus(x, x), Times(IntLiteral(3), x))
+  assertInvalid(solver, wrong2)
+
+  // This is true, and FairZ3Solver should know it (by inlining).
+  private val unknown1 : Expr = Equals(f(x), Plus(x, IntLiteral(1)))
+  assertValid(solver, unknown1)
+
+  test("Check assumptions") {
+    val b1 = Variable(FreshIdentifier("b").setType(BooleanType))
+    val b2 = Variable(FreshIdentifier("b").setType(BooleanType))
+
+    val f = And(b1, Not(b2))
+
+    locally {
+      val sub = solver.getNewSolver
+      sub.assertCnstr(f)
+      assert(sub.check === Some(true))
+    }
+
+    locally {
+      val sub = solver.getNewSolver
+      sub.assertCnstr(f)
+      val result = sub.checkAssumptions(Set(b1))
+
+      assert(result === Some(true))
+      assert(sub.getUnsatCore.isEmpty)
+    }
+
+    locally {
+      val sub = solver.getNewSolver
+      sub.assertCnstr(f)
+
+      val result = sub.checkAssumptions(Set(b1, b2))
+      assert(result === Some(false))
+      assert(sub.getUnsatCore === Set(b2))
+    }
+  }
+}