From fbf2bea6e0e2b9b830c9df3294156d5019439940 Mon Sep 17 00:00:00 2001
From: Etienne Kneuss <ekneuss@gmail.com>
Date: Tue, 4 Aug 2015 09:12:43 +0200
Subject: [PATCH] Implement solver pools
- solvers are not freed directly, they are reclaimed by their
solver factory
- reset() is used when available to reset a solver instead of creating a
fresh one.
---
.../codegen/runtime/ChooseEntryPoint.scala | 6 +-
.../leon/evaluators/RecursiveEvaluator.scala | 2 +-
src/main/scala/leon/repair/rules/Verify.scala | 54 +++++++-------
.../leon/solvers/CantResetException.scala | 3 +
.../leon/solvers/EnumerationSolver.scala | 11 ++-
.../scala/leon/solvers/GroundSolver.scala | 4 +
.../scala/leon/solvers/ResettableSolver.scala | 10 +++
.../solvers/SimpleAssumptionSolverAPI.scala | 2 +-
.../scala/leon/solvers/SimpleSolverAPI.scala | 4 +-
src/main/scala/leon/solvers/Solver.scala | 2 +
.../scala/leon/solvers/SolverFactory.scala | 9 ++-
.../scala/leon/solvers/TimeoutSolver.scala | 7 ++
.../leon/solvers/TimeoutSolverFactory.scala | 7 +-
.../leon/solvers/combinators/DNFSolver.scala | 4 +
.../solvers/combinators/PortfolioSolver.scala | 24 +++---
.../combinators/PortfolioSolverFactory.scala | 27 +++++++
.../leon/solvers/combinators/SolverPool.scala | 73 +++++++++++++++++++
.../solvers/combinators/UnrollingSolver.scala | 16 +++-
src/main/scala/leon/solvers/package.scala | 15 ++--
.../smtlib/SMTLIBCVC4QuantifiedSolver.scala | 2 +-
.../leon/solvers/smtlib/SMTLIBSolver.scala | 15 +++-
.../leon/solvers/z3/AbstractZ3Solver.scala | 4 +
.../leon/synthesis/SynthesisContext.scala | 12 +--
.../scala/leon/synthesis/Synthesizer.scala | 1 -
.../leon/synthesis/rules/CEGISLike.scala | 17 ++---
.../leon/synthesis/rules/EqualitySplit.scala | 4 +-
.../synthesis/rules/InequalitySplit.scala | 4 +-
.../synthesis/rules/OptimisticGround.scala | 4 +-
28 files changed, 251 insertions(+), 92 deletions(-)
create mode 100644 src/main/scala/leon/solvers/CantResetException.scala
create mode 100644 src/main/scala/leon/solvers/ResettableSolver.scala
create mode 100644 src/main/scala/leon/solvers/combinators/PortfolioSolverFactory.scala
create mode 100644 src/main/scala/leon/solvers/combinators/SolverPool.scala
diff --git a/src/main/scala/leon/codegen/runtime/ChooseEntryPoint.scala b/src/main/scala/leon/codegen/runtime/ChooseEntryPoint.scala
index 2a99f0131..e8b38e5ba 100644
--- a/src/main/scala/leon/codegen/runtime/ChooseEntryPoint.scala
+++ b/src/main/scala/leon/codegen/runtime/ChooseEntryPoint.scala
@@ -79,8 +79,8 @@ object ChooseEntryPoint {
} else {
val tStart = System.currentTimeMillis
- val solverf = SolverFactory.default(ctx, program).withTimeout(10.second)
- val solver = solverf.getNewSolver()
+ val solverf = SolverFactory.default(ctx, program)
+ val solver = solverf.getNewSolver().setTimeout(10.seconds)
val inputsMap = (p.as zip inputs).map {
case (id, v) =>
@@ -113,7 +113,7 @@ object ChooseEntryPoint {
throw new LeonCodeGenRuntimeException("Timeout exceeded")
}
} finally {
- solver.free()
+ solverf.reclaim(solver)
solverf.shutdown()
}
}
diff --git a/src/main/scala/leon/evaluators/RecursiveEvaluator.scala b/src/main/scala/leon/evaluators/RecursiveEvaluator.scala
index 95a0c0195..1eb6398ea 100644
--- a/src/main/scala/leon/evaluators/RecursiveEvaluator.scala
+++ b/src/main/scala/leon/evaluators/RecursiveEvaluator.scala
@@ -587,7 +587,7 @@ abstract class RecursiveEvaluator(ctx: LeonContext, prog: Program, maxSteps: Int
throw RuntimeError("Timeout exceeded")
}
} finally {
- solver.free()
+ solverf.reclaim(solver)
solverf.shutdown()
}
})
diff --git a/src/main/scala/leon/repair/rules/Verify.scala b/src/main/scala/leon/repair/rules/Verify.scala
index b3590729e..e9bb92bc3 100644
--- a/src/main/scala/leon/repair/rules/Verify.scala
+++ b/src/main/scala/leon/repair/rules/Verify.scala
@@ -38,34 +38,34 @@ case object Verify extends NormalizingRule("Verify") {
val vc = simp(and(p.pc, letTuple(p.xs, e, not(p.phi))))
- val solver = hctx.sctx.newSolver.setTimeout(2000L)
-
- solver.assertCnstr(vc)
- val osol = solver.check match {
- case Some(false) =>
- Some(Solution(BooleanLiteral(true), Set(), e, true))
-
- case None =>
- hctx.reporter.ifDebug { printer =>
- printer(vc)
- printer("== Unknown ==")
- }
- //None
- //Some(Solution(BooleanLiteral(true), Set(), wrappedE, false))
- None
-
- case _ =>
- hctx.reporter.ifDebug { printer =>
- printer(vc)
- printer("== Invalid! ==")
+ val solverf = hctx.sctx.solverFactory
+ val solver = solverf.getNewSolver.setTimeout(2000L)
+ try {
+ solver.assertCnstr(vc)
+
+ solver.check match {
+ case Some(false) =>
+ Some(solve(Solution(BooleanLiteral(true), Set(), e, true)))
+
+ case None =>
+ hctx.reporter.ifDebug { printer =>
+ printer(vc)
+ printer("== Unknown ==")
+ }
+ //None
+ //Some(Solution(BooleanLiteral(true), Set(), wrappedE, false))
+ None
+
+ case _ =>
+ hctx.reporter.ifDebug { printer =>
+ printer(vc)
+ printer("== Invalid! ==")
+ }
+ None
}
- None
- }
-
- solver.free
-
- osol.map { solve }
-
+ } finally {
+ solverf.reclaim(solver)
+ }
}
alts
diff --git a/src/main/scala/leon/solvers/CantResetException.scala b/src/main/scala/leon/solvers/CantResetException.scala
new file mode 100644
index 000000000..51646c8fe
--- /dev/null
+++ b/src/main/scala/leon/solvers/CantResetException.scala
@@ -0,0 +1,3 @@
+package leon.solvers
+
+class CantResetException(s: Solver) extends Exception(s"Unable to reset solver $s")
diff --git a/src/main/scala/leon/solvers/EnumerationSolver.scala b/src/main/scala/leon/solvers/EnumerationSolver.scala
index d432aaddc..5b14c05da 100644
--- a/src/main/scala/leon/solvers/EnumerationSolver.scala
+++ b/src/main/scala/leon/solvers/EnumerationSolver.scala
@@ -33,15 +33,22 @@ class EnumerationSolver(val context: LeonContext, val program: Program) extends
}
def push() = {
- freeVars = Nil :: freeVars
+ freeVars = Nil :: freeVars
constraints = Nil :: constraints
}
def pop(lvl: Int) = {
- freeVars = freeVars.drop(lvl)
+ freeVars = freeVars.drop(lvl)
constraints = constraints.drop(lvl)
}
+ def reset() = {
+ freeVars = List(Nil)
+ constraints = List(Nil)
+ interrupted = false
+ datagen = None
+ }
+
private var modelMap = Map[Identifier, Expr]()
def check: Option[Boolean] = {
diff --git a/src/main/scala/leon/solvers/GroundSolver.scala b/src/main/scala/leon/solvers/GroundSolver.scala
index 5cdaa5e42..443706fdf 100644
--- a/src/main/scala/leon/solvers/GroundSolver.scala
+++ b/src/main/scala/leon/solvers/GroundSolver.scala
@@ -51,6 +51,10 @@ class GroundSolver(val context: LeonContext, val program: Program) extends Solve
def free(): Unit = assertions = Nil
+ def reset() = {
+ assertions = Nil
+ }
+
def interrupt(): Unit = {}
def recoverInterrupt(): Unit = {}
diff --git a/src/main/scala/leon/solvers/ResettableSolver.scala b/src/main/scala/leon/solvers/ResettableSolver.scala
new file mode 100644
index 000000000..ca5eba931
--- /dev/null
+++ b/src/main/scala/leon/solvers/ResettableSolver.scala
@@ -0,0 +1,10 @@
+/* Copyright 2009-2015 EPFL, Lausanne */
+
+package leon
+package solvers
+
+import purescala.Expressions.Expr
+
+trait ResettableSolver extends Solver {
+ def reset()
+}
diff --git a/src/main/scala/leon/solvers/SimpleAssumptionSolverAPI.scala b/src/main/scala/leon/solvers/SimpleAssumptionSolverAPI.scala
index cc382dd41..eb92c529c 100644
--- a/src/main/scala/leon/solvers/SimpleAssumptionSolverAPI.scala
+++ b/src/main/scala/leon/solvers/SimpleAssumptionSolverAPI.scala
@@ -21,7 +21,7 @@ class SimpleAssumptionSolverAPI(sf: SolverFactory[AssumptionSolver]) extends Sim
(None, Map(), Set())
}
} finally {
- s.free()
+ sf.reclaim(s)
}
}
}
diff --git a/src/main/scala/leon/solvers/SimpleSolverAPI.scala b/src/main/scala/leon/solvers/SimpleSolverAPI.scala
index 9e92f3775..907f903df 100644
--- a/src/main/scala/leon/solvers/SimpleSolverAPI.scala
+++ b/src/main/scala/leon/solvers/SimpleSolverAPI.scala
@@ -13,7 +13,7 @@ class SimpleSolverAPI(sf: SolverFactory[Solver]) {
s.assertCnstr(Not(expression))
s.check.map(r => !r)
} finally {
- s.free()
+ sf.reclaim(s)
}
}
@@ -30,7 +30,7 @@ class SimpleSolverAPI(sf: SolverFactory[Solver]) {
(None, Map())
}
} finally {
- s.free()
+ sf.reclaim(s)
}
}
}
diff --git a/src/main/scala/leon/solvers/Solver.scala b/src/main/scala/leon/solvers/Solver.scala
index 69eef7449..54879dcc4 100644
--- a/src/main/scala/leon/solvers/Solver.scala
+++ b/src/main/scala/leon/solvers/Solver.scala
@@ -25,6 +25,8 @@ trait Solver {
def free()
+ def reset()
+
implicit val debugSection = DebugSectionSolver
private[solvers] def debugS(msg: String) = {
diff --git a/src/main/scala/leon/solvers/SolverFactory.scala b/src/main/scala/leon/solvers/SolverFactory.scala
index 64cf6e3d7..a43dc9664 100644
--- a/src/main/scala/leon/solvers/SolverFactory.scala
+++ b/src/main/scala/leon/solvers/SolverFactory.scala
@@ -14,12 +14,13 @@ import _root_.smtlib.interpreters._
abstract class SolverFactory[+S <: Solver : TypeTag] {
def getNewSolver(): S
- def init(): Unit = {}
def shutdown(): Unit = {}
- val name = typeOf[S].toString.split("\\.").last.replaceAll("Solver", "")+"*"
+ def reclaim(s: Solver) {
+ s.free()
+ }
- init()
+ val name = typeOf[S].toString.split("\\.").last.replaceAll("Solver", "")+"*"
}
object SolverFactory {
@@ -118,7 +119,7 @@ object SolverFactory {
} else if (selectedSolvers.size == 1) {
selectedSolvers.head
} else {
- SolverFactory( () => new PortfolioSolver(ctx, selectedSolvers.toSeq) with TimeoutSolver)
+ new PortfolioSolverFactory(ctx, selectedSolvers.toSeq)
}
}
diff --git a/src/main/scala/leon/solvers/TimeoutSolver.scala b/src/main/scala/leon/solvers/TimeoutSolver.scala
index 1ff88c1d6..a7c27f1a0 100644
--- a/src/main/scala/leon/solvers/TimeoutSolver.scala
+++ b/src/main/scala/leon/solvers/TimeoutSolver.scala
@@ -5,6 +5,8 @@ package solvers
import utils._
+import scala.concurrent.duration._
+
trait TimeoutSolver extends Solver with Interruptible {
val ti = new TimeoutFor(this)
@@ -16,6 +18,11 @@ trait TimeoutSolver extends Solver with Interruptible {
this
}
+ def setTimeout(timeout: Duration): this.type = {
+ optTimeout = Some(timeout.toMillis)
+ this
+ }
+
abstract override def check: Option[Boolean] = {
optTimeout match {
case Some(to) =>
diff --git a/src/main/scala/leon/solvers/TimeoutSolverFactory.scala b/src/main/scala/leon/solvers/TimeoutSolverFactory.scala
index 587b1d744..b5a042147 100644
--- a/src/main/scala/leon/solvers/TimeoutSolverFactory.scala
+++ b/src/main/scala/leon/solvers/TimeoutSolverFactory.scala
@@ -5,12 +5,13 @@ package solvers
import scala.reflect.runtime.universe._
-class TimeoutSolverFactory[+S <: TimeoutSolver : TypeTag](sf: SolverFactory[S], to: Long) extends SolverFactory[S] {
+class TimeoutSolverFactory[+S <: TimeoutSolver : TypeTag](val sf: SolverFactory[S], to: Long) extends SolverFactory[S] {
override def getNewSolver() = sf.getNewSolver().setTimeout(to)
- override val name = "SFact("+typeOf[S].toString+") with t.o"
+ override val name = sf.name+" with t.o"
+
+ override def reclaim(s: Solver) = sf.reclaim(s)
- override def init() = sf.init()
override def shutdown() = sf.shutdown()
}
diff --git a/src/main/scala/leon/solvers/combinators/DNFSolver.scala b/src/main/scala/leon/solvers/combinators/DNFSolver.scala
index 9f9bd8ed0..ad48ca2cd 100644
--- a/src/main/scala/leon/solvers/combinators/DNFSolver.scala
+++ b/src/main/scala/leon/solvers/combinators/DNFSolver.scala
@@ -26,6 +26,10 @@ class DNFSolver(val context: LeonContext,
theConstraint = Some(expression)
}
+ def reset() = {
+ throw new CantResetException(this)
+ }
+
def check : Option[Boolean] = theConstraint.map { expr =>
val simpleSolver = SimpleSolverAPI(underlyings)
diff --git a/src/main/scala/leon/solvers/combinators/PortfolioSolver.scala b/src/main/scala/leon/solvers/combinators/PortfolioSolver.scala
index 1f990a0c5..ea8331a4a 100644
--- a/src/main/scala/leon/solvers/combinators/PortfolioSolver.scala
+++ b/src/main/scala/leon/solvers/combinators/PortfolioSolver.scala
@@ -14,7 +14,7 @@ import scala.concurrent.duration._
import ExecutionContext.Implicits.global
-class PortfolioSolver[S <: Solver with Interruptible](val context: LeonContext, val solvers: Seq[SolverFactory[S]])
+class PortfolioSolver[S <: Solver with Interruptible](val context: LeonContext, val solvers: Seq[S])
extends Solver with Interruptible {
val name = "Pfolio"
@@ -22,17 +22,16 @@ class PortfolioSolver[S <: Solver with Interruptible](val context: LeonContext,
var constraints = List[Expr]()
protected var modelMap = Map[Identifier, Expr]()
- protected var solversInsts: Seq[S] = solvers.map(_.getNewSolver())
protected var resultSolver: Option[Solver] = None
override def getResultSolver = resultSolver
def assertCnstr(expression: Expr): Unit = {
- solversInsts.foreach(_.assertCnstr(expression))
+ solvers.foreach(_.assertCnstr(expression))
}
override def assertVC(vc: VC): Unit = {
- solversInsts.foreach(_.assertVC(vc))
+ solvers.foreach(_.assertVC(vc))
}
def check: Option[Boolean] = {
@@ -40,7 +39,7 @@ class PortfolioSolver[S <: Solver with Interruptible](val context: LeonContext,
context.reporter.debug("Running portfolio check")
// solving
- val fs = solversInsts.map { s =>
+ val fs = solvers.map { s =>
Future {
val result = s.check
val model: Map[Identifier, Expr] = if (result == Some(true)) {
@@ -61,7 +60,7 @@ class PortfolioSolver[S <: Solver with Interruptible](val context: LeonContext,
resultSolver.foreach { solv =>
context.reporter.debug("Solved with "+solv)
}
- solversInsts.foreach(_.interrupt())
+ solvers.foreach(_.interrupt())
r
case None =>
None
@@ -72,8 +71,7 @@ class PortfolioSolver[S <: Solver with Interruptible](val context: LeonContext,
}
def free() = {
- solversInsts.foreach(_.free)
- solversInsts = Nil
+ solvers.foreach(_.free)
modelMap = Map()
constraints = Nil
}
@@ -83,10 +81,16 @@ class PortfolioSolver[S <: Solver with Interruptible](val context: LeonContext,
}
def interrupt(): Unit = {
- solversInsts.foreach(_.interrupt())
+ solvers.foreach(_.interrupt())
}
def recoverInterrupt(): Unit = {
- solversInsts.foreach(_.recoverInterrupt())
+ solvers.foreach(_.recoverInterrupt())
+ }
+
+ def reset() = {
+ solvers.foreach(_.reset)
+ modelMap = Map()
+ constraints = Nil
}
}
diff --git a/src/main/scala/leon/solvers/combinators/PortfolioSolverFactory.scala b/src/main/scala/leon/solvers/combinators/PortfolioSolverFactory.scala
new file mode 100644
index 000000000..85c862d29
--- /dev/null
+++ b/src/main/scala/leon/solvers/combinators/PortfolioSolverFactory.scala
@@ -0,0 +1,27 @@
+/* Copyright 2009-2015 EPFL, Lausanne */
+
+package leon
+package solvers
+package combinators
+
+import utils.Interruptible
+import scala.collection.mutable.Queue
+import scala.reflect.runtime.universe._
+
+class PortfolioSolverFactory[S <: Solver with Interruptible](ctx: LeonContext, sfs: Seq[SolverFactory[S]])(implicit tag: TypeTag[S]) extends SolverFactory[PortfolioSolver[S] with TimeoutSolver] {
+
+ def getNewSolver(): PortfolioSolver[S] with TimeoutSolver = {
+ new PortfolioSolver[S](ctx, sfs.map(_.getNewSolver())) with TimeoutSolver
+ }
+
+ override def reclaim(s: Solver) = s match {
+ case ps: PortfolioSolver[_] =>
+ sfs.zip(ps.solvers).foreach { case (sf, s) =>
+ sf.reclaim(s)
+ }
+
+ case _ =>
+ ctx.reporter.error("Failed to reclaim a non-portfolio solver.")
+ }
+}
+
diff --git a/src/main/scala/leon/solvers/combinators/SolverPool.scala b/src/main/scala/leon/solvers/combinators/SolverPool.scala
new file mode 100644
index 000000000..296e6b713
--- /dev/null
+++ b/src/main/scala/leon/solvers/combinators/SolverPool.scala
@@ -0,0 +1,73 @@
+/* Copyright 2009-2015 EPFL, Lausanne */
+
+package leon
+package solvers
+package combinators
+
+import scala.collection.mutable.Queue
+import scala.reflect.runtime.universe._
+
+/**
+ * This is a straitforward implementation of solver pools. The goal is to avoid
+ * the cost of spawing processes for SMT solvers.
+ *
+ * Sadly smt-z3 is the only SMT solver that supports reset.
+ *
+ * If necessary, we may want to implement async reclaim/reset,
+ * growing/shrinking pool size...
+ */
+
+class SolverPoolFactory[+S <: Solver](ctx: LeonContext, sf: SolverFactory[S])(implicit tag: TypeTag[S]) extends SolverFactory[S] {
+
+ var poolSize = 0
+ val poolMaxSize = 5
+
+ private[this] val availables = Queue[S]()
+ private[this] var inUse = Set[Solver]()
+
+ def getNewSolver(): S = {
+ if (availables.isEmpty) {
+ poolSize += 1
+ availables += sf.getNewSolver()
+ }
+
+ val s = availables.dequeue()
+ inUse += s
+ s
+ }
+
+ override def reclaim(s: Solver) = {
+ try {
+ s.reset()
+ inUse -= s
+ s.reset()
+ availables += s.asInstanceOf[S]
+ } catch {
+ case _: CantResetException =>
+ inUse -= s
+ s.free()
+ sf.reclaim(s)
+ availables += sf.getNewSolver()
+ }
+ }
+
+ def init(): Unit = {
+ for (i <- 1 to poolMaxSize) {
+ availables += sf.getNewSolver()
+ }
+
+ poolSize = poolMaxSize
+ }
+
+ override def shutdown(): Unit = {
+ for (s <- availables ++ inUse) {
+ sf.reclaim(s)
+ }
+
+ availables.clear()
+
+ inUse = Set()
+ }
+
+ init()
+}
diff --git a/src/main/scala/leon/solvers/combinators/UnrollingSolver.scala b/src/main/scala/leon/solvers/combinators/UnrollingSolver.scala
index 7ab318038..b93e6826a 100644
--- a/src/main/scala/leon/solvers/combinators/UnrollingSolver.scala
+++ b/src/main/scala/leon/solvers/combinators/UnrollingSolver.scala
@@ -29,12 +29,12 @@ class UnrollingSolver(val context: LeonContext, program: Program, underlying: In
}
}
- private var lastCheckResult : (Boolean, Option[Boolean], Option[Map[Identifier,Expr]]) = (false, None, None)
+ protected var lastCheckResult : (Boolean, Option[Boolean], Option[Map[Identifier,Expr]]) = (false, None, None)
- private var varsInVC = List[Set[Identifier]](Set())
- private var frameExpressions = List[List[Expr]](Nil)
+ protected var varsInVC = List[Set[Identifier]](Set())
+ protected var frameExpressions = List[List[Expr]](Nil)
- private var interrupted : Boolean = false
+ protected var interrupted : Boolean = false
val reporter = context.reporter
@@ -250,6 +250,14 @@ class UnrollingSolver(val context: LeonContext, program: Program, underlying: In
}
}
+ override def reset() = {
+ underlying.reset()
+ lastCheckResult = (false, None, None)
+ varsInVC = List(Set())
+ frameExpressions = List(Nil)
+ interrupted = false
+ }
+
override def interrupt(): Unit = {
interrupted = true
solver.interrupt()
diff --git a/src/main/scala/leon/solvers/package.scala b/src/main/scala/leon/solvers/package.scala
index e796cf4d1..e08e536da 100644
--- a/src/main/scala/leon/solvers/package.scala
+++ b/src/main/scala/leon/solvers/package.scala
@@ -6,13 +6,18 @@ import scala.reflect.runtime.universe._
import scala.concurrent.duration._
package object solvers {
- implicit class TimeoutableSolverFactory[+S <: TimeoutSolver : TypeTag](sf: SolverFactory[S]) {
- def withTimeout(to: Long) = {
- new TimeoutSolverFactory[S](sf, to)
+ implicit class TimeoutableSolverFactory[+S <: TimeoutSolver : TypeTag](val sf: SolverFactory[S]) {
+ def withTimeout(to: Long): TimeoutSolverFactory[S] = {
+ sf match {
+ case tsf: TimeoutSolverFactory[_] =>
+ new TimeoutSolverFactory[S](tsf.sf, to)
+ case _ =>
+ new TimeoutSolverFactory[S](sf, to)
+ }
}
- def withTimeout(du: Duration) = {
- new TimeoutSolverFactory[S](sf, du.toMillis)
+ def withTimeout(du: Duration): TimeoutSolverFactory[S] = {
+ withTimeout(du.toMillis)
}
}
}
diff --git a/src/main/scala/leon/solvers/smtlib/SMTLIBCVC4QuantifiedSolver.scala b/src/main/scala/leon/solvers/smtlib/SMTLIBCVC4QuantifiedSolver.scala
index fd9085a95..df167148e 100644
--- a/src/main/scala/leon/solvers/smtlib/SMTLIBCVC4QuantifiedSolver.scala
+++ b/src/main/scala/leon/solvers/smtlib/SMTLIBCVC4QuantifiedSolver.scala
@@ -107,7 +107,7 @@ abstract class SMTLIBCVC4QuantifiedSolver(context: LeonContext, program: Program
}
}
- parameterlessAssertions foreach sendCommand
+ parameterlessAssertions.foreach(a => sendCommand(a))
functions.toB(tfd)
}
diff --git a/src/main/scala/leon/solvers/smtlib/SMTLIBSolver.scala b/src/main/scala/leon/solvers/smtlib/SMTLIBSolver.scala
index e9faa425c..478c17d5d 100644
--- a/src/main/scala/leon/solvers/smtlib/SMTLIBSolver.scala
+++ b/src/main/scala/leon/solvers/smtlib/SMTLIBSolver.scala
@@ -31,7 +31,7 @@ import _root_.smtlib.{Interpreter => SMTInterpreter}
abstract class SMTLIBSolver(val context: LeonContext,
val program: Program)
- extends IncrementalSolver with Interruptible {
+ extends IncrementalSolver with ResettableSolver with Interruptible {
/* Solver name */
@@ -686,14 +686,14 @@ abstract class SMTLIBSolver(val context: LeonContext,
/* Send a command to the solver */
- def sendCommand(cmd: Command): CommandResponse = {
+ def sendCommand(cmd: Command, rawOut: Boolean = false): CommandResponse = {
out foreach { o =>
SMTPrinter.printCommand(cmd, o)
o.write("\n")
o.flush()
}
interpreter.eval(cmd) match {
- case err@ErrorResponse(msg) if !hasError && !interrupted =>
+ case err@ErrorResponse(msg) if !hasError && !interrupted && !rawOut =>
reporter.warning(s"Unexpected error from $name solver: $msg")
// Store that there was an error. Now all following check()
// invocations will return None
@@ -725,6 +725,15 @@ abstract class SMTLIBSolver(val context: LeonContext,
}
}
+ override def reset() = {
+ sendCommand(Reset(), rawOut = true) match {
+ case ErrorResponse(msg) =>
+ reporter.warning(s"Failed to reset $name: $msg")
+ throw new CantResetException(this)
+ case _ =>
+ }
+ }
+
override def check: Option[Boolean] = {
if (hasError) None
else sendCommand(CheckSat()) match {
diff --git a/src/main/scala/leon/solvers/z3/AbstractZ3Solver.scala b/src/main/scala/leon/solvers/z3/AbstractZ3Solver.scala
index 1b33ca60d..d24b88473 100644
--- a/src/main/scala/leon/solvers/z3/AbstractZ3Solver.scala
+++ b/src/main/scala/leon/solvers/z3/AbstractZ3Solver.scala
@@ -810,4 +810,8 @@ trait AbstractZ3Solver
z3.mkFreshConst(id.uniqueName, typeToSort(id.getType))
}
+ def reset() = {
+ throw new CantResetException(this)
+ }
+
}
diff --git a/src/main/scala/leon/synthesis/SynthesisContext.scala b/src/main/scala/leon/synthesis/SynthesisContext.scala
index 77de6d641..bb90d2a26 100644
--- a/src/main/scala/leon/synthesis/SynthesisContext.scala
+++ b/src/main/scala/leon/synthesis/SynthesisContext.scala
@@ -4,7 +4,7 @@ package leon
package synthesis
import solvers._
-import solvers.z3._
+import solvers.combinators._
import purescala.Definitions.{Program, FunDef}
/**
@@ -22,16 +22,6 @@ case class SynthesisContext(
val rules = settings.rules
val solverFactory = SolverFactory.getFromSettings(context, program)
-
- def newSolver = {
- solverFactory.getNewSolver()
- }
-
- val fastSolverFactory = SolverFactory.uninterpreted(context, program)
-
- def newFastSolver = {
- fastSolverFactory.getNewSolver()
- }
}
object SynthesisContext {
diff --git a/src/main/scala/leon/synthesis/Synthesizer.scala b/src/main/scala/leon/synthesis/Synthesizer.scala
index 2d2590da0..9659f2b77 100644
--- a/src/main/scala/leon/synthesis/Synthesizer.scala
+++ b/src/main/scala/leon/synthesis/Synthesizer.scala
@@ -112,7 +112,6 @@ class Synthesizer(val context : LeonContext,
def shutdown(): Unit = {
sctx.solverFactory.shutdown()
- sctx.fastSolverFactory.shutdown()
}
}
diff --git a/src/main/scala/leon/synthesis/rules/CEGISLike.scala b/src/main/scala/leon/synthesis/rules/CEGISLike.scala
index 52f104bae..c78750adc 100644
--- a/src/main/scala/leon/synthesis/rules/CEGISLike.scala
+++ b/src/main/scala/leon/synthesis/rules/CEGISLike.scala
@@ -502,7 +502,7 @@ abstract class CEGISLike[T <% Typed](name: String) extends Rule(name) {
}
}
} finally {
- solver.free()
+ solverf.reclaim(solver)
solverf.shutdown()
cTreeFd.fullBody = origImpl
}
@@ -598,7 +598,7 @@ abstract class CEGISLike[T <% Typed](name: String) extends Rule(name) {
Some(None)
}
} finally {
- solver.free()
+ solverf.reclaim(solver)
solverf.shutdown()
}
}
@@ -631,14 +631,10 @@ abstract class CEGISLike[T <% Typed](name: String) extends Rule(name) {
None
}
} finally {
- solver.free()
+ solverf.reclaim(solver)
solverf.shutdown()
}
}
-
- def free(): Unit = {
-
- }
}
List(new RuleInstantiation(this.name) {
@@ -668,7 +664,8 @@ abstract class CEGISLike[T <% Typed](name: String) extends Rule(name) {
if (p.pc == BooleanLiteral(true)) {
baseExampleInputs += InExample(p.as.map(a => simplestValue(a.getType)))
} else {
- val solver = sctx.newSolver.setTimeout(exSolverTo)
+ val solverf = sctx.solverFactory
+ val solver = solverf.getNewSolver.setTimeout(exSolverTo)
solver.assertCnstr(p.pc)
@@ -687,7 +684,7 @@ abstract class CEGISLike[T <% Typed](name: String) extends Rule(name) {
return RuleFailed() // This is not necessary though, but probably wanted
}
} finally {
- solver.free()
+ solverf.reclaim(solver)
}
}
@@ -913,8 +910,6 @@ abstract class CEGISLike[T <% Typed](name: String) extends Rule(name) {
sctx.reporter.warning("CEGIS crashed: "+e.getMessage)
e.printStackTrace()
RuleFailed()
- } finally {
- ndProgram.free()
}
}
})
diff --git a/src/main/scala/leon/synthesis/rules/EqualitySplit.scala b/src/main/scala/leon/synthesis/rules/EqualitySplit.scala
index b1653596a..bc62dbba8 100644
--- a/src/main/scala/leon/synthesis/rules/EqualitySplit.scala
+++ b/src/main/scala/leon/synthesis/rules/EqualitySplit.scala
@@ -10,9 +10,11 @@ import purescala.Constructors._
import solvers._
+import scala.concurrent.duration._
+
case object EqualitySplit extends Rule("Eq. Split") {
def instantiateOn(implicit hctx: SearchContext, p: Problem): Traversable[RuleInstantiation] = {
- val solver = SimpleSolverAPI(hctx.sctx.fastSolverFactory)
+ val solver = SimpleSolverAPI(hctx.sctx.solverFactory.withTimeout(50.millis))
val candidates = p.as.groupBy(_.getType).mapValues(_.combinations(2).filter {
case List(a1, a2) =>
diff --git a/src/main/scala/leon/synthesis/rules/InequalitySplit.scala b/src/main/scala/leon/synthesis/rules/InequalitySplit.scala
index 8cc0f2f31..292e99de8 100644
--- a/src/main/scala/leon/synthesis/rules/InequalitySplit.scala
+++ b/src/main/scala/leon/synthesis/rules/InequalitySplit.scala
@@ -10,9 +10,11 @@ import purescala.Constructors._
import solvers._
+import scala.concurrent.duration._
+
case object InequalitySplit extends Rule("Ineq. Split.") {
def instantiateOn(implicit hctx: SearchContext, p: Problem): Traversable[RuleInstantiation] = {
- val solver = SimpleSolverAPI(hctx.sctx.fastSolverFactory)
+ val solver = SimpleSolverAPI(hctx.sctx.solverFactory.withTimeout(50.millis))
val argsPairs = p.as.filter(_.getType == IntegerType).combinations(2) ++
p.as.filter(_.getType == Int32Type).combinations(2)
diff --git a/src/main/scala/leon/synthesis/rules/OptimisticGround.scala b/src/main/scala/leon/synthesis/rules/OptimisticGround.scala
index 423206003..6085ef9eb 100644
--- a/src/main/scala/leon/synthesis/rules/OptimisticGround.scala
+++ b/src/main/scala/leon/synthesis/rules/OptimisticGround.scala
@@ -10,13 +10,15 @@ import purescala.Constructors._
import solvers._
+import scala.concurrent.duration._
+
case object OptimisticGround extends Rule("Optimistic Ground") {
def instantiateOn(implicit hctx: SearchContext, p: Problem): Traversable[RuleInstantiation] = {
if (p.as.nonEmpty && p.xs.nonEmpty) {
val res = new RuleInstantiation(this.name) {
def apply(hctx: SearchContext) = {
- val solver = SimpleSolverAPI(hctx.sctx.fastSolverFactory) // Optimistic ground is given a simple solver (uninterpreted)
+ val solver = SimpleSolverAPI(hctx.sctx.solverFactory.withTimeout(50.millis))
val xss = p.xs.toSet
val ass = p.as.toSet
--
GitLab