From 62b02b74115492eaad08bef24e06cfcf1f1532f1 Mon Sep 17 00:00:00 2001
From: Nicolas Voirol <voirol.nicolas@gmail.com>
Date: Sun, 1 May 2016 18:22:14 +0200
Subject: [PATCH] Solver contexts to propagate evaluation banks in
solver-evaluator alternations
---
src/main/scala/leon/LeonContext.scala | 2 +
.../scala/leon/codegen/runtime/Monitor.scala | 8 ++-
.../scala/leon/evaluators/Evaluator.scala | 65 ++++++++++---------
.../leon/evaluators/RecursiveEvaluator.scala | 8 ++-
.../engine/UnfoldingTemplateSolver.scala | 2 +-
.../templateSolvers/ExtendedUFSolver.scala | 2 +-
.../UniversalQuantificationSolver.scala | 2 +-
.../leon/solvers/EnumerationSolver.scala | 4 +-
.../scala/leon/solvers/EvaluatingSolver.scala | 22 ++-----
.../scala/leon/solvers/GroundSolver.scala | 2 +-
src/main/scala/leon/solvers/Solver.scala | 13 +++-
.../scala/leon/solvers/SolverFactory.scala | 26 ++++----
.../leon/solvers/SolverUnsupportedError.scala | 2 +-
.../solvers/combinators/PortfolioSolver.scala | 10 +--
.../combinators/PortfolioSolverFactory.scala | 5 +-
.../scala/leon/solvers/cvc4/CVC4Solver.scala | 7 ++
.../solvers/cvc4/CVC4UnrollingSolver.scala | 6 +-
.../isabelle/IsabelleEnvironment.scala | 2 +-
.../solvers/isabelle/IsabelleSolver.scala | 2 +-
.../SMTLIBCVC4CounterExampleSolver.scala | 5 +-
.../smtlib/SMTLIBCVC4ProofSolver.scala | 6 +-
.../smtlib/SMTLIBCVC4QuantifiedSolver.scala | 5 +-
.../smtlib/SMTLIBCVC4QuantifiedTarget.scala | 2 +-
.../solvers/smtlib/SMTLIBCVC4Solver.scala | 10 +--
.../solvers/smtlib/SMTLIBCVC4Target.scala | 2 +-
.../leon/solvers/smtlib/SMTLIBSolver.scala | 2 +-
.../leon/solvers/smtlib/SMTLIBTarget.scala | 13 ++--
.../smtlib/SMTLIBZ3QuantifiedSolver.scala | 2 +-
.../smtlib/SMTLIBZ3QuantifiedTarget.scala | 2 +-
.../leon/solvers/smtlib/SMTLIBZ3Solver.scala | 10 ++-
.../leon/solvers/smtlib/SMTLIBZ3Target.scala | 2 +-
.../leon/solvers/sygus/SygusSolver.scala | 4 +-
.../solvers/unrolling/UnrollingSolver.scala | 4 +-
.../leon/solvers/z3/AbstractZ3Solver.scala | 10 +--
.../scala/leon/solvers/z3/FairZ3Solver.scala | 3 +-
.../solvers/z3/UninterpretedZ3Solver.scala | 2 +-
src/main/scala/leon/solvers/z3/Z3Solver.scala | 7 ++
.../leon/solvers/z3/Z3UnrollingSolver.scala | 7 +-
.../solvers/EnumerationSolverSuite.scala | 2 +-
.../solvers/FairZ3SolverTests.scala | 2 +-
.../solvers/GlobalVariablesSuite.scala | 18 ++---
.../solvers/QuantifierSolverSuite.scala | 22 +++----
.../integration/solvers/SolversSuite.scala | 20 ++----
.../solvers/TimeoutSolverSuite.scala | 4 +-
.../solvers/UnrollingSolverSuite.scala | 4 +-
.../leon/unit/solvers/SolverPoolSuite.scala | 4 +-
46 files changed, 181 insertions(+), 183 deletions(-)
create mode 100644 src/main/scala/leon/solvers/cvc4/CVC4Solver.scala
create mode 100644 src/main/scala/leon/solvers/z3/Z3Solver.scala
diff --git a/src/main/scala/leon/LeonContext.scala b/src/main/scala/leon/LeonContext.scala
index f46e53d04..8e0a414f1 100644
--- a/src/main/scala/leon/LeonContext.scala
+++ b/src/main/scala/leon/LeonContext.scala
@@ -27,6 +27,8 @@ case class LeonContext(
def findOptionOrDefault[A: ClassTag](optDef: LeonOptionDef[A]): A =
findOption(optDef).getOrElse(optDef.default)
+
+ def toSctx = solvers.SolverContext(this, new evaluators.EvaluationBank)
}
object LeonContext {
diff --git a/src/main/scala/leon/codegen/runtime/Monitor.scala b/src/main/scala/leon/codegen/runtime/Monitor.scala
index cdab9cc0e..a1323b4e1 100644
--- a/src/main/scala/leon/codegen/runtime/Monitor.scala
+++ b/src/main/scala/leon/codegen/runtime/Monitor.scala
@@ -19,7 +19,7 @@ import scala.collection.immutable.{Map => ScalaMap}
import scala.collection.mutable.{HashMap => MutableMap, Set => MutableSet}
import scala.concurrent.duration._
-import solvers.SolverFactory
+import solvers.{SolverContext, SolverFactory}
import solvers.unrolling.UnrollingProcedure
import evaluators._
@@ -138,7 +138,8 @@ class StdMonitor(unit: CompilationUnit, invocationsMax: Int, bodies: ScalaMap[Id
} else {
val tStart = System.currentTimeMillis
- val solverf = SolverFactory.getEvalSolver(ctx, program, unit.bank).withTimeout(10.second)
+ val sctx = SolverContext(ctx, unit.bank)
+ val solverf = SolverFactory.getFromSettings(sctx, program).withTimeout(10.second)
val solver = solverf.getNewSolver()
val newTypes = tps.toSeq.map(unit.runtimeIdToTypeMap(_))
@@ -223,7 +224,8 @@ class StdMonitor(unit: CompilationUnit, invocationsMax: Int, bodies: ScalaMap[Id
} else {
val tStart = System.currentTimeMillis
- val solverf = SolverFactory.getEvalSolver(ctx, program, unit.bank).withTimeout(.5.second)
+ val sctx = SolverContext(ctx, unit.bank)
+ val solverf = SolverFactory.getFromSettings(sctx, program).withTimeout(.5.second)
val solver = solverf.getNewSolver()
val newTypes = tps.toSeq.map(unit.runtimeIdToTypeMap(_))
diff --git a/src/main/scala/leon/evaluators/Evaluator.scala b/src/main/scala/leon/evaluators/Evaluator.scala
index de666f389..3cc47bdd6 100644
--- a/src/main/scala/leon/evaluators/Evaluator.scala
+++ b/src/main/scala/leon/evaluators/Evaluator.scala
@@ -109,8 +109,37 @@ trait NDEvaluator extends Evaluator {
type Value = Stream[Expr]
}
-class EvaluationBank {
+/* Status of invariant checking
+ *
+ * For a given invariant, its checking status can be either
+ * - Complete(success) : checking has been performed previously and
+ * resulted in a value of `success`.
+ * - Pending : invariant is currently being checked somewhere
+ * in the program. If it fails, the failure is
+ * assumed to be bubbled up to all relevant failure
+ * points.
+ * - NoCheck : invariant has never been seen before. Discovering
+ * NoCheck for an invariant will automatically update
+ * the status to `Pending` as this creates a checking
+ * obligation.
+ */
+sealed abstract class CheckStatus {
+ /* The invariant was invalid and this particular case class can't exist */
+ def isFailure: Boolean = this match {
+ case Complete(status) => !status
+ case _ => false
+ }
+
+ /* The invariant has never been checked before and the checking obligation
+ * therefore falls onto the first caller of this method. */
+ def isRequired: Boolean = this == NoCheck
+}
+case class Complete(success: Boolean) extends CheckStatus
+case object Pending extends CheckStatus
+case object NoCheck extends CheckStatus
+
+class EvaluationBank private(
/* Shared set that tracks checked case-class invariants
*
* Checking case-class invariants can require invoking a solver
@@ -126,37 +155,9 @@ class EvaluationBank {
* determine whether the invariant of a given case
* class should be checked.
*/
- private val checkCache: MutableMap[CaseClass, CheckStatus] = MutableMap.empty
+ checkCache: MutableMap[CaseClass, CheckStatus]) {
- /* Status of invariant checking
- *
- * For a given invariant, its checking status can be either
- * - Complete(success) : checking has been performed previously and
- * resulted in a value of `success`.
- * - Pending : invariant is currently being checked somewhere
- * in the program. If it fails, the failure is
- * assumed to be bubbled up to all relevant failure
- * points.
- * - NoCheck : invariant has never been seen before. Discovering
- * NoCheck for an invariant will automatically update
- * the status to `Pending` as this creates a checking
- * obligation.
- */
- sealed abstract class CheckStatus {
- /* The invariant was invalid and this particular case class can't exist */
- def isFailure: Boolean = this match {
- case Complete(status) => !status
- case _ => false
- }
-
- /* The invariant has never been checked before and the checking obligation
- * therefore falls onto the first caller of this method. */
- def isRequired: Boolean = this == NoCheck
- }
-
- case class Complete(success: Boolean) extends CheckStatus
- case object Pending extends CheckStatus
- case object NoCheck extends CheckStatus
+ def this() = this(MutableMap.empty)
/* Status of the invariant checking for `cc` */
def invariantCheck(cc: CaseClass): CheckStatus = synchronized {
@@ -171,4 +172,6 @@ class EvaluationBank {
def invariantResult(cc: CaseClass, success: Boolean): Unit = synchronized {
checkCache(cc) = Complete(success)
}
+
+ override def clone: EvaluationBank = new EvaluationBank(checkCache.clone)
}
diff --git a/src/main/scala/leon/evaluators/RecursiveEvaluator.scala b/src/main/scala/leon/evaluators/RecursiveEvaluator.scala
index db18be70e..41b86de7c 100644
--- a/src/main/scala/leon/evaluators/RecursiveEvaluator.scala
+++ b/src/main/scala/leon/evaluators/RecursiveEvaluator.scala
@@ -14,7 +14,7 @@ import purescala.Common._
import purescala.Expressions._
import purescala.Definitions._
import purescala.DefOps
-import solvers.{PartialModel, Model, SolverFactory}
+import solvers.{PartialModel, Model, SolverFactory, SolverContext}
import solvers.unrolling.UnrollingProcedure
import scala.collection.mutable.{Map => MutableMap}
import scala.concurrent.duration._
@@ -618,7 +618,8 @@ abstract class RecursiveEvaluator(ctx: LeonContext, prog: Program, val bank: Eva
newOptions.exists(no => opt.optionDef == no.optionDef)
} ++ newOptions)
- val solverf = SolverFactory.getEvalSolver(newCtx, program, bank).withTimeout(1.second)
+ val sctx = SolverContext(newCtx, bank)
+ val solverf = SolverFactory.getFromSettings(sctx, program).withTimeout(1.second)
val solver = solverf.getNewSolver()
try {
@@ -749,7 +750,8 @@ abstract class RecursiveEvaluator(ctx: LeonContext, prog: Program, val bank: Eva
clpCache.getOrElse((choose, ins), {
val tStart = System.currentTimeMillis
- val solverf = SolverFactory.getFromSettings(ctx, program)
+ val sctx = SolverContext(ctx, bank)
+ val solverf = SolverFactory.getFromSettings(sctx, program)
val solver = solverf.getNewSolver()
try {
diff --git a/src/main/scala/leon/invariant/engine/UnfoldingTemplateSolver.scala b/src/main/scala/leon/invariant/engine/UnfoldingTemplateSolver.scala
index 45316adff..336b79603 100644
--- a/src/main/scala/leon/invariant/engine/UnfoldingTemplateSolver.scala
+++ b/src/main/scala/leon/invariant/engine/UnfoldingTemplateSolver.scala
@@ -193,7 +193,7 @@ class UnfoldingTemplateSolver(ctx: InferenceContext, program: Program, rootFd: F
import leon.solvers.unrolling.UnrollingSolver
def solveUsingLeon(leonctx: LeonContext, p: Program, vc: VC) = {
val solFactory = SolverFactory.uninterpreted(leonctx, program)
- val smtUnrollZ3 = new UnrollingSolver(ctx.leonContext, program, solFactory.getNewSolver()) with TimeoutSolver
+ val smtUnrollZ3 = new UnrollingSolver(ctx.leonContext.toSctx, program, solFactory.getNewSolver()) with TimeoutSolver
smtUnrollZ3.setTimeout(ctx.vcTimeout * 1000)
smtUnrollZ3.assertVC(vc)
smtUnrollZ3.check match {
diff --git a/src/main/scala/leon/invariant/templateSolvers/ExtendedUFSolver.scala b/src/main/scala/leon/invariant/templateSolvers/ExtendedUFSolver.scala
index f81d340c7..8902564de 100644
--- a/src/main/scala/leon/invariant/templateSolvers/ExtendedUFSolver.scala
+++ b/src/main/scala/leon/invariant/templateSolvers/ExtendedUFSolver.scala
@@ -13,7 +13,7 @@ import leon.solvers.z3.UninterpretedZ3Solver
* TODO: need to handle bit vectors
*/
class ExtendedUFSolver(context: LeonContext, program: Program)
- extends UninterpretedZ3Solver(context, program) {
+ extends UninterpretedZ3Solver(context.toSctx, program) {
override val name = "Z3-eu"
override val description = "Extended UF-ADT Z3 Solver"
diff --git a/src/main/scala/leon/invariant/templateSolvers/UniversalQuantificationSolver.scala b/src/main/scala/leon/invariant/templateSolvers/UniversalQuantificationSolver.scala
index 3e40886a5..db02d58c0 100644
--- a/src/main/scala/leon/invariant/templateSolvers/UniversalQuantificationSolver.scala
+++ b/src/main/scala/leon/invariant/templateSolvers/UniversalQuantificationSolver.scala
@@ -63,7 +63,7 @@ class UniversalQuantificationSolver(ctx: InferenceContext, program: Program,
if (usePortfolio) {
if (useIncrementalSolvingForVCs)
throw new IllegalArgumentException("Cannot perform incremental solving with portfolio solvers!")
- new PortfolioSolverFactory(leonctx, Seq(
+ new PortfolioSolverFactory(leonctx.toSctx, Seq(
SolverFactory.getFromName(leonctx, program)("smt-cvc4-u"),
SolverFactory.getFromName(leonctx, program)("smt-z3-u")))
} else
diff --git a/src/main/scala/leon/solvers/EnumerationSolver.scala b/src/main/scala/leon/solvers/EnumerationSolver.scala
index 79f53ef91..86a3a91f0 100644
--- a/src/main/scala/leon/solvers/EnumerationSolver.scala
+++ b/src/main/scala/leon/solvers/EnumerationSolver.scala
@@ -12,7 +12,7 @@ import purescala.ExprOps._
import datagen._
-class EnumerationSolver(val context: LeonContext, val program: Program) extends Solver with NaiveAssumptionSolver {
+class EnumerationSolver(val sctx: SolverContext, val program: Program) extends Solver with NaiveAssumptionSolver {
def name = "Enum"
val maxTried = 10000
@@ -52,7 +52,7 @@ class EnumerationSolver(val context: LeonContext, val program: Program) extends
def check: Option[Boolean] = {
val timer = context.timers.solvers.enum.check.start()
val res = try {
- datagen = Some(new VanuatooDataGen(context, program))
+ datagen = Some(new VanuatooDataGen(context, program, sctx.bank))
if (interrupted) {
None
} else {
diff --git a/src/main/scala/leon/solvers/EvaluatingSolver.scala b/src/main/scala/leon/solvers/EvaluatingSolver.scala
index 0930478d8..292ef1605 100644
--- a/src/main/scala/leon/solvers/EvaluatingSolver.scala
+++ b/src/main/scala/leon/solvers/EvaluatingSolver.scala
@@ -7,28 +7,14 @@ import purescala.Definitions._
import evaluators._
trait EvaluatingSolver extends Solver {
- val context: LeonContext
val program: Program
val useCodeGen: Boolean
- private var _bank: EvaluationBank = new EvaluationBank
- private var _evaluator: DeterministicEvaluator = _
-
- def evaluator: DeterministicEvaluator = {
- if (_evaluator eq null) _evaluator = if (useCodeGen) {
- new CodeGenEvaluator(context, program, bank)
- } else {
- new DefaultEvaluator(context, program, bank)
- }
- _evaluator
- }
-
- def bank: EvaluationBank = _bank
- def setBank(bank: EvaluationBank): this.type = {
- _bank = bank
- _evaluator = null
- this
+ val evaluator: DeterministicEvaluator = if (useCodeGen) {
+ new CodeGenEvaluator(context, program, sctx.bank)
+ } else {
+ new DefaultEvaluator(context, program, sctx.bank)
}
}
diff --git a/src/main/scala/leon/solvers/GroundSolver.scala b/src/main/scala/leon/solvers/GroundSolver.scala
index 130f8d86b..a50b3f814 100644
--- a/src/main/scala/leon/solvers/GroundSolver.scala
+++ b/src/main/scala/leon/solvers/GroundSolver.scala
@@ -14,7 +14,7 @@ import utils.Interruptible
import utils.IncrementalSeq
// This solver only "solves" ground terms by evaluating them
-class GroundSolver(val context: LeonContext, val program: Program) extends Solver with NaiveAssumptionSolver {
+class GroundSolver(val sctx: SolverContext, val program: Program) extends Solver with NaiveAssumptionSolver {
context.interruptManager.registerForInterrupts(this)
diff --git a/src/main/scala/leon/solvers/Solver.scala b/src/main/scala/leon/solvers/Solver.scala
index e1c9525ae..935274abf 100644
--- a/src/main/scala/leon/solvers/Solver.scala
+++ b/src/main/scala/leon/solvers/Solver.scala
@@ -7,12 +7,19 @@ import leon.utils.{DebugSectionSolver, Interruptible}
import purescala.Expressions._
import purescala.Common.Tree
import verification.VC
+import evaluators._
+
+case class SolverContext(context: LeonContext, bank: EvaluationBank) {
+ lazy val reporter = context.reporter
+ override def clone = SolverContext(context, bank.clone)
+}
trait Solver extends Interruptible {
def name: String
- val context: LeonContext
+ val sctx: SolverContext
- implicit lazy val leonContext = context
+ implicit lazy val context = sctx.context
+ lazy val reporter = sctx.reporter
// This is ugly, but helpful for smtlib solvers
def dbg(msg: => Any) {}
@@ -41,7 +48,7 @@ trait Solver extends Interruptible {
protected def unsupported(t: Tree): Nothing = {
val err = SolverUnsupportedError(t, this, None)
- leonContext.reporter.warning(err.getMessage)
+ context.reporter.warning(err.getMessage)
throw err
}
diff --git a/src/main/scala/leon/solvers/SolverFactory.scala b/src/main/scala/leon/solvers/SolverFactory.scala
index bf7e392a7..59d9859fb 100644
--- a/src/main/scala/leon/solvers/SolverFactory.scala
+++ b/src/main/scala/leon/solvers/SolverFactory.scala
@@ -51,8 +51,11 @@ object SolverFactory {
case (name, desc) => f"\n $name%-14s : $desc"
}.mkString("")
- def getFromSettings(implicit ctx: LeonContext, program: Program): SolverFactory[TimeoutSolver] = {
- val names = ctx.findOptionOrDefault(GlobalOptions.optSelectedSolvers)
+ def getFromSettings(implicit ctx: LeonContext, program: Program): SolverFactory[TimeoutSolver] =
+ getFromSettings(SolverContext(ctx, new evaluators.EvaluationBank), program)
+
+ def getFromSettings(implicit ctx: SolverContext, program: Program): SolverFactory[TimeoutSolver] = {
+ val names = ctx.context.findOptionOrDefault(GlobalOptions.optSelectedSolvers)
if (((names contains "fairz3") || (names contains "unrollz3")) && !hasNativeZ3) {
if (hasZ3) {
@@ -75,20 +78,15 @@ object SolverFactory {
}
}
- def getEvalSolver(ctx: LeonContext, program: Program, bank: evaluators.EvaluationBank): SolverFactory[EvaluatingSolver with TimeoutSolver] = {
- val factory = getFromSettings(ctx, program)
- SolverFactory(factory.name, () => factory.getNewSolver() match {
- case ev: EvaluatingSolver => ev.setBank(bank)
- case s => ctx.reporter.fatalError("Cannot use non-evaluating solver " + s + " for evaluation")
- })
- }
-
- private def showSolvers(ctx: LeonContext) = {
+ private def showSolvers(ctx: SolverContext) = {
ctx.reporter.error(availableSolversPretty)
ctx.reporter.fatalError("Aborting Leon...")
}
- def getFromName(ctx: LeonContext, program: Program)(name: String): SolverFactory[TimeoutSolver] = name match {
+ def getFromName(ctx: LeonContext, program: Program)(name: String): SolverFactory[TimeoutSolver] =
+ getFromName(SolverContext(ctx, new evaluators.EvaluationBank), program)(name)
+
+ def getFromName(ctx: SolverContext, program: Program)(name: String): SolverFactory[TimeoutSolver] = name match {
case "enum" => SolverFactory(name, () => new EnumerationSolver(ctx, program) with TimeoutSolver)
case "ground" => SolverFactory(name, () => new GroundSolver(ctx, program) with TimeoutSolver)
case "fairz3" => SolverFactory(name, () => new FairZ3Solver(ctx, program) with TimeoutSolver)
@@ -101,13 +99,13 @@ object SolverFactory {
case "smt-z3-u" => SolverFactory(name, () => new SMTLIBZ3Solver(ctx, program) with TimeoutSolver)
case "smt-cvc4-u" => SolverFactory(name, () => new SMTLIBCVC4Solver(ctx, program) with TimeoutSolver)
case "nativez3-u" => SolverFactory(name, () => new UninterpretedZ3Solver(ctx, program) with TimeoutSolver)
- case "isabelle" => new isabelle.IsabelleSolverFactory(ctx, program)
+ case "isabelle" => new isabelle.IsabelleSolverFactory(ctx.context, program)
case _ =>
ctx.reporter.error(s"Unknown solver $name")
showSolvers(ctx)
}
- def getFromNames(ctx: LeonContext, program: Program)(names: String*): SolverFactory[TimeoutSolver] = {
+ def getFromNames(ctx: SolverContext, program: Program)(names: String*): SolverFactory[TimeoutSolver] = {
val selectedSolvers = names.map(getFromName(ctx, program))
diff --git a/src/main/scala/leon/solvers/SolverUnsupportedError.scala b/src/main/scala/leon/solvers/SolverUnsupportedError.scala
index 8d42223c8..48acc71f4 100644
--- a/src/main/scala/leon/solvers/SolverUnsupportedError.scala
+++ b/src/main/scala/leon/solvers/SolverUnsupportedError.scala
@@ -12,4 +12,4 @@ object SolverUnsupportedError {
}
case class SolverUnsupportedError(t: Tree, s: Solver, reason: Option[String] = None)
- extends Unsupported(t, SolverUnsupportedError.msg(t,s,reason))(s.leonContext)
+ extends Unsupported(t, SolverUnsupportedError.msg(t,s,reason))(s.context)
diff --git a/src/main/scala/leon/solvers/combinators/PortfolioSolver.scala b/src/main/scala/leon/solvers/combinators/PortfolioSolver.scala
index f374344e5..1a942fd42 100644
--- a/src/main/scala/leon/solvers/combinators/PortfolioSolver.scala
+++ b/src/main/scala/leon/solvers/combinators/PortfolioSolver.scala
@@ -13,7 +13,7 @@ import scala.concurrent.duration._
import ExecutionContext.Implicits.global
-class PortfolioSolver[S <: Solver with Interruptible](val context: LeonContext, val solvers: Seq[S])
+class PortfolioSolver[S <: Solver with Interruptible](val sctx: SolverContext, val solvers: Seq[S])
extends Solver with NaiveAssumptionSolver {
val name = "Pfolio"
@@ -36,7 +36,7 @@ class PortfolioSolver[S <: Solver with Interruptible](val context: LeonContext,
def check: Option[Boolean] = {
model = Model.empty
- context.reporter.debug("Running portfolio check")
+ reporter.debug("Running portfolio check")
// solving
val fs = solvers.map { s =>
Future {
@@ -50,7 +50,7 @@ class PortfolioSolver[S <: Solver with Interruptible](val context: LeonContext,
(s, result, model)
} catch {
case _: StackOverflowError =>
- context.reporter.warning("Stack Overflow while running solver.check()!")
+ reporter.warning("Stack Overflow while running solver.check()!")
(s, None, Model.empty)
}
}
@@ -63,12 +63,12 @@ class PortfolioSolver[S <: Solver with Interruptible](val context: LeonContext,
model = m
resultSolver = s.getResultSolver
resultSolver.foreach { solv =>
- context.reporter.debug("Solved with "+solv)
+ reporter.debug("Solved with "+solv)
}
solvers.foreach(_.interrupt())
r
case None =>
- context.reporter.debug("No solver succeeded")
+ reporter.debug("No solver succeeded")
//fs.foreach(f => println(f.value))
None
}
diff --git a/src/main/scala/leon/solvers/combinators/PortfolioSolverFactory.scala b/src/main/scala/leon/solvers/combinators/PortfolioSolverFactory.scala
index d5027a440..2c5f8df14 100644
--- a/src/main/scala/leon/solvers/combinators/PortfolioSolverFactory.scala
+++ b/src/main/scala/leon/solvers/combinators/PortfolioSolverFactory.scala
@@ -6,7 +6,8 @@ package combinators
import scala.reflect.runtime.universe._
-class PortfolioSolverFactory[S <: Solver](ctx: LeonContext, sfs: Seq[SolverFactory[S]]) extends SolverFactory[PortfolioSolver[S] with TimeoutSolver] {
+class PortfolioSolverFactory[S <: Solver](ctx: SolverContext, sfs: Seq[SolverFactory[S]])
+ extends SolverFactory[PortfolioSolver[S] with TimeoutSolver] {
def getNewSolver(): PortfolioSolver[S] with TimeoutSolver = {
new PortfolioSolver[S](ctx, sfs.map(_.getNewSolver())) with TimeoutSolver
@@ -19,7 +20,7 @@ class PortfolioSolverFactory[S <: Solver](ctx: LeonContext, sfs: Seq[SolverFacto
}
case _ =>
- ctx.reporter.error("Failed to reclaim a non-portfolio solver.")
+ ctx.context.reporter.error("Failed to reclaim a non-portfolio solver.")
}
val name = sfs.map(_.name).mkString("Pfolio(", ",", ")")
diff --git a/src/main/scala/leon/solvers/cvc4/CVC4Solver.scala b/src/main/scala/leon/solvers/cvc4/CVC4Solver.scala
new file mode 100644
index 000000000..ff112d792
--- /dev/null
+++ b/src/main/scala/leon/solvers/cvc4/CVC4Solver.scala
@@ -0,0 +1,7 @@
+/* Copyright 2009-2016 EPFL, Lausanne */
+
+package leon
+package solvers
+package cvc4
+
+trait CVC4Solver extends Solver
diff --git a/src/main/scala/leon/solvers/cvc4/CVC4UnrollingSolver.scala b/src/main/scala/leon/solvers/cvc4/CVC4UnrollingSolver.scala
index 97b5d4dc9..b293abbe2 100644
--- a/src/main/scala/leon/solvers/cvc4/CVC4UnrollingSolver.scala
+++ b/src/main/scala/leon/solvers/cvc4/CVC4UnrollingSolver.scala
@@ -9,5 +9,7 @@ import purescala.Definitions._
import unrolling._
import theories._
-class CVC4UnrollingSolver(context: LeonContext, program: Program, underlying: Solver)
- extends UnrollingSolver(context, program, underlying, theories = new BagEncoder(context, program))
+class CVC4UnrollingSolver(context: SolverContext, program: Program, underlying: CVC4Solver)
+ extends UnrollingSolver(context, program, underlying,
+ theories = new BagEncoder(context.context, program))
+ with CVC4Solver
diff --git a/src/main/scala/leon/solvers/isabelle/IsabelleEnvironment.scala b/src/main/scala/leon/solvers/isabelle/IsabelleEnvironment.scala
index 8623bd014..6b3346152 100644
--- a/src/main/scala/leon/solvers/isabelle/IsabelleEnvironment.scala
+++ b/src/main/scala/leon/solvers/isabelle/IsabelleEnvironment.scala
@@ -152,5 +152,5 @@ final class IsabelleEnvironment private(
val selectedFunDefs: List[FunDef]
) {
def solver: IsabelleSolver with TimeoutSolver =
- new IsabelleSolver(context, program, types, functions, system) with TimeoutSolver
+ new IsabelleSolver(context.toSctx, program, types, functions, system) with TimeoutSolver
}
diff --git a/src/main/scala/leon/solvers/isabelle/IsabelleSolver.scala b/src/main/scala/leon/solvers/isabelle/IsabelleSolver.scala
index a6b52a321..b1895380c 100644
--- a/src/main/scala/leon/solvers/isabelle/IsabelleSolver.scala
+++ b/src/main/scala/leon/solvers/isabelle/IsabelleSolver.scala
@@ -18,7 +18,7 @@ import leon.verification.VC
import edu.tum.cs.isabelle._
import edu.tum.cs.isabelle.pure.{Expr => _, _}
-class IsabelleSolver(val context: LeonContext, program: Program, types: Types, functions: Functions, system: System) extends Solver with Interruptible { self: TimeoutSolver =>
+class IsabelleSolver(val sctx: SolverContext, program: Program, types: Types, functions: Functions, system: System) extends Solver with Interruptible { self: TimeoutSolver =>
context.interruptManager.registerForInterrupts(this)
diff --git a/src/main/scala/leon/solvers/smtlib/SMTLIBCVC4CounterExampleSolver.scala b/src/main/scala/leon/solvers/smtlib/SMTLIBCVC4CounterExampleSolver.scala
index 973546c68..ff27a312f 100644
--- a/src/main/scala/leon/solvers/smtlib/SMTLIBCVC4CounterExampleSolver.scala
+++ b/src/main/scala/leon/solvers/smtlib/SMTLIBCVC4CounterExampleSolver.scala
@@ -1,11 +1,12 @@
/* Copyright 2009-2016 EPFL, Lausanne */
package leon
-package solvers.smtlib
+package solvers
+package smtlib
import purescala.Definitions.Program
-class SMTLIBCVC4CounterExampleSolver(context: LeonContext, program: Program) extends SMTLIBCVC4QuantifiedSolver(context, program) {
+class SMTLIBCVC4CounterExampleSolver(context: SolverContext, program: Program) extends SMTLIBCVC4QuantifiedSolver(context, program) {
override def targetName = "cvc4-cex"
diff --git a/src/main/scala/leon/solvers/smtlib/SMTLIBCVC4ProofSolver.scala b/src/main/scala/leon/solvers/smtlib/SMTLIBCVC4ProofSolver.scala
index 8c16d013f..ce6b963ba 100644
--- a/src/main/scala/leon/solvers/smtlib/SMTLIBCVC4ProofSolver.scala
+++ b/src/main/scala/leon/solvers/smtlib/SMTLIBCVC4ProofSolver.scala
@@ -1,7 +1,8 @@
/* Copyright 2009-2016 EPFL, Lausanne */
package leon
-package solvers.smtlib
+package solvers
+package smtlib
import purescala.Definitions.Program
import purescala.Expressions.Expr
@@ -9,7 +10,8 @@ import purescala.Expressions.Expr
import _root_.smtlib.parser.Commands.{Assert => SMTAssert}
import _root_.smtlib.parser.Terms.{Exists => SMTExists}
-class SMTLIBCVC4ProofSolver(context: LeonContext, program: Program) extends SMTLIBCVC4QuantifiedSolver(context, program) {
+class SMTLIBCVC4ProofSolver(context: SolverContext, program: Program)
+ extends SMTLIBCVC4QuantifiedSolver(context, program) {
override def targetName = "cvc4-proof"
diff --git a/src/main/scala/leon/solvers/smtlib/SMTLIBCVC4QuantifiedSolver.scala b/src/main/scala/leon/solvers/smtlib/SMTLIBCVC4QuantifiedSolver.scala
index 39d83d7c7..867686704 100644
--- a/src/main/scala/leon/solvers/smtlib/SMTLIBCVC4QuantifiedSolver.scala
+++ b/src/main/scala/leon/solvers/smtlib/SMTLIBCVC4QuantifiedSolver.scala
@@ -1,13 +1,14 @@
/* Copyright 2009-2016 EPFL, Lausanne */
package leon
-package solvers.smtlib
+package solvers
+package smtlib
import purescala.Definitions.Program
// This solver utilizes the define-funs-rec command of SMTLIB-2.5 to define mutually recursive functions.
// It is not meant as an underlying solver to UnrollingSolver, and does not handle HOFs.
-abstract class SMTLIBCVC4QuantifiedSolver(context: LeonContext, program: Program)
+abstract class SMTLIBCVC4QuantifiedSolver(context: SolverContext, program: Program)
extends SMTLIBCVC4Solver(context, program)
with SMTLIBQuantifiedSolver
with SMTLIBCVC4QuantifiedTarget
diff --git a/src/main/scala/leon/solvers/smtlib/SMTLIBCVC4QuantifiedTarget.scala b/src/main/scala/leon/solvers/smtlib/SMTLIBCVC4QuantifiedTarget.scala
index b67140f4b..8b5fd705b 100644
--- a/src/main/scala/leon/solvers/smtlib/SMTLIBCVC4QuantifiedTarget.scala
+++ b/src/main/scala/leon/solvers/smtlib/SMTLIBCVC4QuantifiedTarget.scala
@@ -22,7 +22,7 @@ trait SMTLIBCVC4QuantifiedTarget extends SMTLIBCVC4Target with SMTLIBQuantifiedT
val (funs, exploredAll) = typedTransitiveCallees(Set(tfd), Some(typedFunDefExplorationLimit))
if (!exploredAll) {
- reporter.warning(
+ context.reporter.warning(
"Did not manage to explore the space of typed functions " +
s"transitively called from ${tfd.id}. The solver may fail"
)
diff --git a/src/main/scala/leon/solvers/smtlib/SMTLIBCVC4Solver.scala b/src/main/scala/leon/solvers/smtlib/SMTLIBCVC4Solver.scala
index 8838ae8ff..f8c36a527 100644
--- a/src/main/scala/leon/solvers/smtlib/SMTLIBCVC4Solver.scala
+++ b/src/main/scala/leon/solvers/smtlib/SMTLIBCVC4Solver.scala
@@ -1,16 +1,18 @@
/* Copyright 2009-2016 EPFL, Lausanne */
package leon
-package solvers.smtlib
+package solvers
+package smtlib
import OptionParsers._
import solvers.theories._
import purescala.Definitions.Program
-class SMTLIBCVC4Solver(context: LeonContext, program: Program)
- extends SMTLIBSolver(context, program, new BagEncoder(context, program))
- with SMTLIBCVC4Target {
+class SMTLIBCVC4Solver(context: SolverContext, program: Program)
+ extends SMTLIBSolver(context, program, new BagEncoder(context.context, program))
+ with SMTLIBCVC4Target
+ with cvc4.CVC4Solver {
def targetName = "cvc4"
diff --git a/src/main/scala/leon/solvers/smtlib/SMTLIBCVC4Target.scala b/src/main/scala/leon/solvers/smtlib/SMTLIBCVC4Target.scala
index 30ae22f98..04763b1b5 100644
--- a/src/main/scala/leon/solvers/smtlib/SMTLIBCVC4Target.scala
+++ b/src/main/scala/leon/solvers/smtlib/SMTLIBCVC4Target.scala
@@ -20,7 +20,7 @@ trait SMTLIBCVC4Target extends SMTLIBTarget {
override def getNewInterpreter(ctx: LeonContext) = {
val opts = interpreterOps(ctx)
- reporter.debug("Invoking solver with "+opts.mkString(" "))
+ context.reporter.debug("Invoking solver with "+opts.mkString(" "))
new CVC4Interpreter("cvc4", opts.toArray)
}
diff --git a/src/main/scala/leon/solvers/smtlib/SMTLIBSolver.scala b/src/main/scala/leon/solvers/smtlib/SMTLIBSolver.scala
index 9f6f92b93..346889d30 100644
--- a/src/main/scala/leon/solvers/smtlib/SMTLIBSolver.scala
+++ b/src/main/scala/leon/solvers/smtlib/SMTLIBSolver.scala
@@ -16,7 +16,7 @@ import _root_.smtlib.parser.CommandsResponses.{Error => ErrorResponse, _}
import theories._
import utils._
-abstract class SMTLIBSolver(val context: LeonContext, val program: Program, theories: TheoryEncoder)
+abstract class SMTLIBSolver(val sctx: SolverContext, val program: Program, theories: TheoryEncoder)
extends Solver with SMTLIBTarget with NaiveAssumptionSolver {
/* Solver name */
diff --git a/src/main/scala/leon/solvers/smtlib/SMTLIBTarget.scala b/src/main/scala/leon/solvers/smtlib/SMTLIBTarget.scala
index cd7eae5e8..87d798528 100644
--- a/src/main/scala/leon/solvers/smtlib/SMTLIBTarget.scala
+++ b/src/main/scala/leon/solvers/smtlib/SMTLIBTarget.scala
@@ -38,7 +38,6 @@ import _root_.smtlib.interpreters.ProcessInterpreter
trait SMTLIBTarget extends Interruptible {
val context: LeonContext
val program: Program
- protected def reporter = context.reporter
def targetName: String
@@ -73,7 +72,7 @@ trait SMTLIBTarget extends Interruptible {
/* Printing VCs */
protected lazy val debugOut: Option[java.io.FileWriter] = {
- if (reporter.isDebugEnabled) {
+ if (context.reporter.isDebugEnabled) {
val file = context.files.headOption.map(_.getName).getOrElse("NA")
val n = DebugFileNumbers.next(targetName + file)
@@ -82,7 +81,7 @@ trait SMTLIBTarget extends Interruptible {
val javaFile = new java.io.File(fileName)
javaFile.getParentFile.mkdirs()
- reporter.debug(s"Outputting smt session into $fileName")
+ context.reporter.debug(s"Outputting smt session into $fileName")
val fw = new java.io.FileWriter(javaFile, false)
@@ -103,7 +102,7 @@ trait SMTLIBTarget extends Interruptible {
}
interpreter.eval(cmd) match {
case err @ ErrorResponse(msg) if !hasError && !interrupted && !rawOut =>
- reporter.warning(s"Unexpected error from $targetName solver: $msg")
+ context.reporter.warning(s"Unexpected error from $targetName solver: $msg")
//println(Thread.currentThread().getStackTrace.map(_.toString).take(10).mkString("\n"))
// Store that there was an error. Now all following check()
// invocations will return None
@@ -117,7 +116,7 @@ trait SMTLIBTarget extends Interruptible {
def parseSuccess() = {
val res = interpreter.parser.parseGenResponse
if (res != Success) {
- reporter.warning("Unnexpected result from " + targetName + ": " + res + " expected success")
+ context.reporter.warning("Unnexpected result from " + targetName + ": " + res + " expected success")
}
}
@@ -895,7 +894,7 @@ trait SMTLIBTarget extends Interruptible {
Equals(ra, fromSMT(b, ra.getType))
case _ =>
- reporter.fatalError("Function " + app + " not handled in fromSMT: " + s)
+ context.reporter.fatalError("Function " + app + " not handled in fromSMT: " + s)
}
case (Core.True(), Some(BooleanType)) => BooleanLiteral(true)
@@ -910,7 +909,7 @@ trait SMTLIBTarget extends Interruptible {
}
case _ =>
- reporter.fatalError(s"Unhandled case in fromSMT: $t : ${otpe.map(_.asString(context)).getOrElse("?")} (${t.getClass})")
+ context.reporter.fatalError(s"Unhandled case in fromSMT: $t : ${otpe.map(_.asString(context)).getOrElse("?")} (${t.getClass})")
}
}
diff --git a/src/main/scala/leon/solvers/smtlib/SMTLIBZ3QuantifiedSolver.scala b/src/main/scala/leon/solvers/smtlib/SMTLIBZ3QuantifiedSolver.scala
index 0be498f13..7dd3e4be7 100644
--- a/src/main/scala/leon/solvers/smtlib/SMTLIBZ3QuantifiedSolver.scala
+++ b/src/main/scala/leon/solvers/smtlib/SMTLIBZ3QuantifiedSolver.scala
@@ -12,7 +12,7 @@ import theories._
* This solver models function definitions as universally quantified formulas.
* It is not meant as an underlying solver to UnrollingSolver, and does not handle HOFs.
*/
-class SMTLIBZ3QuantifiedSolver(context: LeonContext, program: Program)
+class SMTLIBZ3QuantifiedSolver(context: SolverContext, program: Program)
extends SMTLIBZ3Solver(context, program)
with SMTLIBQuantifiedSolver
with SMTLIBZ3QuantifiedTarget
diff --git a/src/main/scala/leon/solvers/smtlib/SMTLIBZ3QuantifiedTarget.scala b/src/main/scala/leon/solvers/smtlib/SMTLIBZ3QuantifiedTarget.scala
index f355392d0..9b696cea0 100644
--- a/src/main/scala/leon/solvers/smtlib/SMTLIBZ3QuantifiedTarget.scala
+++ b/src/main/scala/leon/solvers/smtlib/SMTLIBZ3QuantifiedTarget.scala
@@ -23,7 +23,7 @@ trait SMTLIBZ3QuantifiedTarget extends SMTLIBZ3Target with SMTLIBQuantifiedTarge
val (funs, exploredAll) = typedTransitiveCallees(Set(tfd), Some(typedFunDefExplorationLimit))
if (!exploredAll) {
- reporter.warning(
+ context.reporter.warning(
"Did not manage to explore the space of typed functions " +
s"transitively called from ${tfd.id}. The solver may fail"
)
diff --git a/src/main/scala/leon/solvers/smtlib/SMTLIBZ3Solver.scala b/src/main/scala/leon/solvers/smtlib/SMTLIBZ3Solver.scala
index 43c1643cf..019eea370 100644
--- a/src/main/scala/leon/solvers/smtlib/SMTLIBZ3Solver.scala
+++ b/src/main/scala/leon/solvers/smtlib/SMTLIBZ3Solver.scala
@@ -15,9 +15,7 @@ import _root_.smtlib.theories.Core.{Equals => _, _}
import theories._
-class SMTLIBZ3Solver(context: LeonContext, program: Program)
- extends SMTLIBSolver(context, program, new StringEncoder(context, program))
- with SMTLIBZ3Target {
-
- def getProgram: Program = program
-}
+class SMTLIBZ3Solver(sctx: SolverContext, program: Program)
+ extends SMTLIBSolver(sctx, program, new StringEncoder(sctx.context, program))
+ with SMTLIBZ3Target
+ with z3.Z3Solver
diff --git a/src/main/scala/leon/solvers/smtlib/SMTLIBZ3Target.scala b/src/main/scala/leon/solvers/smtlib/SMTLIBZ3Target.scala
index 00b361323..52894a29c 100644
--- a/src/main/scala/leon/solvers/smtlib/SMTLIBZ3Target.scala
+++ b/src/main/scala/leon/solvers/smtlib/SMTLIBZ3Target.scala
@@ -29,7 +29,7 @@ trait SMTLIBZ3Target extends SMTLIBTarget {
def getNewInterpreter(ctx: LeonContext) = {
val opts = interpreterOps(ctx)
- reporter.debug("Invoking solver "+targetName+" with "+opts.mkString(" "))
+ context.reporter.debug("Invoking solver "+targetName+" with "+opts.mkString(" "))
new Z3Interpreter("z3", opts.toArray)
}
diff --git a/src/main/scala/leon/solvers/sygus/SygusSolver.scala b/src/main/scala/leon/solvers/sygus/SygusSolver.scala
index f8f2c52d1..9cfefb228 100644
--- a/src/main/scala/leon/solvers/sygus/SygusSolver.scala
+++ b/src/main/scala/leon/solvers/sygus/SygusSolver.scala
@@ -81,7 +81,7 @@ abstract class SygusSolver(val context: LeonContext, val program: Program, val p
val res = fromSMT(body, sorts.toA(retSort))(Map(), Map())
Some(res)
case r =>
- reporter.warning("Unnexpected result from cvc4-sygus: "+r)
+ context.reporter.warning("Unnexpected result from cvc4-sygus: "+r)
None
}
}).flatten
@@ -96,7 +96,7 @@ abstract class SygusSolver(val context: LeonContext, val program: Program, val p
None
case r =>
- reporter.warning("Unnexpected result from cvc4-sygus: "+r+" expected unsat")
+ context.reporter.warning("Unnexpected result from cvc4-sygus: "+r+" expected unsat")
None
}
} catch {
diff --git a/src/main/scala/leon/solvers/unrolling/UnrollingSolver.scala b/src/main/scala/leon/solvers/unrolling/UnrollingSolver.scala
index 690f0dc2d..2620bd5dc 100644
--- a/src/main/scala/leon/solvers/unrolling/UnrollingSolver.scala
+++ b/src/main/scala/leon/solvers/unrolling/UnrollingSolver.scala
@@ -76,8 +76,6 @@ trait AbstractUnrollingSolver[T]
protected var interrupted : Boolean = false
- protected val reporter = context.reporter
-
lazy val templateGenerator = new TemplateGenerator(theoryEncoder, templateEncoder, assumePreHolds)
lazy val unrollingBank = new UnrollingBank(context, templateGenerator)
@@ -463,7 +461,7 @@ trait AbstractUnrollingSolver[T]
}
class UnrollingSolver(
- val context: LeonContext,
+ val sctx: SolverContext,
val program: Program,
underlying: Solver,
theories: TheoryEncoder = new NoEncoder
diff --git a/src/main/scala/leon/solvers/z3/AbstractZ3Solver.scala b/src/main/scala/leon/solvers/z3/AbstractZ3Solver.scala
index 7bd2d93e8..95460440e 100644
--- a/src/main/scala/leon/solvers/z3/AbstractZ3Solver.scala
+++ b/src/main/scala/leon/solvers/z3/AbstractZ3Solver.scala
@@ -5,7 +5,7 @@ package solvers.z3
import leon.utils._
-import z3.scala._
+import z3.scala.{Z3Solver => ScalaZ3Solver, _}
import solvers._
import purescala.Common._
import purescala.Definitions._
@@ -19,18 +19,14 @@ import purescala.Types._
case class UnsoundExtractionException(ast: Z3AST, msg: String)
extends Exception("Can't extract " + ast + " : " + msg)
-object AbstractZ3Solver
-
// This is just to factor out the things that are common in "classes that deal
// with a Z3 instance"
-trait AbstractZ3Solver extends Solver {
+trait AbstractZ3Solver extends Z3Solver {
val program : Program
val library = program.library
- protected val reporter : Reporter = context.reporter
-
context.interruptManager.registerForInterrupts(this)
private[this] var freed = false
@@ -57,7 +53,7 @@ trait AbstractZ3Solver extends Solver {
// Well... actually maybe not, but let's just leave it here to be sure
toggleWarningMessages(true)
- protected var solver : Z3Solver = null
+ protected var solver : ScalaZ3Solver = null
override def free(): Unit = {
freed = true
diff --git a/src/main/scala/leon/solvers/z3/FairZ3Solver.scala b/src/main/scala/leon/solvers/z3/FairZ3Solver.scala
index 414d3185a..04f0e34aa 100644
--- a/src/main/scala/leon/solvers/z3/FairZ3Solver.scala
+++ b/src/main/scala/leon/solvers/z3/FairZ3Solver.scala
@@ -16,7 +16,7 @@ import unrolling._
import theories._
import utils._
-class FairZ3Solver(val context: LeonContext, val program: Program)
+class FairZ3Solver(val sctx: SolverContext, val program: Program)
extends AbstractZ3Solver
with AbstractUnrollingSolver[Z3AST] {
@@ -29,7 +29,6 @@ class FairZ3Solver(val context: LeonContext, val program: Program)
override val name = "Z3-f"
override val description = "Fair Z3 Solver"
- override protected val reporter = context.reporter
override def reset(): Unit = super[AbstractZ3Solver].reset()
def declareVariable(id: Identifier): Z3AST = variables.cachedB(Variable(id)) {
diff --git a/src/main/scala/leon/solvers/z3/UninterpretedZ3Solver.scala b/src/main/scala/leon/solvers/z3/UninterpretedZ3Solver.scala
index 829c77343..88031219a 100644
--- a/src/main/scala/leon/solvers/z3/UninterpretedZ3Solver.scala
+++ b/src/main/scala/leon/solvers/z3/UninterpretedZ3Solver.scala
@@ -22,7 +22,7 @@ import purescala.Types._
* - otherwise it returns UNKNOWN
* Results should come back very quickly.
*/
-class UninterpretedZ3Solver(val context : LeonContext, val program: Program)
+class UninterpretedZ3Solver(val sctx: SolverContext, val program: Program)
extends AbstractZ3Solver
with Z3ModelReconstruction {
diff --git a/src/main/scala/leon/solvers/z3/Z3Solver.scala b/src/main/scala/leon/solvers/z3/Z3Solver.scala
new file mode 100644
index 000000000..24feda9ff
--- /dev/null
+++ b/src/main/scala/leon/solvers/z3/Z3Solver.scala
@@ -0,0 +1,7 @@
+/* Copyright 2009-2016 EPFL, Lausanne */
+
+package leon
+package solvers
+package z3
+
+trait Z3Solver extends Solver
diff --git a/src/main/scala/leon/solvers/z3/Z3UnrollingSolver.scala b/src/main/scala/leon/solvers/z3/Z3UnrollingSolver.scala
index fba5f0b10..ce224e8dc 100644
--- a/src/main/scala/leon/solvers/z3/Z3UnrollingSolver.scala
+++ b/src/main/scala/leon/solvers/z3/Z3UnrollingSolver.scala
@@ -9,5 +9,8 @@ import purescala.Definitions._
import unrolling._
import theories._
-class Z3UnrollingSolver(context: LeonContext, program: Program, underlying: Solver)
- extends UnrollingSolver(context, program, underlying, new StringEncoder(context, program) >> new BagEncoder(context, program))
+class Z3UnrollingSolver(context: SolverContext, program: Program, underlying: Z3Solver)
+ extends UnrollingSolver(context, program, underlying,
+ new StringEncoder(context.context, program) >>
+ new BagEncoder(context.context, program))
+ with Z3Solver
diff --git a/src/test/scala/leon/integration/solvers/EnumerationSolverSuite.scala b/src/test/scala/leon/integration/solvers/EnumerationSolverSuite.scala
index 50897d972..cd3f846e8 100644
--- a/src/test/scala/leon/integration/solvers/EnumerationSolverSuite.scala
+++ b/src/test/scala/leon/integration/solvers/EnumerationSolverSuite.scala
@@ -11,7 +11,7 @@ import leon.LeonContext
class EnumerationSolverSuite extends LeonSolverSuite {
def getSolver(implicit ctx: LeonContext, pgm: Program) = {
- new EnumerationSolver(ctx, pgm)
+ new EnumerationSolver(ctx.toSctx, pgm)
}
val sources = Nil
diff --git a/src/test/scala/leon/integration/solvers/FairZ3SolverTests.scala b/src/test/scala/leon/integration/solvers/FairZ3SolverTests.scala
index 91967c426..6901791ad 100644
--- a/src/test/scala/leon/integration/solvers/FairZ3SolverTests.scala
+++ b/src/test/scala/leon/integration/solvers/FairZ3SolverTests.scala
@@ -21,7 +21,7 @@ class FairZ3SolverTests extends LeonSolverSuite {
)
def getSolver(implicit ctx: LeonContext, pgm: Program) = {
- new FairZ3Solver(ctx, pgm)
+ new FairZ3Solver(ctx.toSctx, pgm)
}
test("Tautology 1") { implicit fix =>
diff --git a/src/test/scala/leon/integration/solvers/GlobalVariablesSuite.scala b/src/test/scala/leon/integration/solvers/GlobalVariablesSuite.scala
index 628086b41..1e8fc65d1 100644
--- a/src/test/scala/leon/integration/solvers/GlobalVariablesSuite.scala
+++ b/src/test/scala/leon/integration/solvers/GlobalVariablesSuite.scala
@@ -31,20 +31,14 @@ class GlobalVariablesSuite extends LeonTestSuiteWithProgram with ExpressionsDSL
|} """.stripMargin
)
- val getFactories: Seq[(String, (LeonContext, Program) => Solver)] = {
- (if (SolverFactory.hasNativeZ3) Seq(
- ("fairz3", (ctx: LeonContext, pgm: Program) => new FairZ3Solver(ctx, pgm))
- ) else Nil) ++
- (if (SolverFactory.hasZ3) Seq(
- ("smt-z3", (ctx: LeonContext, pgm: Program) => new UnrollingSolver(ctx, pgm, new SMTLIBZ3Solver(ctx, pgm)))
- ) else Nil) ++
- (if (SolverFactory.hasCVC4) Seq(
- ("smt-cvc4", (ctx: LeonContext, pgm: Program) => new UnrollingSolver(ctx, pgm, new SMTLIBCVC4Solver(ctx, pgm)))
- ) else Nil)
+ val solverNames: Seq[String] = {
+ (if (SolverFactory.hasNativeZ3) Seq("fairz3") else Nil) ++
+ (if (SolverFactory.hasZ3) Seq("smt-z3") else Nil) ++
+ (if (SolverFactory.hasCVC4) Seq("smt-cvc4") else Nil)
}
// Check that we correctly extract several types from solver models
- for ((sname, sf) <- getFactories) {
+ for (sname <- solverNames) {
test(s"Global Variables in $sname") { implicit fix =>
val ctx = fix._1
val pgm = fix._2
@@ -55,7 +49,7 @@ class GlobalVariablesSuite extends LeonTestSuiteWithProgram with ExpressionsDSL
fd.body = Some(IfExpr(b0.toVariable, bi(1), bi(-1)))
val cnstr = LessThan(FunctionInvocation(fd.typed, Seq(bi(42))), bi(0))
- val solver = sf(ctx, pgm)
+ val solver = SolverFactory.getFromName(ctx, pgm)(sname).getNewSolver()
solver.assertCnstr(And(b0.toVariable, cnstr))
try {
diff --git a/src/test/scala/leon/integration/solvers/QuantifierSolverSuite.scala b/src/test/scala/leon/integration/solvers/QuantifierSolverSuite.scala
index 0bc83e224..f50eb57c7 100644
--- a/src/test/scala/leon/integration/solvers/QuantifierSolverSuite.scala
+++ b/src/test/scala/leon/integration/solvers/QuantifierSolverSuite.scala
@@ -22,16 +22,10 @@ class QuantifierSolverSuite extends LeonTestSuiteWithProgram {
override val leonOpts = List("--checkmodels")
- val getFactories: Seq[(String, (LeonContext, Program) => Solver)] = {
- (if (SolverFactory.hasNativeZ3) Seq(
- ("fairz3", (ctx: LeonContext, pgm: Program) => new FairZ3Solver(ctx, pgm))
- ) else Nil) ++
- (if (SolverFactory.hasZ3) Seq(
- ("smt-z3", (ctx: LeonContext, pgm: Program) => new Z3UnrollingSolver(ctx, pgm, new SMTLIBZ3Solver(ctx, pgm)))
- ) else Nil) ++
- (if (SolverFactory.hasCVC4) Seq(
- ("smt-cvc4", (ctx: LeonContext, pgm: Program) => new CVC4UnrollingSolver(ctx, pgm, new SMTLIBCVC4Solver(ctx, pgm)))
- ) else Nil)
+ val solverNames: Seq[String] = {
+ (if (SolverFactory.hasNativeZ3) Seq("fairz3") else Nil) ++
+ (if (SolverFactory.hasZ3) Seq("smt-z3") else Nil) ++
+ (if (SolverFactory.hasCVC4) Seq("smt-cvc4") else Nil)
}
val f1: Identifier = FreshIdentifier("f1", FunctionType(Seq(IntegerType, IntegerType), IntegerType))
@@ -119,10 +113,10 @@ class QuantifierSolverSuite extends LeonTestSuiteWithProgram {
}
}
- for ((sname, sf) <- getFactories; (ename, expr) <- satisfiable) {
+ for (sname <- solverNames; (ename, expr) <- satisfiable) {
test(s"Satisfiable quantified formula $ename in $sname") { implicit fix =>
val (ctx, pgm) = fix
- val solver = sf(ctx, pgm)
+ val solver = SolverFactory.getFromName(ctx, pgm)(sname).getNewSolver()
checkSolver(solver, expr, true)
}
@@ -137,10 +131,10 @@ class QuantifierSolverSuite extends LeonTestSuiteWithProgram {
*/
}
- for ((sname, sf) <- getFactories; (ename, expr) <- unsatisfiable) {
+ for (sname <- solverNames; (ename, expr) <- unsatisfiable) {
test(s"Unsatisfiable quantified formula $ename in $sname") { implicit fix =>
val (ctx, pgm) = fix
- val solver = sf(ctx, pgm)
+ val solver = SolverFactory.getFromName(ctx, pgm)(sname).getNewSolver()
checkSolver(solver, expr, false)
}
}
diff --git a/src/test/scala/leon/integration/solvers/SolversSuite.scala b/src/test/scala/leon/integration/solvers/SolversSuite.scala
index f47f3c9b9..5f987a145 100644
--- a/src/test/scala/leon/integration/solvers/SolversSuite.scala
+++ b/src/test/scala/leon/integration/solvers/SolversSuite.scala
@@ -19,16 +19,10 @@ class SolversSuite extends LeonTestSuiteWithProgram {
val sources = List()
- val getFactories: Seq[(String, (LeonContext, Program) => Solver)] = {
- (if (SolverFactory.hasNativeZ3) Seq(
- ("fairz3", (ctx: LeonContext, pgm: Program) => new FairZ3Solver(ctx, pgm))
- ) else Nil) ++
- (if (SolverFactory.hasZ3) Seq(
- ("smt-z3", (ctx: LeonContext, pgm: Program) => new Z3UnrollingSolver(ctx, pgm, new SMTLIBZ3Solver(ctx, pgm)))
- ) else Nil) ++
- (if (SolverFactory.hasCVC4) Seq(
- ("smt-cvc4", (ctx: LeonContext, pgm: Program) => new Z3UnrollingSolver(ctx, pgm, new SMTLIBCVC4Solver(ctx, pgm)))
- ) else Nil)
+ val solverNames: Seq[String] = {
+ (if (SolverFactory.hasNativeZ3) Seq("fairz3") else Nil) ++
+ (if (SolverFactory.hasZ3) Seq("smt-z3") else Nil) ++
+ (if (SolverFactory.hasCVC4) Seq("smt-cvc4") else Nil)
}
val types = Seq(
@@ -88,18 +82,18 @@ class SolversSuite extends LeonTestSuiteWithProgram {
}
// Check that we correctly extract several types from solver models
- for ((sname, sf) <- getFactories) {
+ for (sname <- solverNames) {
test(s"Model Extraction in $sname") { implicit fix =>
val ctx = fix._1
val pgm = fix._2
- val solver = sf(ctx, pgm)
+ val solver = SolverFactory.getFromName(ctx, pgm)(sname).getNewSolver()
checkSolver(solver, vs.toSet, andJoin(cnstrs))
}
}
test(s"Data generation in enum solver") { implicit fix =>
for ((v,cnstr) <- vs zip cnstrs) {
- val solver = new EnumerationSolver(fix._1, fix._2)
+ val solver = new EnumerationSolver(fix._1.toSctx, fix._2)
checkSolver(solver, Set(v), cnstr)
}
}
diff --git a/src/test/scala/leon/integration/solvers/TimeoutSolverSuite.scala b/src/test/scala/leon/integration/solvers/TimeoutSolverSuite.scala
index 9714c5678..ca0eaf2b7 100644
--- a/src/test/scala/leon/integration/solvers/TimeoutSolverSuite.scala
+++ b/src/test/scala/leon/integration/solvers/TimeoutSolverSuite.scala
@@ -11,7 +11,7 @@ import leon.purescala.Expressions._
import leon.purescala.Types._
class TimeoutSolverSuite extends LeonTestSuite {
- private class IdioticSolver(val context : LeonContext, val program: Program) extends Solver with NaiveAssumptionSolver {
+ private class IdioticSolver(val sctx: SolverContext, val program: Program) extends Solver with NaiveAssumptionSolver {
val name = "Idiotic"
val description = "Loops"
@@ -45,7 +45,7 @@ class TimeoutSolverSuite extends LeonTestSuite {
}
private def getTOSolver(ctx: LeonContext): SolverFactory[Solver] = {
- SolverFactory("idiotic", () => (new IdioticSolver(ctx, Program.empty) with TimeoutSolver).setTimeout(200L))
+ SolverFactory("idiotic", () => (new IdioticSolver(ctx.toSctx, Program.empty) with TimeoutSolver).setTimeout(200L))
}
private def check(sf: SolverFactory[Solver], e: Expr): Option[Boolean] = {
diff --git a/src/test/scala/leon/integration/solvers/UnrollingSolverSuite.scala b/src/test/scala/leon/integration/solvers/UnrollingSolverSuite.scala
index 413ee804c..04450dfc2 100644
--- a/src/test/scala/leon/integration/solvers/UnrollingSolverSuite.scala
+++ b/src/test/scala/leon/integration/solvers/UnrollingSolverSuite.scala
@@ -7,7 +7,7 @@ import leon.purescala.Expressions._
import leon.purescala.Types._
import leon.purescala.Common._
import leon.purescala.Definitions._
-import leon.solvers.z3._
+import leon.solvers._
class UnrollingSolverSuite extends LeonSolverSuite {
@@ -26,7 +26,7 @@ class UnrollingSolverSuite extends LeonSolverSuite {
)
def getSolver(implicit ctx: LeonContext, pgm: Program) = {
- new Z3UnrollingSolver(ctx, pgm, new UninterpretedZ3Solver(ctx, pgm))
+ SolverFactory.getFromName(ctx, pgm)("unrollz3").getNewSolver()
}
test("'true' should be valid") { implicit fix =>
diff --git a/src/test/scala/leon/unit/solvers/SolverPoolSuite.scala b/src/test/scala/leon/unit/solvers/SolverPoolSuite.scala
index ad781b577..09f9fc603 100644
--- a/src/test/scala/leon/unit/solvers/SolverPoolSuite.scala
+++ b/src/test/scala/leon/unit/solvers/SolverPoolSuite.scala
@@ -12,7 +12,7 @@ import leon.purescala.Expressions._
class SolverPoolSuite extends LeonTestSuite {
- private class DummySolver(val context : LeonContext, val program: Program) extends Solver with NaiveAssumptionSolver {
+ private class DummySolver(val sctx: SolverContext, val program: Program) extends Solver with NaiveAssumptionSolver {
val name = "Dummy"
val description = "dummy"
@@ -28,7 +28,7 @@ class SolverPoolSuite extends LeonTestSuite {
}
def sfactory(implicit ctx: LeonContext): SolverFactory[Solver] = {
- SolverFactory("dummy", () => new DummySolver(ctx, Program.empty))
+ SolverFactory("dummy", () => new DummySolver(ctx.toSctx, Program.empty))
}
val poolSize = 5;
--
GitLab