diff --git a/src/main/scala/leon/solvers/z3/FairZ3Solver.scala b/src/main/scala/leon/solvers/z3/FairZ3Solver.scala
index 8ce1ca76428667e36b6c81e2ef100864ac933750..09172b636c6508f62d2e96da51fb4d132e1ff92c 100644
--- a/src/main/scala/leon/solvers/z3/FairZ3Solver.scala
+++ b/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 {
diff --git a/src/test/scala/leon/test/solvers/z3/BugWithEmptySetNewAPI.scala b/src/test/scala/leon/test/solvers/z3/BugWithEmptySetNewAPI.scala
new file mode 100644
index 0000000000000000000000000000000000000000..98cf970756012ac4c7e6be4277d0ced361e46e1b
--- /dev/null
+++ b/src/test/scala/leon/test/solvers/z3/BugWithEmptySetNewAPI.scala
@@ -0,0 +1,70 @@
+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}""")
+ }
+}
diff --git a/src/test/scala/leon/test/solvers/z3/FairZ3SolverTestsNewAPI.scala b/src/test/scala/leon/test/solvers/z3/FairZ3SolverTestsNewAPI.scala
new file mode 100644
index 0000000000000000000000000000000000000000..92dc5720289fa14f6ea63b8ab99588ca22fe7cf4
--- /dev/null
+++ b/src/test/scala/leon/test/solvers/z3/FairZ3SolverTestsNewAPI.scala
@@ -0,0 +1,122 @@
+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))
+ }
+ }
+}