From 0b0723905aa7da0a9ea5f2a728a5d4c6202997fb Mon Sep 17 00:00:00 2001
From: Etienne Kneuss <ekneuss@gmail.com>
Date: Wed, 28 Nov 2012 15:20:58 +0100
Subject: [PATCH] Bettern handling of incremental solvers
---
.../leon/solvers/IncrementalSolver.scala | 72 +++++++++++++++++++
.../scala/leon/solvers/ParallelSolver.scala | 2 +-
.../scala/leon/solvers/RandomSolver.scala | 2 +-
src/main/scala/leon/solvers/Solver.scala | 44 +-----------
.../scala/leon/solvers/TimeoutSolver.scala | 2 +-
.../scala/leon/solvers/TrivialSolver.scala | 2 +-
.../leon/solvers/z3/AbstractZ3Solver.scala | 21 +-----
.../scala/leon/solvers/z3/FairZ3Solver.scala | 52 ++++++++++----
.../solvers/z3/UninterpretedZ3Solver.scala | 42 +++++++++++
9 files changed, 159 insertions(+), 80 deletions(-)
create mode 100644 src/main/scala/leon/solvers/IncrementalSolver.scala
diff --git a/src/main/scala/leon/solvers/IncrementalSolver.scala b/src/main/scala/leon/solvers/IncrementalSolver.scala
new file mode 100644
index 000000000..8a8e5de49
--- /dev/null
+++ b/src/main/scala/leon/solvers/IncrementalSolver.scala
@@ -0,0 +1,72 @@
+package leon
+package solvers
+
+import purescala.Common._
+import purescala.Definitions._
+import purescala.TreeOps._
+import purescala.Trees._
+
+trait IncrementalSolverBuilder {
+ def getNewSolver: IncrementalSolver
+}
+
+trait IncrementalSolver {
+ // New Solver API
+ // Moslty for z3 solvers since z3 4.3
+
+ def push(): Unit
+ def pop(lvl: Int = 1): Unit
+ def assertCnstr(expression: Expr): Unit
+
+ def check: Option[Boolean]
+ def checkAssumptions(assumptions: Seq[Expr]): Option[Boolean]
+ def getModel: Map[Identifier, Expr]
+ def getUnsatCore: Set[Expr]
+}
+
+trait NaiveIncrementalSolver extends IncrementalSolverBuilder {
+ def solveSAT(e: Expr): (Option[Boolean], Map[Identifier, Expr])
+
+ def getNewSolver = new IncrementalSolver {
+ private var stack = List[List[Expr]]()
+
+ def push() {
+ stack = Nil :: stack
+ }
+
+ def pop(lvl: Int = 1) {
+ stack = stack.drop(lvl)
+ }
+
+ def assertCnstr(expression: Expr) {
+ stack = (expression :: stack.head) :: stack.tail
+ }
+
+ private def allConstraints() = stack.flatten
+
+ private var unsatCore = Set[Expr]()
+
+ def check: Option[Boolean] = {
+ solveSAT(And(allConstraints()))._1
+ }
+
+ def checkAssumptions(assumptions: Seq[Expr]): Option[Boolean] = {
+ solveSAT(And(assumptions ++ allConstraints()))._1 match {
+ case Some(true) =>
+ unsatCore = Set[Expr]()
+ Some(true)
+ case r =>
+ unsatCore = assumptions.toSet
+ r
+ }
+ }
+
+ def getModel: Map[Identifier, Expr] = {
+ Map[Identifier, Expr]()
+ }
+
+ def getUnsatCore: Set[Expr] = {
+ unsatCore
+ }
+ }
+}
diff --git a/src/main/scala/leon/solvers/ParallelSolver.scala b/src/main/scala/leon/solvers/ParallelSolver.scala
index 3bc724c68..3ecf8df6f 100644
--- a/src/main/scala/leon/solvers/ParallelSolver.scala
+++ b/src/main/scala/leon/solvers/ParallelSolver.scala
@@ -15,7 +15,7 @@ import scala.actors.Actor._
import scala.concurrent.Lock
@deprecated("Unused, Untested, Unmaintained", "")
-class ParallelSolver(solvers : Solver*) extends Solver(solvers(0).context) {
+class ParallelSolver(solvers : Solver*) extends Solver(solvers(0).context) with NaiveIncrementalSolver {
private val nbSolvers = solvers.size
require(nbSolvers >= 2)
diff --git a/src/main/scala/leon/solvers/RandomSolver.scala b/src/main/scala/leon/solvers/RandomSolver.scala
index f5e37ca29..fead03a79 100644
--- a/src/main/scala/leon/solvers/RandomSolver.scala
+++ b/src/main/scala/leon/solvers/RandomSolver.scala
@@ -12,7 +12,7 @@ import Evaluator._
import scala.util.Random
@deprecated("Unused, Untested, Unmaintained", "")
-class RandomSolver(context: LeonContext, val nbTrial: Option[Int] = None) extends Solver(context) {
+class RandomSolver(context: LeonContext, val nbTrial: Option[Int] = None) extends Solver(context) with NaiveIncrementalSolver {
require(nbTrial.forall(i => i >= 0))
private val reporter = context.reporter
diff --git a/src/main/scala/leon/solvers/Solver.scala b/src/main/scala/leon/solvers/Solver.scala
index 7afbff9b2..0cd3dcac0 100644
--- a/src/main/scala/leon/solvers/Solver.scala
+++ b/src/main/scala/leon/solvers/Solver.scala
@@ -6,7 +6,7 @@ import purescala.Definitions._
import purescala.TreeOps._
import purescala.Trees._
-abstract class Solver(val context : LeonContext) {
+abstract class Solver(val context : LeonContext) extends IncrementalSolverBuilder {
// This used to be in Extension
val description : String
val shortDescription : String
@@ -55,47 +55,5 @@ abstract class Solver(val context : LeonContext) {
}
protected def forceStop = _forceStop
-
- // New Solver API
- // Moslty for z3 solvers since z3 4.3
- private var stack = List[List[Expr]](Nil)
- def push() {
- stack = Nil :: stack
- }
-
- def pop(lvl: Int = 1) {
- stack = stack.drop(lvl)
- }
-
- def assertCnstr(expression: Expr) {
- stack = (expression :: stack.head) :: stack.tail
- }
-
- private def allConstraints() = stack.flatten
-
- def check: Option[Boolean] = {
- solveSAT(And(allConstraints()))._1
- }
-
- private var unsatCore = Set[Expr]()
-
- def checkAssumptions(assumptions: Seq[Expr]): Option[Boolean] = {
- solveSAT(And(assumptions ++ allConstraints()))._1 match {
- case Some(true) =>
- unsatCore = Set[Expr]()
- Some(true)
- case r =>
- unsatCore = assumptions.toSet
- r
- }
- }
-
- def getModel: Map[Identifier, Expr] = {
- Map[Identifier, Expr]()
- }
-
- def getUnsatCore: Set[Expr] = {
- unsatCore
- }
}
diff --git a/src/main/scala/leon/solvers/TimeoutSolver.scala b/src/main/scala/leon/solvers/TimeoutSolver.scala
index 2c1de0e4b..8f1f18ad1 100644
--- a/src/main/scala/leon/solvers/TimeoutSolver.scala
+++ b/src/main/scala/leon/solvers/TimeoutSolver.scala
@@ -8,7 +8,7 @@ import purescala.TypeTrees._
import scala.sys.error
-class TimeoutSolver(solver : Solver, timeout : Int) extends Solver(solver.context) {
+class TimeoutSolver(solver : Solver, timeout : Int) extends Solver(solver.context) with NaiveIncrementalSolver {
val description = solver.description + ", with timeout"
override val shortDescription = solver.shortDescription + "+t"
diff --git a/src/main/scala/leon/solvers/TrivialSolver.scala b/src/main/scala/leon/solvers/TrivialSolver.scala
index 17fac01f0..bd8edcf50 100644
--- a/src/main/scala/leon/solvers/TrivialSolver.scala
+++ b/src/main/scala/leon/solvers/TrivialSolver.scala
@@ -6,7 +6,7 @@ import purescala.Definitions._
import purescala.Trees._
import purescala.TypeTrees._
-class TrivialSolver(context: LeonContext) extends Solver(context) {
+class TrivialSolver(context: LeonContext) extends Solver(context) with NaiveIncrementalSolver {
val description = "Solver for syntactically trivial formulas"
override val shortDescription = "trivial"
diff --git a/src/main/scala/leon/solvers/z3/AbstractZ3Solver.scala b/src/main/scala/leon/solvers/z3/AbstractZ3Solver.scala
index 993496484..bfcec027c 100644
--- a/src/main/scala/leon/solvers/z3/AbstractZ3Solver.scala
+++ b/src/main/scala/leon/solvers/z3/AbstractZ3Solver.scala
@@ -13,7 +13,7 @@ import scala.collection.mutable.{Set => MutableSet}
// This is just to factor out the things that are common in "classes that deal
// with a Z3 instance"
-trait AbstractZ3Solver {
+trait AbstractZ3Solver extends solvers.IncrementalSolverBuilder {
self: leon.solvers.Solver =>
val context : LeonContext
@@ -96,25 +96,6 @@ trait AbstractZ3Solver {
}
}
- override def push() {
- solver.push
- }
-
- override def pop(lvl: Int = 1) {
- solver.pop(lvl)
- }
-
- override def assertCnstr(expression: Expr) {
- solver.assertCnstr(toZ3Formula(expression).get)
- }
-
- override def check: Option[Boolean] = {
- solver.check
- }
-
- override def checkAssumptions(assumptions: Seq[Expr]): Option[Boolean] = {
- solver.checkAssumptions(assumptions.map(toZ3Formula(_).get) : _*)
- }
protected[leon] def restartZ3 : Unit = {
counter = 0
diff --git a/src/main/scala/leon/solvers/z3/FairZ3Solver.scala b/src/main/scala/leon/solvers/z3/FairZ3Solver.scala
index 93c0e8e73..0660dd26c 100644
--- a/src/main/scala/leon/solvers/z3/FairZ3Solver.scala
+++ b/src/main/scala/leon/solvers/z3/FairZ3Solver.scala
@@ -160,19 +160,6 @@ class FairZ3Solver(context : LeonContext) extends Solver(context) with AbstractZ
}
}
- override def getModel = {
- modelToMap(solver.getModel, varsInVC)
- }
-
- override def getUnsatCore = {
- solver.getUnsatCore.map(ast => fromZ3Formula(null, ast, None) match {
- case n @ Not(Variable(_)) => n
- case v @ Variable(_) => v
- case x => scala.sys.error("Impossible element extracted from core: " + ast + " (as Leon tree : " + x + ")")
- }).toSet
- }
-
-
override def solveSATWithCores(expression: Expr, assumptions: Set[Expr]): (Option[Boolean], Map[Identifier, Expr], Set[Expr]) = {
restartZ3
decideWithModel(expression, false, None, Some(assumptions))
@@ -703,5 +690,44 @@ class FairZ3Solver(context : LeonContext) extends Solver(context) with AbstractZ
}
}
+
+ def getNewSolver = new solvers.IncrementalSolver {
+ val solver = z3.mkSolver
+
+ def push() {
+ solver.push
+ }
+
+ def pop(lvl: Int = 1) {
+ solver.pop(lvl)
+ }
+
+ def assertCnstr(expression: Expr) {
+ solver.assertCnstr(toZ3Formula(expression).get)
+ }
+
+ def check: Option[Boolean] = {
+ solver.check
+ }
+
+ def checkAssumptions(assumptions: Seq[Expr]): Option[Boolean] = {
+ solver.checkAssumptions(assumptions.map(toZ3Formula(_).get) : _*)
+ }
+
+ def getModel = {
+ modelToMap(solver.getModel, varsInVC)
+ }
+
+ def getUnsatCore = {
+ solver.getUnsatCore.map(ast => fromZ3Formula(null, ast, None) match {
+ case n @ Not(Variable(_)) => n
+ case v @ Variable(_) => v
+ case x => scala.sys.error("Impossible element extracted from core: " + ast + " (as Leon tree : " + x + ")")
+ }).toSet
+ }
+
+
+ }
+
}
diff --git a/src/main/scala/leon/solvers/z3/UninterpretedZ3Solver.scala b/src/main/scala/leon/solvers/z3/UninterpretedZ3Solver.scala
index 9215e6c40..2d40fcf1d 100644
--- a/src/main/scala/leon/solvers/z3/UninterpretedZ3Solver.scala
+++ b/src/main/scala/leon/solvers/z3/UninterpretedZ3Solver.scala
@@ -80,4 +80,46 @@ class UninterpretedZ3Solver(context : LeonContext) extends Solver(context) with
result
}
+
+ def getNewSolver = new solvers.IncrementalSolver {
+ val solver = z3.mkSolver
+
+ def push() {
+ solver.push
+ }
+
+ def pop(lvl: Int = 1) {
+ solver.pop(lvl)
+ }
+
+ private var variables = Set[Identifier]()
+
+ def assertCnstr(expression: Expr) {
+ variables ++= variablesOf(expression)
+ solver.assertCnstr(toZ3Formula(expression).get)
+ }
+
+ def check: Option[Boolean] = {
+ solver.check
+ }
+
+ def checkAssumptions(assumptions: Seq[Expr]): Option[Boolean] = {
+ variables ++= assumptions.flatMap(variablesOf(_))
+ solver.checkAssumptions(assumptions.map(toZ3Formula(_).get) : _*)
+ }
+
+ def getModel = {
+ modelToMap(solver.getModel, variables)
+ }
+
+ def getUnsatCore = {
+ solver.getUnsatCore.map(ast => fromZ3Formula(null, ast, None) match {
+ case n @ Not(Variable(_)) => n
+ case v @ Variable(_) => v
+ case x => scala.sys.error("Impossible element extracted from core: " + ast + " (as Leon tree : " + x + ")")
+ }).toSet
+ }
+
+
+ }
}
--
GitLab