diff --git a/build.sbt b/build.sbt
index 39ab1fb41bb5b097439ebb93f8eeec8031e8876f..533388b861ccc4cd3c669c3478259d0808a28fde 100644
--- a/build.sbt
+++ b/build.sbt
@@ -162,6 +162,8 @@ testOptions in NativeZ3RegressionTest := Seq(Tests.Argument("-oDF"), Tests.Filte
parallelExecution in NativeZ3RegressionTest := false
+logBuffered in NativeZ3RegressionTest := false
+
// Isabelle Tests
lazy val IsabelleTest = config("isabelle") extend(Test)
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/CompilationUnit.scala b/src/main/scala/leon/codegen/CompilationUnit.scala
index 88f1679bceda88c4d535e2f5e51b18d7e5b1b1cb..1eac956d238a9256d42277c3b15aae0e8b884672 100644
--- a/src/main/scala/leon/codegen/CompilationUnit.scala
+++ b/src/main/scala/leon/codegen/CompilationUnit.scala
@@ -25,9 +25,11 @@ import scala.collection.JavaConverters._
import java.lang.reflect.Constructor
import synthesis.Problem
+import evaluators._
class CompilationUnit(val ctx: LeonContext,
val program: Program,
+ val bank: EvaluationBank = new EvaluationBank,
val params: CodeGenParams = CodeGenParams.default) extends CodeGeneration {
diff --git a/src/main/scala/leon/codegen/runtime/Monitor.scala b/src/main/scala/leon/codegen/runtime/Monitor.scala
index e4a0afa66a578cd19bce0e83e66c626d9399c5a6..a1323b4e1ddbc39d4103a094d9fe843a397280fa 100644
--- a/src/main/scala/leon/codegen/runtime/Monitor.scala
+++ b/src/main/scala/leon/codegen/runtime/Monitor.scala
@@ -19,9 +19,10 @@ 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._
import synthesis._
abstract class Monitor {
@@ -85,7 +86,7 @@ class StdMonitor(unit: CompilationUnit, invocationsMax: Int, bodies: ScalaMap[Id
def invariantCheck(obj: AnyRef, tpeIdx: Int): Boolean = {
val tpe = unit.runtimeIdToTypeMap(tpeIdx)
val cc = unit.jvmToValue(obj, tpe).asInstanceOf[LeonCaseClass]
- val result = evaluators.Evaluator.invariantCheck(cc)
+ val result = unit.bank.invariantCheck(cc)
if (result.isFailure) throw new LeonCodeGenRuntimeException("ADT invariant failed @" + cc.ct.classDef.invariant.get.getPos)
else result.isRequired
}
@@ -93,7 +94,7 @@ class StdMonitor(unit: CompilationUnit, invocationsMax: Int, bodies: ScalaMap[Id
def invariantResult(obj: AnyRef, tpeIdx: Int, result: Boolean): Unit = {
val tpe = unit.runtimeIdToTypeMap(tpeIdx)
val cc = unit.jvmToValue(obj, tpe).asInstanceOf[LeonCaseClass]
- evaluators.Evaluator.invariantResult(cc, result)
+ unit.bank.invariantResult(cc, result)
if (!result) throw new LeonCodeGenRuntimeException("ADT invariant failed @" + cc.ct.classDef.invariant.get.getPos)
}
@@ -137,7 +138,8 @@ class StdMonitor(unit: CompilationUnit, invocationsMax: Int, bodies: ScalaMap[Id
} else {
val tStart = System.currentTimeMillis
- val solverf = SolverFactory.getFromSettings(ctx, program).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(_))
@@ -222,7 +224,8 @@ class StdMonitor(unit: CompilationUnit, invocationsMax: Int, bodies: ScalaMap[Id
} else {
val tStart = System.currentTimeMillis
- val solverf = SolverFactory.getFromSettings(ctx, program).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/datagen/VanuatooDataGen.scala b/src/main/scala/leon/datagen/VanuatooDataGen.scala
index 6e13cb030ad7df32b6a5ec1543e6d2c80915903d..ccba55af919489697d9d9e6a3aa59768d29dbab2 100644
--- a/src/main/scala/leon/datagen/VanuatooDataGen.scala
+++ b/src/main/scala/leon/datagen/VanuatooDataGen.scala
@@ -18,8 +18,8 @@ import vanuatoo.{Pattern => VPattern, _}
import evaluators._
-class VanuatooDataGen(ctx: LeonContext, p: Program) extends DataGenerator {
- val unit = new CompilationUnit(ctx, p, CodeGenParams.default.copy(doInstrument = true))
+class VanuatooDataGen(ctx: LeonContext, p: Program, bank: EvaluationBank = new EvaluationBank) extends DataGenerator {
+ val unit = new CompilationUnit(ctx, p, bank, CodeGenParams.default.copy(doInstrument = true))
val ints = (for (i <- Set(0, 1, 2, 3)) yield {
i -> Constructor[Expr, TypeTree](List(), Int32Type, s => IntLiteral(i), ""+i)
diff --git a/src/main/scala/leon/evaluators/AngelicEvaluator.scala b/src/main/scala/leon/evaluators/AngelicEvaluator.scala
index 8230aa85845d35e0113aec976800cbe5a5f49799..26db1865b824d2fe9bae2efe3b937bb913385d72 100644
--- a/src/main/scala/leon/evaluators/AngelicEvaluator.scala
+++ b/src/main/scala/leon/evaluators/AngelicEvaluator.scala
@@ -9,11 +9,13 @@ import EvaluationResults._
class AngelicEvaluator(underlying: NDEvaluator)
extends Evaluator(underlying.context, underlying.program)
- with DeterministicEvaluator
-{
+ with DeterministicEvaluator {
+
val description: String = "angelic evaluator"
val name: String = "Interpreter that returns the first solution of a non-deterministic program"
+ val bank = new EvaluationBank
+
def eval(expr: Expr, model: Model): EvaluationResult = underlying.eval(expr, model) match {
case Successful(Stream(h, _*)) =>
Successful(h)
@@ -26,11 +28,13 @@ class AngelicEvaluator(underlying: NDEvaluator)
class DemonicEvaluator(underlying: NDEvaluator)
extends Evaluator(underlying.context, underlying.program)
- with DeterministicEvaluator
-{
+ with DeterministicEvaluator {
+
val description: String = "demonic evaluator"
val name: String = "Interpreter that demands an underlying non-deterministic program has unique solution"
+ val bank = new EvaluationBank
+
def eval(expr: Expr, model: Model): EvaluationResult = underlying.eval(expr, model) match {
case Successful(Stream(h)) =>
Successful(h)
diff --git a/src/main/scala/leon/evaluators/CodeGenEvaluator.scala b/src/main/scala/leon/evaluators/CodeGenEvaluator.scala
index 8521094fababa7b0679dee1bc84691a22048e822..74df09badc4cd7058a8ee152ee614ea35c1fde78 100644
--- a/src/main/scala/leon/evaluators/CodeGenEvaluator.scala
+++ b/src/main/scala/leon/evaluators/CodeGenEvaluator.scala
@@ -14,14 +14,16 @@ import codegen.CodeGenParams
import leon.codegen.runtime.LeonCodeGenRuntimeException
import leon.codegen.runtime.LeonCodeGenEvaluationException
-class CodeGenEvaluator(ctx: LeonContext, val unit : CompilationUnit) extends Evaluator(ctx, unit.program) with DeterministicEvaluator {
+class CodeGenEvaluator(ctx: LeonContext, val unit: CompilationUnit) extends Evaluator(ctx, unit.program) with DeterministicEvaluator {
val name = "codegen-eval"
val description = "Evaluator for PureScala expressions based on compilation to JVM"
+ val bank = unit.bank
+
/** Another constructor to make it look more like other `Evaluator`s. */
- def this(ctx : LeonContext, prog : Program, params: CodeGenParams = CodeGenParams.default) {
- this(ctx, new CompilationUnit(ctx, prog, params))
+ def this(ctx: LeonContext, prog: Program, bank: EvaluationBank = new EvaluationBank, params: CodeGenParams = CodeGenParams.default) {
+ this(ctx, new CompilationUnit(ctx, prog, bank, params))
}
private def compileExpr(expression: Expr, args: Seq[Identifier]): Option[CompiledExpression] = {
diff --git a/src/main/scala/leon/evaluators/DefaultEvaluator.scala b/src/main/scala/leon/evaluators/DefaultEvaluator.scala
index b62446c8d1916537afb315dcac7e88c69b707e21..90fb4e0b91ebe303874f9a173adc8a137af8414d 100644
--- a/src/main/scala/leon/evaluators/DefaultEvaluator.scala
+++ b/src/main/scala/leon/evaluators/DefaultEvaluator.scala
@@ -5,7 +5,7 @@ package evaluators
import purescala.Definitions.Program
-class DefaultEvaluator(ctx: LeonContext, prog: Program)
- extends RecursiveEvaluator(ctx, prog, 50000)
- with HasDefaultGlobalContext
- with HasDefaultRecContext
+class DefaultEvaluator(ctx: LeonContext, prog: Program, bank: EvaluationBank = new EvaluationBank)
+ extends RecursiveEvaluator(ctx, prog, bank, 50000)
+ with HasDefaultGlobalContext
+ with HasDefaultRecContext
diff --git a/src/main/scala/leon/evaluators/DualEvaluator.scala b/src/main/scala/leon/evaluators/DualEvaluator.scala
index a59559185cf1b2fde266dfc20b5802867d9444a1..a99f4d4773d70f35fc981d41908f59f35856c2be 100644
--- a/src/main/scala/leon/evaluators/DualEvaluator.scala
+++ b/src/main/scala/leon/evaluators/DualEvaluator.scala
@@ -11,15 +11,19 @@ import purescala.Types._
import codegen._
import codegen.runtime.{StdMonitor, Monitor}
-class DualEvaluator(ctx: LeonContext, prog: Program, params: CodeGenParams)
- extends RecursiveEvaluator(ctx, prog, params.maxFunctionInvocations)
- with HasDefaultGlobalContext {
+class DualEvaluator(
+ ctx: LeonContext,
+ prog: Program,
+ bank: EvaluationBank = new EvaluationBank,
+ params: CodeGenParams = CodeGenParams.default
+) extends RecursiveEvaluator(ctx, prog, params.maxFunctionInvocations)
+ with HasDefaultGlobalContext {
type RC = DualRecContext
def initRC(mappings: Map[Identifier, Expr]): RC = DualRecContext(mappings)
implicit val debugSection = utils.DebugSectionEvaluation
- val unit = new CompilationUnit(ctx, prog, params)
+ val unit = new CompilationUnit(ctx, prog, bank, params)
var monitor: Monitor = new StdMonitor(unit, params.maxFunctionInvocations, Map())
diff --git a/src/main/scala/leon/evaluators/Evaluator.scala b/src/main/scala/leon/evaluators/Evaluator.scala
index 50f28a451d9376ec2deabfcc9c4d448aa5365ff0..ccde2fd20d9677f7c6331fb652121e529d8a29d8 100644
--- a/src/main/scala/leon/evaluators/Evaluator.scala
+++ b/src/main/scala/leon/evaluators/Evaluator.scala
@@ -48,6 +48,8 @@ abstract class Evaluator(val context: LeonContext, val program: Program) extends
trait DeterministicEvaluator extends Evaluator {
type Value = Expr
+
+ val bank: EvaluationBank
/**Evaluates the environment first, resolving non-cyclic dependencies, and then evaluate the expression */
override def eval(expr: Expr, mapping: Map[Identifier, Expr]) : EvaluationResult = {
@@ -65,7 +67,7 @@ trait DeterministicEvaluator extends Evaluator {
}
}
}
-
+
/** Returns an evaluated environment. If it fails, removes all non-values from the environment. */
def evalEnv(mapping: Iterable[(Identifier, Expr)]): Map[Identifier, Value] = {
if(mapping.forall{ case (key, value) => purescala.ExprOps.isValue(value) }) {
@@ -112,9 +114,38 @@ trait NDEvaluator extends Evaluator {
type Value = Stream[Expr]
}
-object Evaluator {
+/* 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
- /* Global set that tracks checked case-class invariants
+class EvaluationBank private(
+ /* Shared set that tracks checked case-class invariants
*
* Checking case-class invariants can require invoking a solver
* on a ground formula that contains a reference to `this` (the
@@ -123,42 +154,15 @@ object Evaluator {
* will again contain the constructor for the current case-class.
* This will create an invariant-checking loop.
*
- * To avoid this problem, we introduce a global set of invariants
- * that have already been checked. This set is used by all
- * evaluators to determine whether the invariant of a given case
+ * To avoid this problem, we introduce a set of invariants
+ * that have already been checked that is shared between related
+ * solvers and evaluators. This set is used by the evaluators to
+ * determine whether the invariant of a given case
* class should be checked.
*/
- private val checkCache: MutableMap[CaseClass, CheckStatus] = MutableMap.empty
-
- /* 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
- }
+ checkCache: MutableMap[CaseClass, CheckStatus]) {
- 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 {
@@ -174,4 +178,5 @@ object Evaluator {
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 e1786d1f082c5fceb2b72440d5217e4f624753f9..cc1c45bf135b786407c2df7642d1e8286fb6e2fe 100644
--- a/src/main/scala/leon/evaluators/RecursiveEvaluator.scala
+++ b/src/main/scala/leon/evaluators/RecursiveEvaluator.scala
@@ -15,15 +15,20 @@ import purescala.Expressions._
import purescala.Definitions._
import solvers.TimeoutableSolverFactory
import solvers.{PartialModel, SolverFactory}
+import purescala.DefOps
+import solvers.{PartialModel, Model, SolverFactory, SolverContext}
import solvers.unrolling.UnrollingProcedure
import scala.collection.mutable.{Map => MutableMap}
import scala.concurrent.duration._
import org.apache.commons.lang3.StringEscapeUtils
-abstract class RecursiveEvaluator(ctx: LeonContext, prog: Program, maxSteps: Int)
+abstract class RecursiveEvaluator(ctx: LeonContext, prog: Program, val bank: EvaluationBank, maxSteps: Int)
extends ContextualEvaluator(ctx, prog, maxSteps)
with DeterministicEvaluator {
+ def this(ctx: LeonContext, prog: Program, maxSteps: Int) =
+ this(ctx, prog, new EvaluationBank, maxSteps)
+
val name = "evaluator"
val description = "Recursive interpreter for PureScala expressions"
@@ -215,13 +220,13 @@ abstract class RecursiveEvaluator(ctx: LeonContext, prog: Program, maxSteps: Int
case CaseClass(cct, args) =>
val cc = CaseClass(cct, args.map(e))
- val check = Evaluator.invariantCheck(cc)
+ val check = bank.invariantCheck(cc)
if (check.isFailure) {
throw RuntimeError("ADT invariant violation for " + cct.classDef.id.asString + " reached in evaluation.: " + cct.invariant.get.asString)
} else if (check.isRequired) {
e(FunctionInvocation(cct.invariant.get, Seq(cc))) match {
case BooleanLiteral(success) =>
- Evaluator.invariantResult(cc, success)
+ bank.invariantResult(cc, success)
if (!success)
throw RuntimeError("ADT invariant violation for " + cct.classDef.id.asString + " reached in evaluation.: " + cct.invariant.get.asString)
case other =>
@@ -620,7 +625,8 @@ abstract class RecursiveEvaluator(ctx: LeonContext, prog: Program, maxSteps: Int
newOptions.exists(no => opt.optionDef == no.optionDef)
} ++ newOptions)
- val solverf = SolverFactory.getFromSettings(newCtx, program).withTimeout(1.second)
+ val sctx = SolverContext(newCtx, bank)
+ val solverf = SolverFactory.getFromSettings(sctx, program).withTimeout(1.second)
val solver = solverf.getNewSolver()
try {
@@ -751,7 +757,8 @@ abstract class RecursiveEvaluator(ctx: LeonContext, prog: Program, maxSteps: Int
clpCache.getOrElse((choose, ins), {
val tStart = System.currentTimeMillis
- val solverf = SolverFactory.getFromSettings(ctx, program).withTimeout(1.seconds)
+ val sctx = SolverContext(ctx, bank)
+ val solverf = SolverFactory.getFromSettings(sctx, program).withTimeout(1.seconds)
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/CegisSolver.scala b/src/main/scala/leon/invariant/templateSolvers/CegisSolver.scala
index da717fe778a33335ad77845ebbad7af97d649f65..72bffc37c94b5791af3b16582e3d6a4e740c90c5 100644
--- a/src/main/scala/leon/invariant/templateSolvers/CegisSolver.scala
+++ b/src/main/scala/leon/invariant/templateSolvers/CegisSolver.scala
@@ -155,7 +155,7 @@ class CegisCore(ctx: InferenceContext,
}
val t3 = System.currentTimeMillis()
val elapsedTime = (t3 - startTime)
- val solver2 = SimpleSolverAPI(new TimeoutSolverFactory(SolverFactory(() => new ExtendedUFSolver(context, program) with TimeoutSolver),
+ val solver2 = SimpleSolverAPI(new TimeoutSolverFactory(SolverFactory("extededUF", () => new ExtendedUFSolver(context, program) with TimeoutSolver),
timeoutMillis - elapsedTime))
val (res1, newModel) = if (solveAsInt) {
val intctr = And(newctr, initRealCtr)
@@ -214,7 +214,7 @@ class CegisCore(ctx: InferenceContext,
val debugMinimization = false
def minimizeReals(inputCtr: Expr, objective: Expr): (Option[Boolean], Model) = {
- val sol = SimpleSolverAPI(new TimeoutSolverFactory(SolverFactory(() => new ExtendedUFSolver(context, program) with TimeoutSolver), timeoutMillis))
+ val sol = SimpleSolverAPI(new TimeoutSolverFactory(SolverFactory("extendedUF", () => new ExtendedUFSolver(context, program) with TimeoutSolver), timeoutMillis))
val (res, model1) = sol.solveSAT(inputCtr)
res match {
case Some(true) => {
@@ -253,7 +253,7 @@ class CegisCore(ctx: InferenceContext,
}
val boundCtr = LessEquals(objective, currval)
- val solver2 = SimpleSolverAPI(new TimeoutSolverFactory(SolverFactory(() => new ExtendedUFSolver(context, program) with TimeoutSolver), timeoutMillis))
+ val solver2 = SimpleSolverAPI(new TimeoutSolverFactory(SolverFactory("extendedUF", () => new ExtendedUFSolver(context, program) with TimeoutSolver), timeoutMillis))
val (res, newModel) = sol.solveSAT(And(inputCtr, boundCtr))
res match {
case Some(true) => {
@@ -296,7 +296,7 @@ class CegisCore(ctx: InferenceContext,
}
def minimizeIntegers(inputCtr: Expr, objective: Expr): (Option[Boolean], Model) = {
- val sol = SimpleSolverAPI(new TimeoutSolverFactory(SolverFactory(() => new ExtendedUFSolver(context, program) with TimeoutSolver), timeoutMillis))
+ val sol = SimpleSolverAPI(new TimeoutSolverFactory(SolverFactory("extendedUF", () => new ExtendedUFSolver(context, program) with TimeoutSolver), timeoutMillis))
val (res, model1) = sol.solveSAT(inputCtr)
res match {
case Some(true) => {
@@ -328,7 +328,7 @@ class CegisCore(ctx: InferenceContext,
} else 2 * upperBound
}
val boundCtr = LessEquals(objective, InfiniteIntegerLiteral(currval))
- val solver2 = SimpleSolverAPI(new TimeoutSolverFactory(SolverFactory(() => new ExtendedUFSolver(context, program) with TimeoutSolver), timeoutMillis))
+ val solver2 = SimpleSolverAPI(new TimeoutSolverFactory(SolverFactory("extededUF", () => new ExtendedUFSolver(context, program) with TimeoutSolver), timeoutMillis))
val (res, newModel) = sol.solveSAT(And(inputCtr, boundCtr))
res match {
case Some(true) => {
@@ -367,4 +367,4 @@ class CegisCore(ctx: InferenceContext,
}
}
-}
\ No newline at end of file
+}
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/FarkasLemmaSolver.scala b/src/main/scala/leon/invariant/templateSolvers/FarkasLemmaSolver.scala
index 5831fcda02e1a14e9f0aa6bb0085b6b87fbcc22e..11a560be07ec4c678ad479971dedd8a079149f88 100644
--- a/src/main/scala/leon/invariant/templateSolvers/FarkasLemmaSolver.scala
+++ b/src/main/scala/leon/invariant/templateSolvers/FarkasLemmaSolver.scala
@@ -273,8 +273,9 @@ class FarkasLemmaSolver(ctx: InferenceContext, program: Program) {
//new ExtendedUFSolver(leonctx, program, useBitvectors = true, bitvecSize = bvsize) with TimeoutSolver
} else {
//new AbortableSolver(() => new SMTLIBZ3Solver(leonctx, program) with TimeoutSolver, ctx)
- SimpleSolverAPI(new TimeoutSolverFactory(SolverFactory(() =>
- new SMTLIBZ3Solver(leonctx, program) with TimeoutSolver), timeout * 1000))
+ SimpleSolverAPI(new TimeoutSolverFactory(
+ SolverFactory.getFromName(leonctx, program)("smt-z3-u"),
+ timeout * 1000))
}
if (verbose) reporter.info("solving...")
val (res, model) =
@@ -324,4 +325,4 @@ class FarkasLemmaSolver(ctx: InferenceContext, program: Program) {
(res, model)
}
}
-}
\ No newline at end of file
+}
diff --git a/src/main/scala/leon/invariant/templateSolvers/UniversalQuantificationSolver.scala b/src/main/scala/leon/invariant/templateSolvers/UniversalQuantificationSolver.scala
index b22f402ae5180edcb7efb5ec7e9997e9c1eaf174..db02d58c035fcfc08b06cd5d98347dfa34c4d9b7 100644
--- a/src/main/scala/leon/invariant/templateSolvers/UniversalQuantificationSolver.scala
+++ b/src/main/scala/leon/invariant/templateSolvers/UniversalQuantificationSolver.scala
@@ -63,8 +63,9 @@ class UniversalQuantificationSolver(ctx: InferenceContext, program: Program,
if (usePortfolio) {
if (useIncrementalSolvingForVCs)
throw new IllegalArgumentException("Cannot perform incremental solving with portfolio solvers!")
- SolverFactory(() => new PortfolioSolver(leonctx, Seq(new SMTLIBCVC4Solver(leonctx, program),
- new SMTLIBZ3Solver(leonctx, program))) with TimeoutSolver)
+ new PortfolioSolverFactory(leonctx.toSctx, Seq(
+ SolverFactory.getFromName(leonctx, program)("smt-cvc4-u"),
+ SolverFactory.getFromName(leonctx, program)("smt-z3-u")))
} else
SolverFactory.uninterpreted(leonctx, program)
@@ -360,7 +361,7 @@ class UniversalQuantificationSolver(ctx: InferenceContext, program: Program,
solver.pop()
solRes
} else
- SimpleSolverAPI(SolverFactory(() => solver)).solveSAT(instExpr)
+ SimpleSolverAPI(SolverFactory(solver.name, () => solver)).solveSAT(instExpr)
} { vccTime =>
if (verbose) reporter.info("checked VC inst... in " + vccTime / 1000.0 + "s")
updateCounterTime(vccTime, "VC-check-time", "disjuncts")
@@ -370,7 +371,7 @@ class UniversalQuantificationSolver(ctx: InferenceContext, program: Program,
/*ctrTracker.getVC(fd).checkUnflattening(tempVarMap,
SimpleSolverAPI(SolverFactory(() => solverFactory.getNewSolver())),
defaultEval)*/
- verifyModel(funData.simpleParts, packedModel, SimpleSolverAPI(SolverFactory(() => solverFactory.getNewSolver())))
+ verifyModel(funData.simpleParts, packedModel, SimpleSolverAPI(solverFactory))
//val unflatPath = ctrTracker.getVC(fd).pickSatFromUnflatFormula(funData.simpleParts, packedModel, defaultEval)
}
//for statistics
@@ -379,7 +380,7 @@ class UniversalQuantificationSolver(ctx: InferenceContext, program: Program,
unflatten(simplifyArithmetic(instantiateTemplate(ctrTracker.getVC(fd).eliminateBlockers, tempVarMap)))
Stats.updateCounterStats(atomNum(compressedVC), "Compressed-VC-size", "disjuncts")
time {
- SimpleSolverAPI(SolverFactory(() => solverFactory.getNewSolver())).solveSAT(compressedVC)
+ SimpleSolverAPI(solverFactory).solveSAT(compressedVC)
} { compTime =>
Stats.updateCumTime(compTime, "TotalCompressVCCTime")
reporter.info("checked compressed VC... in " + compTime / 1000.0 + "s")
diff --git a/src/main/scala/leon/invariant/util/Minimizer.scala b/src/main/scala/leon/invariant/util/Minimizer.scala
index ddf7c01dda693e9067376a2f1b01942ad7e007c2..a05b9d72b49f104c3b0a7eb227a4e8d331c1161a 100644
--- a/src/main/scala/leon/invariant/util/Minimizer.scala
+++ b/src/main/scala/leon/invariant/util/Minimizer.scala
@@ -54,8 +54,9 @@ class Minimizer(ctx: InferenceContext, program: Program) {
*/
def minimizeBounds(nestMap: Map[Variable, Int])(inputCtr: Expr, initModel: Model): Model = {
val orderedTempVars = nestMap.toSeq.sortWith((a, b) => a._2 >= b._2).map(_._1)
- lazy val solver = new SimpleSolverAPI(new TimeoutSolverFactory(SolverFactory(() =>
- new SMTLIBZ3Solver(leonctx, program) with TimeoutSolver), ctx.vcTimeout * 1000))
+ lazy val solver = new SimpleSolverAPI(new TimeoutSolverFactory(
+ SolverFactory.getFromName(leonctx,program)("smt-z3-u"),
+ ctx.vcTimeout * 1000))
reporter.info("minimizing...")
var currentModel = initModel
@@ -189,4 +190,4 @@ class Minimizer(ctx: InferenceContext, program: Program) {
functionNesting(template)
nestMap
}
-}
\ No newline at end of file
+}
diff --git a/src/main/scala/leon/invariant/util/SolverUtil.scala b/src/main/scala/leon/invariant/util/SolverUtil.scala
index e0f3fe000b8ddd332f7cf6557b6874613c7c3982..97d94021d00d3ad798595822c4f7fe7129966eea 100644
--- a/src/main/scala/leon/invariant/util/SolverUtil.scala
+++ b/src/main/scala/leon/invariant/util/SolverUtil.scala
@@ -72,7 +72,7 @@ object SolverUtil {
if (idmap.keys.nonEmpty) {
val newpathcond = replace(idmap, expr)
//check if this is solvable
- val solver = SimpleSolverAPI(SolverFactory(() => new ExtendedUFSolver(ctx, prog)))
+ val solver = SimpleSolverAPI(SolverFactory("extendedUF", () => new ExtendedUFSolver(ctx, prog)))
solver.solveSAT(newpathcond)._1 match {
case Some(true) => {
println("Path satisfiable for a?,c? -->6,2 ")
@@ -143,4 +143,4 @@ object SolverUtil {
}
}
-}
\ No newline at end of file
+}
diff --git a/src/main/scala/leon/purescala/ExprOps.scala b/src/main/scala/leon/purescala/ExprOps.scala
index c24201f719ea0b365c08ffef7afafaafd29dd72f..caf54fbb9472cf30e19faf0f6b3075ce53374768 100644
--- a/src/main/scala/leon/purescala/ExprOps.scala
+++ b/src/main/scala/leon/purescala/ExprOps.scala
@@ -2145,9 +2145,10 @@ object ExprOps extends GenTreeOps[Expr] {
case _ =>
fun
}
- var msgs: String = ""
- implicit class BooleanAdder(b: Boolean) {
- def <(msg: String) = {if(!b) msgs += msg; b}
+
+ // Use this only to debug isValueOfType
+ private implicit class BooleanAdder(b: Boolean) {
+ @inline def <(msg: String) = {/*if(!b) println(msg); */b}
}
/** Returns true if expr is a value of type t */
@@ -2184,11 +2185,12 @@ object ExprOps extends GenTreeOps[Expr] {
(ct == ct2) < s"$ct not equal to $ct2" &&
((args zip ct.fieldsTypes) forall (argstyped => isValueOfType(argstyped._1, argstyped._2)))
case (FiniteLambda(mapping, default, tpe), exTpe@FunctionType(ins, out)) =>
+ variablesOf(e).isEmpty &&
tpe == exTpe
case (Lambda(valdefs, body), FunctionType(ins, out)) =>
variablesOf(e).isEmpty &&
- (valdefs zip ins forall (vdin => (vdin._1.getType == vdin._2) < s"${vdin._1.getType} is not equal to ${vdin._2}")) &&
- (body.getType == out) < s"${body.getType} is not equal to ${out}"
+ (valdefs zip ins forall (vdin => TypeOps.isSubtypeOf(vdin._2, vdin._1.getType) < s"${vdin._2} is not a subtype of ${vdin._1.getType}")) &&
+ (TypeOps.isSubtypeOf(body.getType, out)) < s"${body.getType} is not a subtype of ${out}"
case (FiniteBag(elements, fbtpe), BagType(tpe)) =>
fbtpe == tpe && elements.forall{ case (key, value) => isValueOfType(key, tpe) && isValueOfType(value, IntegerType) }
case _ => false
diff --git a/src/main/scala/leon/purescala/SelfPrettyPrinter.scala b/src/main/scala/leon/purescala/SelfPrettyPrinter.scala
index 2488aec8cebdd6de10d070800a4991df2e9894ba..9212163a71956a25e23cce33b9c786fdffb4ccc3 100644
--- a/src/main/scala/leon/purescala/SelfPrettyPrinter.scala
+++ b/src/main/scala/leon/purescala/SelfPrettyPrinter.scala
@@ -109,12 +109,11 @@ class SelfPrettyPrinter {
case _ => false
} match {
case None => orElse
- case Some(l) =>
- ctx.reporter.debug("Executing pretty printer for type " + v.getType + " : " + l + " on " + v)
+ case Some(Lambda(Seq(ValDef(id)), body)) =>
+ ctx.reporter.debug("Executing pretty printer for type " + v.getType + " : " + v + " on " + v)
val ste = new DefaultEvaluator(ctx, program)
try {
- val toEvaluate = application(l, Seq(v))
- val result = ste.eval(toEvaluate)
+ val result = ste.eval(body, Map(id -> v))
result.result match {
case Some(StringLiteral(res)) if res != "" =>
diff --git a/src/main/scala/leon/repair/Repairman.scala b/src/main/scala/leon/repair/Repairman.scala
index 5027d5fdd3b72c63cabe25d9d62790f467dcf2b1..4cf9e1d359b8725527217e807f629257512618e8 100644
--- a/src/main/scala/leon/repair/Repairman.scala
+++ b/src/main/scala/leon/repair/Repairman.scala
@@ -224,7 +224,7 @@ class Repairman(ctx: LeonContext, program: Program, fd: FunDef, verifTimeoutMs:
val maxEnumerated = 1000
val maxValid = 400
- val evaluator = new CodeGenEvaluator(ctx, program, CodeGenParams.default)
+ val evaluator = new CodeGenEvaluator(ctx, program)
val inputsToExample: Seq[Expr] => Example = { ins =>
evaluator.eval(functionInvocation(fd, ins)) match {
diff --git a/src/main/scala/leon/solvers/ADTManager.scala b/src/main/scala/leon/solvers/ADTManager.scala
index e2deeb2d5b3d0112ff27edbe927db0f21e36a830..9e3c20a9e3997f1f65d874e6761aff54935f9761 100644
--- a/src/main/scala/leon/solvers/ADTManager.scala
+++ b/src/main/scala/leon/solvers/ADTManager.scala
@@ -70,7 +70,15 @@ class ADTManager(ctx: LeonContext) {
def forEachType(t: TypeTree)(f: TypeTree => Unit): Unit = t match {
case NAryType(tps, builder) =>
f(t)
- tps.foreach(forEachType(_)(f))
+ // note: each of the tps could be abstract classes in which case we need to
+ // lock their dependencies, transitively.
+ tps.foreach {
+ case ct: ClassType =>
+ val (root, sub) = getHierarchy(ct)
+ (root +: sub).flatMap(_.fields.map(_.getType)).foreach(subt => forEachType(subt)(f))
+ case othert =>
+ forEachType(othert)(f)
+ }
}
protected def findDependencies(t: TypeTree): Unit = t match {
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 835d352ed7fe544b2f22c109bf3b3c6ca47d6315..292ef160541ac0dd2d0e431feacba6790f1da90b 100644
--- a/src/main/scala/leon/solvers/EvaluatingSolver.scala
+++ b/src/main/scala/leon/solvers/EvaluatingSolver.scala
@@ -7,15 +7,14 @@ import purescala.Definitions._
import evaluators._
trait EvaluatingSolver extends Solver {
- val context: LeonContext
val program: Program
val useCodeGen: Boolean
- lazy val evaluator: DeterministicEvaluator =
- if (useCodeGen) {
- new CodeGenEvaluator(context, program)
- } else {
- new DefaultEvaluator(context, program)
- }
+ 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 e295adafbb5468eba718b803ca7477d3703a7394..59d9859fb7bcde2f7d048543a9d67c99e381ac42 100644
--- a/src/main/scala/leon/solvers/SolverFactory.scala
+++ b/src/main/scala/leon/solvers/SolverFactory.scala
@@ -13,7 +13,7 @@ import purescala.Definitions._
import scala.reflect.runtime.universe._
import _root_.smtlib.interpreters._
-abstract class SolverFactory[+S <: Solver : TypeTag] {
+abstract class SolverFactory[+S <: Solver] {
def getNewSolver(): S
def shutdown(): Unit = {}
@@ -22,12 +22,13 @@ abstract class SolverFactory[+S <: Solver : TypeTag] {
s.free()
}
- val name = typeOf[S].toString.split("\\.").last.replaceAll("Solver", "")+"*"
+ val name: String
}
object SolverFactory {
- def apply[S <: Solver : TypeTag](builder: () => S): SolverFactory[S] = {
+ def apply[S <: Solver : TypeTag](nme: String, builder: () => S): SolverFactory[S] = {
new SolverFactory[S] {
+ val name = nme
def getNewSolver() = builder()
}
}
@@ -50,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) {
@@ -74,48 +78,34 @@ object SolverFactory {
}
}
- 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 {
- case "fairz3" =>
- SolverFactory(() => new FairZ3Solver(ctx, program) with TimeoutSolver)
-
- case "unrollz3" =>
- SolverFactory(() => new Z3UnrollingSolver(ctx, program, new UninterpretedZ3Solver(ctx, program)) with TimeoutSolver)
-
- case "enum" =>
- SolverFactory(() => new EnumerationSolver(ctx, program) with TimeoutSolver)
-
- case "ground" =>
- SolverFactory(() => new GroundSolver(ctx, program) with TimeoutSolver)
-
- case "smt-z3" =>
- SolverFactory(() => new Z3UnrollingSolver(ctx, program, new SMTLIBZ3Solver(ctx, program)) with TimeoutSolver)
-
- case "smt-z3-q" =>
- SolverFactory(() => new SMTLIBZ3QuantifiedSolver(ctx, program) with TimeoutSolver)
-
- case "smt-cvc4" =>
- SolverFactory(() => new CVC4UnrollingSolver(ctx, program, new SMTLIBCVC4Solver(ctx, program)) with TimeoutSolver)
-
- case "smt-cvc4-proof" =>
- SolverFactory(() => new SMTLIBCVC4ProofSolver(ctx, program) with TimeoutSolver)
-
- case "smt-cvc4-cex" =>
- SolverFactory(() => new SMTLIBCVC4CounterExampleSolver(ctx, program) with TimeoutSolver)
-
- case "isabelle" =>
- new isabelle.IsabelleSolverFactory(ctx, program)
-
+ 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)
+ case "unrollz3" => SolverFactory(name, () => new Z3UnrollingSolver(ctx, program, new UninterpretedZ3Solver(ctx, program)) with TimeoutSolver)
+ case "smt-z3" => SolverFactory(name, () => new Z3UnrollingSolver(ctx, program, new SMTLIBZ3Solver(ctx, program)) with TimeoutSolver)
+ case "smt-z3-q" => SolverFactory(name, () => new SMTLIBZ3QuantifiedSolver(ctx, program) with TimeoutSolver)
+ case "smt-cvc4" => SolverFactory(name, () => new CVC4UnrollingSolver(ctx, program, new SMTLIBCVC4Solver(ctx, program)) with TimeoutSolver)
+ case "smt-cvc4-proof" => SolverFactory(name, () => new SMTLIBCVC4ProofSolver(ctx, program) with TimeoutSolver)
+ case "smt-cvc4-cex" => SolverFactory(name, () => new SMTLIBCVC4CounterExampleSolver(ctx, program) with TimeoutSolver)
+ 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.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))
@@ -137,29 +127,30 @@ object SolverFactory {
// Fast solver used by simplifications, to discharge simple tautologies
def uninterpreted(ctx: LeonContext, program: Program): SolverFactory[TimeoutSolver] = {
val names = ctx.findOptionOrDefault(GlobalOptions.optSelectedSolvers)
-
+ val fromName = getFromName(ctx, program) _
+
if ((names contains "fairz3") && !hasNativeZ3) {
if (hasZ3) {
if (!reported) {
ctx.reporter.warning("The Z3 native interface is not available, falling back to smt-z3.")
reported = true
}
- SolverFactory(() => new SMTLIBZ3Solver(ctx, program) with TimeoutSolver)
+ fromName("smt-z3-u")
} else if (hasCVC4) {
if (!reported) {
ctx.reporter.warning("The Z3 native interface is not available, falling back to smt-cvc4.")
reported = true
}
- SolverFactory(() => new SMTLIBCVC4Solver(ctx, program) with TimeoutSolver)
+ fromName("smt-cvc4-u")
} else {
ctx.reporter.fatalError("No SMT solver available: native Z3 api could not load and 'cvc4' or 'z3' binaries were not found in PATH.")
}
} else if(names contains "smt-cvc4") {
- SolverFactory(() => new SMTLIBCVC4Solver(ctx, program) with TimeoutSolver)
+ fromName("smt-cvc4-u")
} else if(names contains "smt-z3") {
- SolverFactory(() => new SMTLIBZ3Solver(ctx, program) with TimeoutSolver)
+ fromName("smt-z3-u")
} else if ((names contains "fairz3") && hasNativeZ3) {
- SolverFactory(() => new UninterpretedZ3Solver(ctx, program) with TimeoutSolver)
+ fromName("nativez3-u")
} else {
ctx.reporter.fatalError("No SMT solver available: native Z3 api could not load and 'cvc4' or 'z3' binaries were not found in PATH.")
}
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 f6a70043182fc237298c30d3b6ffa5c943233bea..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]])(implicit tag: TypeTag[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,9 @@ 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/combinators/SolverPool.scala b/src/main/scala/leon/solvers/combinators/SolverPool.scala
index 2d38591f69b3bcb3417ab59f335edc5e20543bd0..4df3a27b842167b4788ed2c07e16417fec5f553f 100644
--- a/src/main/scala/leon/solvers/combinators/SolverPool.scala
+++ b/src/main/scala/leon/solvers/combinators/SolverPool.scala
@@ -17,7 +17,9 @@ import scala.reflect.runtime.universe._
* growing/shrinking pool size...
*/
-class SolverPoolFactory[+S <: Solver](ctx: LeonContext, sf: SolverFactory[S])(implicit tag: TypeTag[S]) extends SolverFactory[S] {
+class SolverPoolFactory[+S <: Solver](ctx: LeonContext, sf: SolverFactory[S]) extends SolverFactory[S] {
+
+ val name = "Pool(" + sf.name + ")"
var poolSize = 0
val poolMaxSize = 5
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/isabelle/IsabelleSolverFactory.scala b/src/main/scala/leon/solvers/isabelle/IsabelleSolverFactory.scala
index 0e356aa5559c4d00326971401f3e9c7e79546327..11dfe40d392d1b0bb88fee7e1d7f9f1a2166450b 100644
--- a/src/main/scala/leon/solvers/isabelle/IsabelleSolverFactory.scala
+++ b/src/main/scala/leon/solvers/isabelle/IsabelleSolverFactory.scala
@@ -12,6 +12,8 @@ import leon.solvers._
final class IsabelleSolverFactory(context: LeonContext, program: Program) extends SolverFactory[TimeoutSolver] {
+ val name = "isabelle"
+
private val env = IsabelleEnvironment(context, program)
override def shutdown() =
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 70f86f454f2a2f02a4f636efb088a2273a6c359d..c75b140a228f2c8bb2fa280e1ba8b8fb49327c24 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/QuantificationManager.scala b/src/main/scala/leon/solvers/unrolling/QuantificationManager.scala
index 85382cfcdf39a7d1cd77c78a4a76b7ed32a02689..e4fabf2daf1bb200d95e272188223efc9a8c105b 100644
--- a/src/main/scala/leon/solvers/unrolling/QuantificationManager.scala
+++ b/src/main/scala/leon/solvers/unrolling/QuantificationManager.scala
@@ -446,7 +446,7 @@ class QuantificationManager[T](encoder: TemplateEncoder[T]) extends LambdaManage
(qarg, arg) <- (qargs zip args)
_ = strictnessCnstr(qarg, arg)
} qarg match {
- case Left(quant) if subst.isDefinedAt(quant) =>
+ case Left(quant) if !quantified(quant) || subst.isDefinedAt(quant) =>
eqConstraints += (quant -> arg.encoded)
case Left(quant) if quantified(quant) =>
subst += quant -> arg
diff --git a/src/main/scala/leon/solvers/unrolling/UnrollingSolver.scala b/src/main/scala/leon/solvers/unrolling/UnrollingSolver.scala
index 03431b57720647b4017c3857d6146a615cc679b4..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)
@@ -215,7 +213,7 @@ trait AbstractUnrollingSolver[T]
val newExpr = model.toSeq.foldLeft(expr){
case (e, (k, v)) => let(k, v, e)
}
-
+
evaluator.eval(newExpr) match {
case EvaluationResults.Successful(BooleanLiteral(true)) =>
reporter.debug("- Model validated.")
@@ -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/main/scala/leon/synthesis/ExamplesFinder.scala b/src/main/scala/leon/synthesis/ExamplesFinder.scala
index 52756108c029ff7fcad5d0f2a0e6aaceb3d6770c..08f6513ba0f084cf0e90e1eb11ccacdd2f3a2d4b 100644
--- a/src/main/scala/leon/synthesis/ExamplesFinder.scala
+++ b/src/main/scala/leon/synthesis/ExamplesFinder.scala
@@ -119,7 +119,7 @@ class ExamplesFinder(ctx0: LeonContext, program: Program) {
def generateForPC(ids: List[Identifier], pc: Expr, ctx: LeonContext, maxValid: Int = 400, maxEnumerated: Int = 1000): ExamplesBank = {
//println(program.definedClasses)
- val evaluator = new CodeGenEvaluator(ctx, program, CodeGenParams.default)
+ val evaluator = new CodeGenEvaluator(ctx, program)
val datagen = new GrammarDataGen(evaluator, ValueGrammar)
val solverF = SolverFactory.getFromSettings(ctx, program)
val solverDataGen = new SolverDataGen(ctx, program, solverF)
diff --git a/src/main/scala/leon/synthesis/rules/CEGISLike.scala b/src/main/scala/leon/synthesis/rules/CEGISLike.scala
index 41e82c459b70fa61da686a89a1041433f6a599e4..1247edf3357e91eb9ce6535cdc4db868e4628542 100644
--- a/src/main/scala/leon/synthesis/rules/CEGISLike.scala
+++ b/src/main/scala/leon/synthesis/rules/CEGISLike.scala
@@ -798,7 +798,7 @@ abstract class CEGISLike(name: String) extends Rule(name) {
if (useVanuatoo) {
new VanuatooDataGen(hctx, hctx.program).generateFor(p.as, p.pc.toClause, nTests, 3000).map(InExample)
} else {
- val evaluator = new DualEvaluator(hctx, hctx.program, CodeGenParams.default)
+ val evaluator = new DualEvaluator(hctx, hctx.program)
new GrammarDataGen(evaluator, ValueGrammar).generateFor(p.as, p.pc.toClause, nTests, 1000).map(InExample)
}
}
diff --git a/src/main/scala/leon/synthesis/rules/unused/BottomUpTegis.scala b/src/main/scala/leon/synthesis/rules/unused/BottomUpTegis.scala
index 9f5dff95eed832330677112833987e32da01c35f..212ba7f6ae73746eaf14b2c32e7fe2f3b9cff244 100644
--- a/src/main/scala/leon/synthesis/rules/unused/BottomUpTegis.scala
+++ b/src/main/scala/leon/synthesis/rules/unused/BottomUpTegis.scala
@@ -41,7 +41,7 @@ abstract class BottomUpTEGISLike(name: String) extends Rule(name) {
val evalParams = CodeGenParams.default.copy(maxFunctionInvocations = 2000)
//val evaluator = new CodeGenEvaluator(sctx.context, sctx.program, evalParams)
//val evaluator = new DefaultEvaluator(sctx.context, sctx.program)
- val evaluator = new DualEvaluator(hctx, hctx.program, evalParams)
+ val evaluator = new DualEvaluator(hctx, hctx.program, params = evalParams)
val grammar = getGrammar(hctx, p)
diff --git a/src/main/scala/leon/synthesis/rules/unused/TEGISLike.scala b/src/main/scala/leon/synthesis/rules/unused/TEGISLike.scala
index ee49610d06a4070154df5bfb744925121754f054..fc36521ff86564e9502eb5ec7aea751700f0bc8e 100644
--- a/src/main/scala/leon/synthesis/rules/unused/TEGISLike.scala
+++ b/src/main/scala/leon/synthesis/rules/unused/TEGISLike.scala
@@ -43,7 +43,7 @@ abstract class TEGISLike(name: String) extends Rule(name) {
val inputGenerator: Iterator[Seq[Expr]] = if (useVanuatoo) {
new VanuatooDataGen(hctx, hctx.program).generateFor(p.as, p.pc.toClause, nTests, 3000)
} else {
- val evaluator = new DualEvaluator(hctx, hctx.program, CodeGenParams.default)
+ val evaluator = new DualEvaluator(hctx, hctx.program)
new GrammarDataGen(evaluator, ValueGrammar).generateFor(p.as, p.pc.toClause, nTests, 1000)
}
@@ -63,7 +63,7 @@ abstract class TEGISLike(name: String) extends Rule(name) {
if (gi.nonEmpty) {
val evalParams = CodeGenParams.default.copy(maxFunctionInvocations = 2000)
- val evaluator = new DualEvaluator(hctx, hctx.program, evalParams)
+ val evaluator = new DualEvaluator(hctx, hctx.program, params = evalParams)
val enum = new MemoizedEnumerator[Label, Expr, ProductionRule[Label, Expr]](grammar.getProductions)
diff --git a/src/main/scala/leon/termination/TerminationPhase.scala b/src/main/scala/leon/termination/TerminationPhase.scala
index d5b07f276264c548e9b31a295ca1efdd101e0871..a7802c490efb494f419e8158439d3c8dbe848f3f 100644
--- a/src/main/scala/leon/termination/TerminationPhase.scala
+++ b/src/main/scala/leon/termination/TerminationPhase.scala
@@ -30,6 +30,6 @@ object TerminationPhase extends SimpleLeonPhase[Program, TerminationReport] {
}
val endTime = System.currentTimeMillis
- new TerminationReport(ctx, results, (endTime - startTime).toDouble / 1000.0d)
+ new TerminationReport(ctx, tc.program, results, (endTime - startTime).toDouble / 1000.0d)
}
}
diff --git a/src/main/scala/leon/termination/TerminationReport.scala b/src/main/scala/leon/termination/TerminationReport.scala
index c7fc3a0b3d7a870b7730022da35e7c3fa3f7483d..47ef92268834a47ab584720f7169989def23531b 100644
--- a/src/main/scala/leon/termination/TerminationReport.scala
+++ b/src/main/scala/leon/termination/TerminationReport.scala
@@ -6,8 +6,10 @@ package termination
import purescala.Definitions._
import utils.Report
import utils.ASCIIHelpers._
+import leon.purescala.PrettyPrinter
+import leon.purescala.SelfPrettyPrinter
-case class TerminationReport(ctx: LeonContext, results : Seq[(FunDef,TerminationGuarantee)], time : Double) extends Report {
+case class TerminationReport(ctx: LeonContext, program: Program, results : Seq[(FunDef,TerminationGuarantee)], time : Double) extends Report {
def summaryString : String = {
var t = Table("Termination summary")
@@ -18,7 +20,10 @@ case class TerminationReport(ctx: LeonContext, results : Seq[(FunDef,Termination
val result = if (g.isGuaranteed) "\u2713" else "\u2717"
val verdict = g match {
case LoopsGivenInputs(reason, args) =>
- "Non-terminating for call: " + args.mkString(fd.id + "(", ",", ")")
+ val niceArgs = args.map { v =>
+ SelfPrettyPrinter.print(v, PrettyPrinter(v))(ctx, program)
+ }
+ "Non-terminating for call: " + niceArgs.mkString(fd.id + "(", ",", ")")
case CallsNonTerminating(funDefs) =>
"Calls non-terminating functions " + funDefs.map(_.id).mkString(",")
case Terminates(reason) =>
diff --git a/src/test/scala/leon/integration/evaluators/CodegenEvaluatorSuite.scala b/src/test/scala/leon/integration/evaluators/CodegenEvaluatorSuite.scala
index 8882238999acebde711027ec6a8b1db152813b20..e0e1b2b85b35b03170660730c41ea06183eaaf0a 100644
--- a/src/test/scala/leon/integration/evaluators/CodegenEvaluatorSuite.scala
+++ b/src/test/scala/leon/integration/evaluators/CodegenEvaluatorSuite.scala
@@ -330,7 +330,7 @@ class CodegenEvaluatorSuite extends LeonTestSuiteWithProgram with helpers.Expres
val testName = f"$name%-20s $opts%-18s"
test("Evaluation of "+testName) { implicit fix =>
- val eval = new CodeGenEvaluator(fix._1, fix._2, CodeGenParams(
+ val eval = new CodeGenEvaluator(fix._1, fix._2, params = CodeGenParams(
maxFunctionInvocations = if (requireMonitor) 1000 else -1, // Monitor calls and abort execution if more than X calls
checkContracts = true, // Generate calls that checks pre/postconditions
doInstrument = doInstrument // Instrument reads to case classes (mainly for vanuatoo)
diff --git a/src/test/scala/leon/integration/evaluators/EvaluatorSuite.scala b/src/test/scala/leon/integration/evaluators/EvaluatorSuite.scala
index bf828a9fb07ae255ad78c7ab71f3e76eb7cee02e..e0c1537166cdca38c05c430df0f6bd3e5a5621d0 100644
--- a/src/test/scala/leon/integration/evaluators/EvaluatorSuite.scala
+++ b/src/test/scala/leon/integration/evaluators/EvaluatorSuite.scala
@@ -399,7 +399,7 @@ class EvaluatorSuite extends LeonTestSuiteWithProgram with ExpressionsDSL {
}
test("Infinite Recursion") { implicit fix =>
- val e = new CodeGenEvaluator(fix._1, fix._2, CodeGenParams.default.copy(maxFunctionInvocations = 32))
+ val e = new CodeGenEvaluator(fix._1, fix._2, params = CodeGenParams.default.copy(maxFunctionInvocations = 32))
eval(e, fcall("Recursion.c")(i(42))).failed
}
diff --git a/src/test/scala/leon/integration/purescala/SimplifyPathsSuite.scala b/src/test/scala/leon/integration/purescala/SimplifyPathsSuite.scala
index bd477c54a30bbd3dbeb938db0566d166ad498f5a..c95b75e3ea3603ff773e9621498c30095c16e033 100644
--- a/src/test/scala/leon/integration/purescala/SimplifyPathsSuite.scala
+++ b/src/test/scala/leon/integration/purescala/SimplifyPathsSuite.scala
@@ -25,7 +25,7 @@ class SimplifyPathsSuite extends LeonTestSuite {
val l2 = InfiniteIntegerLiteral(2)
def simplifyPaths(ctx: LeonContext, expr: Expr): Expr = {
- val uninterpretedZ3 = SolverFactory(() => new UninterpretedZ3Solver(ctx, Program.empty))
+ val uninterpretedZ3 = SolverFactory.getFromName(ctx, Program.empty)("nativez3-u")
try {
ExprOps.simplifyPaths(uninterpretedZ3)(expr)
} finally {
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 e491737cdc12adcfd9331396e7cde874ee4c8c55..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(() => (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 eba92b1f00039287753a1db5a3e5b3bb660fd718..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(() => new DummySolver(ctx, Program.empty))
+ SolverFactory("dummy", () => new DummySolver(ctx.toSctx, Program.empty))
}
val poolSize = 5;
diff --git a/testcases/verification/xlang/GuessNumber.scala b/testcases/verification/xlang/GuessNumber.scala
deleted file mode 100644
index ca1ea724a51d25f3652092e1644259ba07013e5c..0000000000000000000000000000000000000000
--- a/testcases/verification/xlang/GuessNumber.scala
+++ /dev/null
@@ -1,35 +0,0 @@
-import leon.lang._
-import leon.lang.xlang._
-import leon.util.Random
-
-object GuessNumber {
-
- def pickRandomly(min: BigInt, max: BigInt): BigInt = {
- require(min >= 0 && max >= min)
- Random.nextBigInt(max - min + 1) + min
- }
-
- def main(): Unit = {
- val choice = pickRandomly(0, 10)
-
- var guess = pickRandomly(0, 10)
- var top: BigInt = 10
- var bot: BigInt = 0
-
- (while(bot < top) {
- if(isGreater(guess, choice)) {
- top = guess-1
- guess = pickRandomly(bot, top)
- } else if(isSmaller(guess, choice)) {
- bot = guess+1
- guess = pickRandomly(bot, top)
- }
- }) invariant(guess >= bot && guess <= top && bot >= 0 && top <= 10 && bot <= top && choice >= bot && choice <= top)
- val answer = bot
- assert(answer == choice)
- }
-
- def isGreater(guess: BigInt, choice: BigInt): Boolean = guess > choice
- def isSmaller(guess: BigInt, choice: BigInt): Boolean = guess < choice
-
-}
diff --git a/testcases/verification/xlang/GuessNumberInteractive.scala b/testcases/verification/xlang/io/GuessNumber.scala
similarity index 98%
rename from testcases/verification/xlang/GuessNumberInteractive.scala
rename to testcases/verification/xlang/io/GuessNumber.scala
index 85b083bba201f064c97224dedbcefd7a715defcb..46bf0d99a556aef8e49bab51bbfa05553b89993b 100644
--- a/testcases/verification/xlang/GuessNumberInteractive.scala
+++ b/testcases/verification/xlang/io/GuessNumber.scala
@@ -4,7 +4,7 @@ import leon.io.StdIn
import leon.annotation._
-object GuessNumberInteractive {
+object GuessNumber {
@extern
def pickBetween(bot: BigInt, top: BigInt): BigInt = {