diff --git a/src/main/scala/leon/LeonContext.scala b/src/main/scala/leon/LeonContext.scala index f46e53d0461d862a29d8778f9b32379fbe8409ea..8e0a414f147ba551a85fe417bc5fa5a409e6c821 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 cdab9cc0e714982a664f3f8f644e5c2082845e9a..a1323b4e1ddbc39d4103a094d9fe843a397280fa 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 de666f389dd4f8ea64af18b7a11a3ce0cc7b3b3c..3cc47bdd677582ee74b5da2168494cbd0084b331 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 db18be70ef483f4e9ec138a8a40a90c3a78b21d1..41b86de7c8bbf83d2c6200c469bbb6e06401e27d 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 45316adff5d64d141f5793e539d3cc1a1dbccefa..336b7960303946553f02b37ad0c0250dd1d06100 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 f81d340c73b37346e2b69d3d2574787dbe858d76..8902564ded5e43b97bf736a838966e200cd4cfa3 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 3e40886a549b4685dc3597ddd36754708d54371e..db02d58c035fcfc08b06cd5d98347dfa34c4d9b7 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 79f53ef9134a07198b8ef2c87f3deff0571e26ad..86a3a91f012ef581c871a33f5198e3b7c3407c96 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 0930478d8356ef05dde8e4401a8e1593040a4563..292ef160541ac0dd2d0e431feacba6790f1da90b 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 130f8d86b32218bc7af5fc677dc43997c7cd5aac..a50b3f814fac04474cbf0604583f3e4c05cea83c 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 e1c9525ae3e20b24f6ee474634b07dc91647fcf3..935274abfaef3b8e3a8bcdffd245b7e9496cab53 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 bf7e392a7e56b5739e5281cd1d00d811fb127a12..59d9859fb7bcde2f7d048543a9d67c99e381ac42 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 8d42223c814ae6b91020328a7a4f07661c4fa19a..48acc71f478f53fd6326d35bd850044a54f91868 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 f374344e56bbbd388f9d9d8c8ef82065860780d1..1a942fd420ba09a238e1d3c3bb70146ddb3d9903 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 d5027a440761b8f8671cd2c96826312335a0d35c..2c5f8df14e9e801e62851981d78a37c00b486f49 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 0000000000000000000000000000000000000000..ff112d7921fdf9f1c74bf7c7187f1e312c58d713 --- /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 97b5d4dc91a2efcf8c4c6446a7049f4ef28b42fa..b293abbe209269ef1373ed4937be52a43850bc1c 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 8623bd014a7d8f06d41b4859e4d95210f1a03289..6b3346152ef0bfc0e4e16dd20291190154b5387d 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 a6b52a3211e0729b78d62bce27281d98905af5f2..b1895380c94483c4646950d68b676aacf3cdb986 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 973546c6891e3a321c05a4777e873bdb2dff35fd..ff27a312f858992f5fdd890181f9d86ac5f8aac3 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 8c16d013fb34e653f99abd207fff7fcbc3f2e202..ce6b963ba88fe7e5280f6e30291d56a17d431b4b 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 39d83d7c7354fab56ad7fd73ac72e8dc3e137384..86768670465a89ea498e5bf30d29fc19d578c48a 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 b67140f4b8db84784395f892d19c3694ffee787d..8b5fd705b6aa6fe37ff55a0c902599f957f2011b 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 8838ae8ffc6443ba2961f51ecce795004dc98233..f8c36a52793a88b93b2eb83e889285f7a2067058 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 30ae22f989a2b021e56165fdaf3021246720a013..04763b1b593df46c358651e28f6dfbd905fd4269 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 9f6f92b93c0cafc7cf73210879d32b3c9defff2b..346889d30a4b9e86ad2d3531ed339b6db184f652 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 cd7eae5e8330bac85f5a554b624bf98576655895..87d7985281b49d82cda40aa7a493f6e00200584c 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 0be498f1352e0ced484318ca5b48d3f8d7b1da00..7dd3e4be718ce0e2d39de37086ccc637cc90d202 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 f355392d069edfd55ab97a530b814bb0211a8e8a..9b696cea0b496014d402ac4b9f9491d4b9494272 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 43c1643cf89bef425d30fa1c4e6e11eaa02cf3ed..019eea370b46fa97af8042bda18449c72c623e9a 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 00b361323de76d5647a124eb65f449161390a15e..52894a29c644183f0ff77c9ea36ac530aab73ef8 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 f8f2c52d1cf5c21e57d6637e88015490245c3e2b..9cfefb228f95ac9adaa39023aa1671fb98fa4509 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 690f0dc2d7bfaef7b7587ea471b4bd6bf8f580ff..2620bd5dcbec43cb4775a8e3dafe70776ccafd21 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 7bd2d93e828ce92ae948f11b1c0ce06e0fae4aff..95460440e8245ee33cf6f7e21ab0e63714b948c3 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 414d3185a8af4a449ed88ce389e2b4bff1cf9ed1..04f0e34aa46c012425622a2b5fce9f8054d04405 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 829c773438dd8a1509ab08560a730cf1ede86b18..88031219a18f0c43867696f77c78e73e4777bdf1 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 0000000000000000000000000000000000000000..24feda9fff650925419fb14450f0e198ad9a29ae --- /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 fba5f0b100181f385496e0ace906d3252e110f1d..ce224e8dc2baaa4e7d0861f9677c663919dc5aa7 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 50897d972c9808cb91258619061f9554235b76da..cd3f846e8ada4e44a4a1f636e0425d498d2c3fb5 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 91967c426ab02e3167b3dd724973708950717cdd..6901791ad92a5620d04f0e1d7e2d80abc5922671 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 628086b41c9df04e255aa91ec5d422e568d239a7..1e8fc65d1126075c63ba87c764a7db063850aab7 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 0bc83e224c8632042d7dbf35b94971f9f23e49e3..f50eb57c72ec467dd906811e4d1003a9d187d6d5 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 f47f3c9b9e58f9eb44c601716d363cbeedc6b3d3..5f987a1454f4c025d8a44864a13c24523a904138 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 9714c5678c7490fa415f11149c7b2640af123183..ca0eaf2b71cfd04b384842d3314ce5cc22b6c9d4 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 413ee804ccb639fe479d36f918d8aee2fd6679f2..04450dfc2eef9bdf705e8a4bb42660ddf114383c 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 ad781b577e27414638686b78940ece46f288ba7d..09f9fc603a5e7d15da443d65caf632bcba781915 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;