diff --git a/src/main/scala/leon/codegen/runtime/ChooseEntryPoint.scala b/src/main/scala/leon/codegen/runtime/ChooseEntryPoint.scala
index c5ed3070e4e2d7526d5ec755f55eb6230325b1ed..0316953f1804a6323a85da5a601bab665bdd2ac5 100644
--- a/src/main/scala/leon/codegen/runtime/ChooseEntryPoint.scala
+++ b/src/main/scala/leon/codegen/runtime/ChooseEntryPoint.scala
@@ -9,6 +9,7 @@ import purescala.Definitions._
import purescala.Trees.{Tuple => LeonTuple, _}
import purescala.TreeOps.valuateWithModel
import purescala.TypeTrees._
+import solvers.TimeoutSolver
import solvers.z3._
import codegen.CompilationUnit
@@ -41,7 +42,7 @@ object ChooseEntryPoint {
val tStart = System.currentTimeMillis;
- val solver = new FairZ3Solver(ctx, program).setTimeout(10000L)
+ val solver = (new FairZ3Solver(ctx, program) with TimeoutSolver).setTimeout(10000L)
val inputsMap = (p.as zip inputs).map {
case (id, v) =>
diff --git a/src/main/scala/leon/evaluators/RecursiveEvaluator.scala b/src/main/scala/leon/evaluators/RecursiveEvaluator.scala
index ab78f94dcac73ebf335398305c9dc87313398ec3..0d61de43985b6e345907c5e6a9d581bd691dfd1e 100644
--- a/src/main/scala/leon/evaluators/RecursiveEvaluator.scala
+++ b/src/main/scala/leon/evaluators/RecursiveEvaluator.scala
@@ -9,6 +9,8 @@ import purescala.TreeOps._
import purescala.Trees._
import purescala.TypeTrees._
+import solvers.TimeoutSolver
+
import xlang.Trees._
abstract class RecursiveEvaluator(ctx: LeonContext, prog: Program) extends Evaluator(ctx, prog) {
@@ -370,7 +372,7 @@ abstract class RecursiveEvaluator(ctx: LeonContext, prog: Program) extends Evalu
val tStart = System.currentTimeMillis;
- val solver = new FairZ3Solver(ctx, program).setTimeout(10000L)
+ val solver = (new FairZ3Solver(ctx, program) with TimeoutSolver).setTimeout(10000L)
val inputsMap = p.as.map {
case id =>
diff --git a/src/main/scala/leon/solvers/TimeoutAssumptionSolver.scala b/src/main/scala/leon/solvers/TimeoutAssumptionSolver.scala
index ae59400daba40d71cd5cea4d2aa448cc8ab4974f..bfae8365d27b29d282990f999149399d52a773f6 100644
--- a/src/main/scala/leon/solvers/TimeoutAssumptionSolver.scala
+++ b/src/main/scala/leon/solvers/TimeoutAssumptionSolver.scala
@@ -7,16 +7,14 @@ import purescala.Trees.Expr
trait TimeoutAssumptionSolver extends TimeoutSolver with AssumptionSolver {
- protected def innerCheckAssumptions(assumptions: Set[Expr]): Option[Boolean]
-
- override def checkAssumptions(assumptions: Set[Expr]): Option[Boolean] = {
+ abstract override def checkAssumptions(assumptions: Set[Expr]): Option[Boolean] = {
optTimeout match {
case Some(to) =>
interruptAfter(to) {
- innerCheckAssumptions(assumptions)
+ super.checkAssumptions(assumptions)
}
case None =>
- innerCheckAssumptions(assumptions)
+ super.checkAssumptions(assumptions)
}
}
}
diff --git a/src/main/scala/leon/solvers/TimeoutSolver.scala b/src/main/scala/leon/solvers/TimeoutSolver.scala
index ab98755c24aaf59204edc4f9dd64efec9eb102d1..1f805c3db44d68ba7e07a1373c5b31a496cc1781 100644
--- a/src/main/scala/leon/solvers/TimeoutSolver.scala
+++ b/src/main/scala/leon/solvers/TimeoutSolver.scala
@@ -55,16 +55,14 @@ trait TimeoutSolver extends Solver with Interruptible {
this
}
- protected def innerCheck: Option[Boolean]
-
- override def check: Option[Boolean] = {
+ abstract override def check: Option[Boolean] = {
optTimeout match {
case Some(to) =>
interruptAfter(to) {
- innerCheck
+ super.check
}
case None =>
- innerCheck
+ super.check
}
}
diff --git a/src/main/scala/leon/solvers/z3/AbstractZ3Solver.scala b/src/main/scala/leon/solvers/z3/AbstractZ3Solver.scala
index aebc323478d90bd70049ca3a98dac6075b344760..873388137625de6c28ad579a59d24ac861f3c685 100644
--- a/src/main/scala/leon/solvers/z3/AbstractZ3Solver.scala
+++ b/src/main/scala/leon/solvers/z3/AbstractZ3Solver.scala
@@ -21,9 +21,9 @@ import scala.collection.mutable.{Set => MutableSet}
// with a Z3 instance"
trait AbstractZ3Solver
extends Solver
- with TimeoutAssumptionSolver
with AssumptionSolver
- with IncrementalSolver {
+ with IncrementalSolver
+ with Interruptible {
val context : LeonContext
val program : Program
diff --git a/src/main/scala/leon/solvers/z3/FairZ3Solver.scala b/src/main/scala/leon/solvers/z3/FairZ3Solver.scala
index b863c5ac8e676ec1c1c5cc72875985722cd280fc..71589d58fa81ede5a40c70afc928ca57d4d40fa8 100644
--- a/src/main/scala/leon/solvers/z3/FairZ3Solver.scala
+++ b/src/main/scala/leon/solvers/z3/FairZ3Solver.scala
@@ -354,11 +354,11 @@ class FairZ3Solver(val context : LeonContext, val program: Program)
frameExpressions = frameExpressions.drop(lvl)
}
- def innerCheck: Option[Boolean] = {
+ override def check: Option[Boolean] = {
fairCheck(Set())
}
- def innerCheckAssumptions(assumptions: Set[Expr]): Option[Boolean] = {
+ override def checkAssumptions(assumptions: Set[Expr]): Option[Boolean] = {
fairCheck(assumptions)
}
diff --git a/src/main/scala/leon/solvers/z3/UninterpretedZ3Solver.scala b/src/main/scala/leon/solvers/z3/UninterpretedZ3Solver.scala
index d9f2696caa0f8fe463b68728cb9bf7c5a8105d77..59b0f79fe1446c1923a86e5d7493922283fa4f1a 100644
--- a/src/main/scala/leon/solvers/z3/UninterpretedZ3Solver.scala
+++ b/src/main/scala/leon/solvers/z3/UninterpretedZ3Solver.scala
@@ -76,7 +76,7 @@ class UninterpretedZ3Solver(val context : LeonContext, val program: Program)
solver.assertCnstr(toZ3Formula(expression).get)
}
- def innerCheck: Option[Boolean] = {
+ override def check: Option[Boolean] = {
solver.check match {
case Some(true) =>
if (containsFunCalls) {
@@ -90,7 +90,7 @@ class UninterpretedZ3Solver(val context : LeonContext, val program: Program)
}
}
- def innerCheckAssumptions(assumptions: Set[Expr]): Option[Boolean] = {
+ override def checkAssumptions(assumptions: Set[Expr]): Option[Boolean] = {
variables ++= assumptions.flatMap(variablesOf(_))
solver.checkAssumptions(assumptions.toSeq.map(toZ3Formula(_).get) : _*)
}
diff --git a/src/main/scala/leon/synthesis/SynthesisContext.scala b/src/main/scala/leon/synthesis/SynthesisContext.scala
index adf89f1cc3d441af80e10755adf744e0d3fc6a7e..cd938e9466c1b3369902997ac6f02905155a9974 100644
--- a/src/main/scala/leon/synthesis/SynthesisContext.scala
+++ b/src/main/scala/leon/synthesis/SynthesisContext.scala
@@ -21,11 +21,11 @@ case class SynthesisContext(
) {
def newSolver: SynthesisContext.SynthesisSolver = {
- new FairZ3Solver(context, program)
+ new FairZ3Solver(context, program) with TimeoutAssumptionSolver
}
def newFastSolver: SynthesisContext.SynthesisSolver = {
- new UninterpretedZ3Solver(context, program)
+ new UninterpretedZ3Solver(context, program) with TimeoutAssumptionSolver
}
val solverFactory = SolverFactory(() => newSolver)
diff --git a/src/main/scala/leon/synthesis/Synthesizer.scala b/src/main/scala/leon/synthesis/Synthesizer.scala
index 78e5f20a251ab3a4ed98248e7f772ebddf3a9379..9bb0bda005c5d86367441727add33ae10e052570 100644
--- a/src/main/scala/leon/synthesis/Synthesizer.scala
+++ b/src/main/scala/leon/synthesis/Synthesizer.scala
@@ -81,7 +81,7 @@ class Synthesizer(val context : LeonContext,
val (npr, fds) = solutionToProgram(sol)
- val solverf = SolverFactory(() => new FairZ3Solver(context, npr).setTimeout(timeoutMs))
+ val solverf = SolverFactory(() => (new FairZ3Solver(context, npr) with TimeoutSolver).setTimeout(timeoutMs))
val vcs = generateVerificationConditions(reporter, npr, fds.map(_.id.name))
val vctx = VerificationContext(context, Seq(solverf), context.reporter)
diff --git a/src/main/scala/leon/termination/Processor.scala b/src/main/scala/leon/termination/Processor.scala
index c66333a4fea09c064d0c370a9be30f42f2fc8bd3..6c72adb980c72933092ebd16878147f1ff1eb251 100644
--- a/src/main/scala/leon/termination/Processor.scala
+++ b/src/main/scala/leon/termination/Processor.scala
@@ -99,7 +99,7 @@ trait Solvable { self: Processor =>
val newProgram : Program = program.copy(mainObject = program.mainObject.copy(defs = allDefs))
val context : LeonContext = self.checker.context
- solvers = new TimeoutSolverFactory(SolverFactory(() => new FairZ3Solver(context, newProgram)), 500) :: Nil
+ solvers = new TimeoutSolverFactory(SolverFactory(() => new FairZ3Solver(context, newProgram) with TimeoutSolver), 500) :: Nil
}
}
diff --git a/src/main/scala/leon/testgen/TestGeneration.scala b/src/main/scala/leon/testgen/TestGeneration.scala
index e08e7b1721e714b093079910e3ea0704cadb5245..ce6d2fa6df8661678cc3a8e79c990b8854f235fe 100644
--- a/src/main/scala/leon/testgen/TestGeneration.scala
+++ b/src/main/scala/leon/testgen/TestGeneration.scala
@@ -59,7 +59,7 @@ class TestGeneration(context : LeonContext) {
}
def generatePathConditions(program: Program): Set[Expr] = {
- val z3Solverf = SolverFactory( () => new FairZ3Solver(context, program))
+ val z3Solverf = SolverFactory( () => new FairZ3Solver(context, program) with TimeoutSolver)
val callGraph = new CallGraph(program)
callGraph.writeDotFile("testgen.dot")
@@ -74,7 +74,7 @@ class TestGeneration(context : LeonContext) {
private def generateTestCases(program: Program): Set[Map[Identifier, Expr]] = {
val allPaths = generatePathConditions(program)
- val z3Solverf = SolverFactory( () => new FairZ3Solver(context, program))
+ val z3Solverf = SolverFactory( () => new FairZ3Solver(context, program) with TimeoutSolver)
allPaths.flatMap(pathCond => {
reporter.info("Now considering path condition: " + pathCond)
diff --git a/src/main/scala/leon/verification/AnalysisPhase.scala b/src/main/scala/leon/verification/AnalysisPhase.scala
index 905b37484d719507100ac6df97a54d265a7edb40..dc67963e713459d9392a39420a40849320343aa2 100644
--- a/src/main/scala/leon/verification/AnalysisPhase.scala
+++ b/src/main/scala/leon/verification/AnalysisPhase.scala
@@ -151,7 +151,7 @@ object AnalysisPhase extends LeonPhase[Program,VerificationReport] {
val reporter = ctx.reporter
val baseFactories = Seq(
- SolverFactory(() => new FairZ3Solver(ctx, program))
+ SolverFactory(() => new FairZ3Solver(ctx, program) with TimeoutSolver)
)
val solverFactories = timeout match {
diff --git a/src/test/scala/leon/test/solvers/TimeoutSolverTests.scala b/src/test/scala/leon/test/solvers/TimeoutSolverTests.scala
index edd96fdc19763e4d33f4eb1943fe06f753ab3950..5678bd6277fc3a0f1a44d0be667f9a0bbad8de96 100644
--- a/src/test/scala/leon/test/solvers/TimeoutSolverTests.scala
+++ b/src/test/scala/leon/test/solvers/TimeoutSolverTests.scala
@@ -4,6 +4,7 @@ package leon.test
package solvers
import leon._
+import leon.utils.Interruptible
import leon.solvers._
import leon.solvers.combinators._
import leon.purescala.Common._
@@ -12,13 +13,13 @@ import leon.purescala.Trees._
import leon.purescala.TypeTrees._
class TimeoutSolverTests extends LeonTestSuite {
- private class IdioticSolver(val context : LeonContext, val program: Program) extends Solver with TimeoutSolver {
+ private class IdioticSolver(val context : LeonContext, val program: Program) extends Solver with Interruptible{
val name = "Idiotic"
val description = "Loops"
var interrupted = false
- def innerCheck = {
+ override def check: Option[Boolean] = {
while(!interrupted) {
Thread.sleep(100)
}
@@ -41,7 +42,7 @@ class TimeoutSolverTests extends LeonTestSuite {
}
private def getTOSolver : SolverFactory[Solver] = {
- SolverFactory(() => new IdioticSolver(testContext, Program.empty).setTimeout(1000L))
+ SolverFactory(() => (new IdioticSolver(testContext, Program.empty) with TimeoutSolver).setTimeout(1000L))
}
private def check(sf: SolverFactory[Solver], e: Expr): Option[Boolean] = {