From a3cab185b6275cc299c0063d93da3f924280e1c5 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?R=C3=A9gis=20Blanc?= <regwblanc@gmail.com>
Date: Fri, 31 Jan 2014 16:38:46 +0100
Subject: [PATCH] remove the need for innerXXX methods
Refactor the TimeoutSolver and TimeoutAssumptionSolver so
that they no longer use innerCheck methods. We now only
create solver as subclassing Solver or IncrementalSolver and
implementing the interuptible trait, and we can turn them into
TimeoutSolver at instantiation time with a mixin.
---
.../scala/leon/codegen/runtime/ChooseEntryPoint.scala | 3 ++-
src/main/scala/leon/evaluators/RecursiveEvaluator.scala | 4 +++-
src/main/scala/leon/solvers/TimeoutAssumptionSolver.scala | 8 +++-----
src/main/scala/leon/solvers/TimeoutSolver.scala | 8 +++-----
src/main/scala/leon/solvers/z3/AbstractZ3Solver.scala | 4 ++--
src/main/scala/leon/solvers/z3/FairZ3Solver.scala | 4 ++--
.../scala/leon/solvers/z3/UninterpretedZ3Solver.scala | 4 ++--
src/main/scala/leon/synthesis/SynthesisContext.scala | 4 ++--
src/main/scala/leon/synthesis/Synthesizer.scala | 2 +-
src/main/scala/leon/termination/Processor.scala | 2 +-
src/main/scala/leon/testgen/TestGeneration.scala | 4 ++--
src/main/scala/leon/verification/AnalysisPhase.scala | 2 +-
src/test/scala/leon/test/solvers/TimeoutSolverTests.scala | 7 ++++---
13 files changed, 28 insertions(+), 28 deletions(-)
diff --git a/src/main/scala/leon/codegen/runtime/ChooseEntryPoint.scala b/src/main/scala/leon/codegen/runtime/ChooseEntryPoint.scala
index c5ed3070e..0316953f1 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 ab78f94dc..0d61de439 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 ae59400da..bfae8365d 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 ab98755c2..1f805c3db 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 aebc32347..873388137 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 b863c5ac8..71589d58f 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 d9f2696ca..59b0f79fe 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 adf89f1cc..cd938e946 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 78e5f20a2..9bb0bda00 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 c66333a4f..6c72adb98 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 e08e7b172..ce6d2fa6d 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 905b37484..dc67963e7 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 edd96fdc1..5678bd627 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] = {
--
GitLab