From b232716878173851851cd7cd3f24922efbd4ac28 Mon Sep 17 00:00:00 2001
From: Philippe Suter <philippe.suter@gmail.com>
Date: Fri, 26 Oct 2012 19:32:56 +0200
Subject: [PATCH] First (sbt) test to make it into master.
---
.gitignore | 4 +
build.sbt | 5 ++
src/main/scala/leon/Reporter.scala | 9 +-
.../solvers/z3/UninterpretedZ3Solver.scala | 27 +++---
.../z3/UninterpretedZ3SolverTests.scala | 85 +++++++++++++++++++
5 files changed, 112 insertions(+), 18 deletions(-)
create mode 100644 src/test/scala/leon/test/solvers/z3/UninterpretedZ3SolverTests.scala
diff --git a/.gitignore b/.gitignore
index 8230049b1..a35dc06b8 100644
--- a/.gitignore
+++ b/.gitignore
@@ -1,3 +1,7 @@
+# Vim
+*.swp
+
+# sbt
target
/project/build
/leon
diff --git a/build.sbt b/build.sbt
index 9c65cad86..817f553b6 100644
--- a/build.sbt
+++ b/build.sbt
@@ -12,5 +12,10 @@ scalacOptions += "-unchecked"
libraryDependencies += "org.scala-lang" % "scala-compiler" % "2.9.1-1"
+libraryDependencies += "org.scalatest" %% "scalatest" % "1.8" % "test"
+
unmanagedBase <<= baseDirectory { base => base / "unmanaged" }
+fork in run := true
+
+fork in test := true
diff --git a/src/main/scala/leon/Reporter.scala b/src/main/scala/leon/Reporter.scala
index 2cdea3d02..03512770f 100644
--- a/src/main/scala/leon/Reporter.scala
+++ b/src/main/scala/leon/Reporter.scala
@@ -57,6 +57,11 @@ class DefaultReporter extends Reporter {
}
class QuietReporter extends DefaultReporter {
- override def warning(msg: Any) = {}
- override def info(msg: Any) = {}
+ override def warning(msg : Any) = {}
+ override def info(msg : Any) = {}
+}
+
+class SilentReporter extends QuietReporter {
+ override def error(msg : Any) = {}
+ override def fatalError(msg : Any) = throw new Exception("Fatal error: " + msg.toString)
}
diff --git a/src/main/scala/leon/solvers/z3/UninterpretedZ3Solver.scala b/src/main/scala/leon/solvers/z3/UninterpretedZ3Solver.scala
index 10162c266..1ad2ed1fc 100644
--- a/src/main/scala/leon/solvers/z3/UninterpretedZ3Solver.scala
+++ b/src/main/scala/leon/solvers/z3/UninterpretedZ3Solver.scala
@@ -52,20 +52,25 @@ class UninterpretedZ3Solver(reporter : Reporter) extends Solver(reporter) with A
// Where the solving occurs
override def solveOrGetCounterexample(expression : Expr) : (Option[Boolean],Map[Identifier,Expr]) = {
+ restartZ3
+
val emptyModel = Map.empty[Identifier,Expr]
val unknownResult = (None, emptyModel)
val validResult = (Some(true), emptyModel)
- containedInvocations = false
val result = toZ3Formula(expression).map { asZ3 =>
z3.assertCnstr(z3.mkNot(asZ3))
z3.checkAndGetModel() match {
case (Some(false), _) => validResult
- case (Some(true), model) if !containedInvocations => {
- val variables = variablesOf(expression)
- val r = (Some(false), modelToMap(model, variables))
- model.delete
- r
+ case (Some(true), model) => {
+ if(containsFunctionCalls(expression)) {
+ unknownResult
+ } else {
+ val variables = variablesOf(expression)
+ val r = (Some(false), modelToMap(model, variables))
+ model.delete
+ r
+ }
}
case _ => unknownResult
}
@@ -73,14 +78,4 @@ class UninterpretedZ3Solver(reporter : Reporter) extends Solver(reporter) with A
result
}
-
- private var containedInvocations : Boolean = _
-
- override def toZ3Formula(expr : Expr, m : Map[Identifier,Z3AST] = Map.empty) : Option[Z3AST] = {
- expr match {
- case FunctionInvocation(_, _) => containedInvocations = true
- case _ => ;
- }
- super.toZ3Formula(expr,m)
- }
}
diff --git a/src/test/scala/leon/test/solvers/z3/UninterpretedZ3SolverTests.scala b/src/test/scala/leon/test/solvers/z3/UninterpretedZ3SolverTests.scala
new file mode 100644
index 000000000..168205440
--- /dev/null
+++ b/src/test/scala/leon/test/solvers/z3/UninterpretedZ3SolverTests.scala
@@ -0,0 +1,85 @@
+package leon.test.solvers.z3
+
+import leon.purescala.Common._
+import leon.purescala.Definitions._
+import leon.purescala.Trees._
+import leon.purescala.TreeOps._
+import leon.purescala.TypeTrees._
+
+import leon.SilentReporter
+
+import leon.Extensions.Solver
+import leon.solvers.z3.UninterpretedZ3Solver
+
+import org.scalatest.FunSuite
+
+class UninterpretedZ3SolverTests 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) {
+ assert(solver.solve(expr) === expected, 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 silentReporter = 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 UninterpretedZ3Solver(silentReporter)
+ solver.setProgram(minimalProgram)
+
+ 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, but that solver shouldn't know it.
+ private val unknown1 : Expr = Equals(f(x), Plus(x, IntLiteral(1)))
+ assertUnknown(solver, unknown1)
+}
--
GitLab