From deca849d35f914c7172b6ae91f5c5d2f856569a0 Mon Sep 17 00:00:00 2001
From: Philippe Suter <philippe.suter@gmail.com>
Date: Mon, 26 Nov 2012 13:09:40 +0100
Subject: [PATCH] The full `LeonContext` is now passed to `Solver`s.
---
src/main/scala/leon/LeonContext.scala | 4 +++-
src/main/scala/leon/LeonOption.scala | 4 +++-
src/main/scala/leon/isabelle/Main.scala | 8 ++++++--
src/main/scala/leon/solvers/ParallelSolver.scala | 5 ++++-
src/main/scala/leon/solvers/RandomSolver.scala | 5 ++++-
src/main/scala/leon/solvers/Solver.scala | 2 +-
src/main/scala/leon/solvers/TimeoutSolver.scala | 2 +-
src/main/scala/leon/solvers/TrivialSolver.scala | 2 +-
src/main/scala/leon/solvers/z3/AbstractZ3Solver.scala | 3 ++-
src/main/scala/leon/solvers/z3/FairZ3Solver.scala | 2 +-
.../scala/leon/solvers/z3/UninterpretedZ3Solver.scala | 2 +-
src/main/scala/leon/synthesis/ParallelSearch.scala | 3 ++-
src/main/scala/leon/synthesis/SynthesisPhase.scala | 6 +++---
src/main/scala/leon/testgen/TestGeneration.scala | 9 ++++++---
src/main/scala/leon/verification/Analyser.scala | 5 +++--
src/main/scala/leon/verification/Analysis.scala | 7 ++++---
src/main/scala/leon/verification/AnalysisPhase.scala | 2 +-
src/test/scala/leon/test/purescala/TreeOpsTests.scala | 8 +++++---
.../scala/leon/test/solvers/z3/BugWithEmptySet.scala | 9 +++++----
.../scala/leon/test/solvers/z3/FairZ3SolverTests.scala | 9 +++++----
.../test/solvers/z3/UninterpretedZ3SolverTests.scala | 9 +++++----
21 files changed, 66 insertions(+), 40 deletions(-)
diff --git a/src/main/scala/leon/LeonContext.scala b/src/main/scala/leon/LeonContext.scala
index e2145ed87..d41a4136f 100644
--- a/src/main/scala/leon/LeonContext.scala
+++ b/src/main/scala/leon/LeonContext.scala
@@ -3,10 +3,12 @@ package leon
import purescala.Definitions.Program
import java.io.File
+/** Everything that is part of a compilation unit, except the actual program tree.
+ * Contexts are immutable, and so should all there fields (with the possible
+ * exception of the reporter). */
case class LeonContext(
val settings: Settings = Settings(),
val options: List[LeonOption] = Nil,
val files: List[File] = Nil,
val reporter: Reporter = new DefaultReporter
)
-
diff --git a/src/main/scala/leon/LeonOption.scala b/src/main/scala/leon/LeonOption.scala
index a2ceda071..4678772d2 100644
--- a/src/main/scala/leon/LeonOption.scala
+++ b/src/main/scala/leon/LeonOption.scala
@@ -1,12 +1,14 @@
package leon
+/** Describes a command-line option. */
sealed abstract class LeonOption {
val name: String
}
+/** Boolean (on/off) options. Present means "on". */
case class LeonFlagOption(name: String) extends LeonOption
+/** Options of the form --option=value. */
case class LeonValueOption(name: String, value: String) extends LeonOption {
-
def splitList : Seq[String] = value.split(':').map(_.trim).filter(!_.isEmpty)
}
diff --git a/src/main/scala/leon/isabelle/Main.scala b/src/main/scala/leon/isabelle/Main.scala
index 080e7d038..9cf1040b3 100644
--- a/src/main/scala/leon/isabelle/Main.scala
+++ b/src/main/scala/leon/isabelle/Main.scala
@@ -1,4 +1,5 @@
-package leon.isabelle
+package leon
+package isabelle
import leon.Reporter
import leon.Settings._
@@ -17,10 +18,13 @@ import java.lang.StringBuffer
import java.io._
import scala.collection.mutable.ListMap
-class Main(reporter: Reporter) extends Analyser(reporter) {
+@deprecated("Unused, Untested, Unmaintained.", "")
+class Main(context : LeonContext) extends Analyser(context) {
val description = "Generates Isabelle source"
val shortDescription = "isabelle"
+ private val reporter = context.reporter
+
var mapParentTypes = new ListMap[String, String]
//map for each function keeps the functions that it calls inside it
diff --git a/src/main/scala/leon/solvers/ParallelSolver.scala b/src/main/scala/leon/solvers/ParallelSolver.scala
index 6ac173414..3bc724c68 100644
--- a/src/main/scala/leon/solvers/ParallelSolver.scala
+++ b/src/main/scala/leon/solvers/ParallelSolver.scala
@@ -14,10 +14,13 @@ import scala.actors.Actor._
import scala.concurrent.Lock
-class ParallelSolver(solvers: Solver*) extends Solver(solvers(0).reporter) {
+@deprecated("Unused, Untested, Unmaintained", "")
+class ParallelSolver(solvers : Solver*) extends Solver(solvers(0).context) {
private val nbSolvers = solvers.size
require(nbSolvers >= 2)
+ private val reporter = context.reporter
+
val description = "Solver running subsolvers in parallel " + solvers.map(_.description).mkString("(", ", ", ")")
override val shortDescription = solvers.map(_.shortDescription).mkString("//")
override val superseeds : Seq[String] = solvers.map(_.shortDescription).toSeq
diff --git a/src/main/scala/leon/solvers/RandomSolver.scala b/src/main/scala/leon/solvers/RandomSolver.scala
index 3b44cae39..f5e37ca29 100644
--- a/src/main/scala/leon/solvers/RandomSolver.scala
+++ b/src/main/scala/leon/solvers/RandomSolver.scala
@@ -11,9 +11,12 @@ import Evaluator._
import scala.util.Random
-class RandomSolver(reporter: Reporter, val nbTrial: Option[Int] = None) extends Solver(reporter) {
+@deprecated("Unused, Untested, Unmaintained", "")
+class RandomSolver(context: LeonContext, val nbTrial: Option[Int] = None) extends Solver(context) {
require(nbTrial.forall(i => i >= 0))
+ private val reporter = context.reporter
+
val description = "Solver applying random testing (QuickCheck-like)"
override val shortDescription = "QC"
diff --git a/src/main/scala/leon/solvers/Solver.scala b/src/main/scala/leon/solvers/Solver.scala
index b31a083be..f6c546306 100644
--- a/src/main/scala/leon/solvers/Solver.scala
+++ b/src/main/scala/leon/solvers/Solver.scala
@@ -6,7 +6,7 @@ import purescala.Definitions._
import purescala.TreeOps._
import purescala.Trees._
-abstract class Solver(val reporter: Reporter) {
+abstract class Solver(val context : LeonContext) {
// This used to be in Extension
val description : String
val shortDescription : String
diff --git a/src/main/scala/leon/solvers/TimeoutSolver.scala b/src/main/scala/leon/solvers/TimeoutSolver.scala
index 6fa76d0bf..2c1de0e4b 100644
--- a/src/main/scala/leon/solvers/TimeoutSolver.scala
+++ b/src/main/scala/leon/solvers/TimeoutSolver.scala
@@ -8,7 +8,7 @@ import purescala.TypeTrees._
import scala.sys.error
-class TimeoutSolver(solver : Solver, timeout : Int) extends Solver(solver.reporter) {
+class TimeoutSolver(solver : Solver, timeout : Int) extends Solver(solver.context) {
val description = solver.description + ", with timeout"
override val shortDescription = solver.shortDescription + "+t"
diff --git a/src/main/scala/leon/solvers/TrivialSolver.scala b/src/main/scala/leon/solvers/TrivialSolver.scala
index b75c157d8..17fac01f0 100644
--- a/src/main/scala/leon/solvers/TrivialSolver.scala
+++ b/src/main/scala/leon/solvers/TrivialSolver.scala
@@ -6,7 +6,7 @@ import purescala.Definitions._
import purescala.Trees._
import purescala.TypeTrees._
-class TrivialSolver(reporter: Reporter) extends Solver(reporter) {
+class TrivialSolver(context: LeonContext) extends Solver(context) {
val description = "Solver for syntactically trivial formulas"
override val shortDescription = "trivial"
diff --git a/src/main/scala/leon/solvers/z3/AbstractZ3Solver.scala b/src/main/scala/leon/solvers/z3/AbstractZ3Solver.scala
index 20992d2e3..e0de253ce 100644
--- a/src/main/scala/leon/solvers/z3/AbstractZ3Solver.scala
+++ b/src/main/scala/leon/solvers/z3/AbstractZ3Solver.scala
@@ -16,7 +16,8 @@ import scala.collection.mutable.{Set => MutableSet}
trait AbstractZ3Solver {
self: leon.solvers.Solver =>
- val reporter: Reporter
+ val context : LeonContext
+ protected[z3] val reporter : Reporter = context.reporter
protected[leon] val USEBV : Boolean = Settings.bitvectorBitwidth.isDefined
protected[leon] val BVWIDTH : Int = Settings.bitvectorBitwidth.getOrElse(-1)
diff --git a/src/main/scala/leon/solvers/z3/FairZ3Solver.scala b/src/main/scala/leon/solvers/z3/FairZ3Solver.scala
index 20341ff93..9087c942c 100644
--- a/src/main/scala/leon/solvers/z3/FairZ3Solver.scala
+++ b/src/main/scala/leon/solvers/z3/FairZ3Solver.scala
@@ -15,7 +15,7 @@ import purescala.TypeTrees._
import scala.collection.mutable.{Map => MutableMap}
import scala.collection.mutable.{Set => MutableSet}
-class FairZ3Solver(reporter: Reporter) extends Solver(reporter) with AbstractZ3Solver with Z3ModelReconstruction {
+class FairZ3Solver(context : LeonContext) extends Solver(context) with AbstractZ3Solver with Z3ModelReconstruction {
// have to comment this to use the solver for constraint solving...
// assert(Settings.useFairInstantiator)
diff --git a/src/main/scala/leon/solvers/z3/UninterpretedZ3Solver.scala b/src/main/scala/leon/solvers/z3/UninterpretedZ3Solver.scala
index 74aef6fcd..08b27c9ed 100644
--- a/src/main/scala/leon/solvers/z3/UninterpretedZ3Solver.scala
+++ b/src/main/scala/leon/solvers/z3/UninterpretedZ3Solver.scala
@@ -19,7 +19,7 @@ import purescala.TypeTrees._
* - otherwise it returns UNKNOWN
* Results should come back very quickly.
*/
-class UninterpretedZ3Solver(reporter : Reporter) extends Solver(reporter) with AbstractZ3Solver with Z3ModelReconstruction {
+class UninterpretedZ3Solver(context : LeonContext) extends Solver(context) with AbstractZ3Solver with Z3ModelReconstruction {
val description = "Uninterpreted Z3 Solver"
override val shortDescription = "Z3-u"
diff --git a/src/main/scala/leon/synthesis/ParallelSearch.scala b/src/main/scala/leon/synthesis/ParallelSearch.scala
index cd8f11d33..f11526f3c 100644
--- a/src/main/scala/leon/synthesis/ParallelSearch.scala
+++ b/src/main/scala/leon/synthesis/ParallelSearch.scala
@@ -14,7 +14,8 @@ class ParallelSearch(synth: Synthesizer,
def initWorkerContext(wr: ActorRef) = {
val reporter = new SilentReporter
- val solver = new FairZ3Solver(reporter)
+ // TODO FIXME : the proper LeonContext should make its way here.
+ val solver = new FairZ3Solver(LeonContext(reporter = reporter))
solver.setProgram(synth.program)
SynthesisContext(solver = solver, reporter = synth.reporter)
diff --git a/src/main/scala/leon/synthesis/SynthesisPhase.scala b/src/main/scala/leon/synthesis/SynthesisPhase.scala
index a6ea6b654..2901bb382 100644
--- a/src/main/scala/leon/synthesis/SynthesisPhase.scala
+++ b/src/main/scala/leon/synthesis/SynthesisPhase.scala
@@ -23,12 +23,12 @@ object SynthesisPhase extends LeonPhase[Program, Program] {
)
def run(ctx: LeonContext)(p: Program): Program = {
- val reporter = new SilentReporter
+ val silentContext : LeonContext = ctx.copy(reporter = new SilentReporter)
- val mainSolver = new FairZ3Solver(reporter)
+ val mainSolver = new FairZ3Solver(silentContext)
mainSolver.setProgram(p)
- val uninterpretedZ3 = new UninterpretedZ3Solver(reporter)
+ val uninterpretedZ3 = new UninterpretedZ3Solver(silentContext)
uninterpretedZ3.setProgram(p)
var inPlace = false
diff --git a/src/main/scala/leon/testgen/TestGeneration.scala b/src/main/scala/leon/testgen/TestGeneration.scala
index 0502be540..0876e1721 100644
--- a/src/main/scala/leon/testgen/TestGeneration.scala
+++ b/src/main/scala/leon/testgen/TestGeneration.scala
@@ -1,4 +1,5 @@
-package leon.testgen
+package leon
+package testgen
import leon.verification.Analyser
@@ -13,12 +14,14 @@ import leon.Reporter
import scala.collection.mutable.{Set => MutableSet}
-class TestGeneration(reporter: Reporter) extends Analyser(reporter) {
+@deprecated("Unused, Untested, Unmaintained.", "")
+class TestGeneration(context : LeonContext) extends Analyser(context) {
def description: String = "Generate random testcases"
def shortDescription: String = "test"
- private val z3Solver = new FairZ3Solver(reporter)
+ private val reporter = context.reporter
+ private val z3Solver = new FairZ3Solver(context)
def analyse(program: Program) {
z3Solver.setProgram(program)
diff --git a/src/main/scala/leon/verification/Analyser.scala b/src/main/scala/leon/verification/Analyser.scala
index 708a3a756..5885531e8 100644
--- a/src/main/scala/leon/verification/Analyser.scala
+++ b/src/main/scala/leon/verification/Analyser.scala
@@ -3,8 +3,9 @@ package verification
import purescala.Definitions.Program
-// TODO this class is slowly but surely becoming useless, as we now have a notion of phases.
-abstract class Analyser(reporter: Reporter) {
+// TODO FIXME this class is slowly but surely becoming useless,
+// as we now have a notion of phases.
+abstract class Analyser(context : LeonContext) {
// Does whatever the analysis should. Uses the reporter to
// signal results and/or errors.
def analyse(program: Program) : Unit
diff --git a/src/main/scala/leon/verification/Analysis.scala b/src/main/scala/leon/verification/Analysis.scala
index 77cebb211..2d4b29f7e 100644
--- a/src/main/scala/leon/verification/Analysis.scala
+++ b/src/main/scala/leon/verification/Analysis.scala
@@ -12,11 +12,12 @@ import solvers.z3.FairZ3Solver
import scala.collection.mutable.{Set => MutableSet}
-class Analysis(val program : Program, val reporter: Reporter) {
+class Analysis(val program : Program, val context: LeonContext) {
+ private val reporter = context.reporter
- val trivialSolver = new TrivialSolver(reporter)
+ val trivialSolver = new TrivialSolver(context)
- val fairZ3 = new FairZ3Solver(reporter)
+ val fairZ3 = new FairZ3Solver(context)
val solvers : Seq[Solver] = trivialSolver :: fairZ3 :: Nil
diff --git a/src/main/scala/leon/verification/AnalysisPhase.scala b/src/main/scala/leon/verification/AnalysisPhase.scala
index 12953a93b..1ec1084e0 100644
--- a/src/main/scala/leon/verification/AnalysisPhase.scala
+++ b/src/main/scala/leon/verification/AnalysisPhase.scala
@@ -12,6 +12,6 @@ object AnalysisPhase extends LeonPhase[Program,VerificationReport] {
)
def run(ctx: LeonContext)(program: Program) : VerificationReport = {
- new Analysis(program, ctx.reporter).analyse
+ new Analysis(program, ctx).analyse
}
}
diff --git a/src/test/scala/leon/test/purescala/TreeOpsTests.scala b/src/test/scala/leon/test/purescala/TreeOpsTests.scala
index ae3be5513..c77406e25 100644
--- a/src/test/scala/leon/test/purescala/TreeOpsTests.scala
+++ b/src/test/scala/leon/test/purescala/TreeOpsTests.scala
@@ -1,17 +1,19 @@
package leon.test.purescala
+import leon.LeonContext
+import leon.SilentReporter
+
import leon.purescala.Common._
import leon.purescala.Definitions._
import leon.purescala.Trees._
import leon.purescala.TypeTrees._
import leon.purescala.TreeOps._
import leon.purescala.LikelyEq
-import leon.SilentReporter
import org.scalatest.FunSuite
class TreeOpsTests extends FunSuite {
- private val silentReporter = new SilentReporter
+ private val silentContext = LeonContext(reporter = new SilentReporter)
private val emptyProgram = Program(
FreshIdentifier("Empty"),
@@ -20,7 +22,7 @@ class TreeOpsTests extends FunSuite {
test("Path-aware simplifications") {
import leon.solvers.z3.UninterpretedZ3Solver
- val solver = new UninterpretedZ3Solver(silentReporter)
+ val solver = new UninterpretedZ3Solver(silentContext)
solver.setProgram(emptyProgram)
// TODO actually testing something here would be better, sorry
diff --git a/src/test/scala/leon/test/solvers/z3/BugWithEmptySet.scala b/src/test/scala/leon/test/solvers/z3/BugWithEmptySet.scala
index c650efe88..569dba2a4 100644
--- a/src/test/scala/leon/test/solvers/z3/BugWithEmptySet.scala
+++ b/src/test/scala/leon/test/solvers/z3/BugWithEmptySet.scala
@@ -1,13 +1,14 @@
package leon.test.solvers.z3
+import leon.LeonContext
+import leon.SilentReporter
+
import leon.purescala.Common._
import leon.purescala.Definitions._
import leon.purescala.Trees._
import leon.purescala.TreeOps._
import leon.purescala.TypeTrees._
-import leon.SilentReporter
-
import leon.solvers.Solver
import leon.solvers.z3.UninterpretedZ3Solver
@@ -30,8 +31,8 @@ class BugWithEmptySet extends FunSuite {
val f1 = Equals(e1, e2)
- val silentReporter = new SilentReporter
- val solver : Solver = new UninterpretedZ3Solver(silentReporter)
+ val silentContext = LeonContext(reporter = new SilentReporter)
+ val solver : Solver = new UninterpretedZ3Solver(silentContext)
solver.setProgram(emptyProgram)
assert(solver.solve(f1) === Some(true),
diff --git a/src/test/scala/leon/test/solvers/z3/FairZ3SolverTests.scala b/src/test/scala/leon/test/solvers/z3/FairZ3SolverTests.scala
index 1902dbab5..8fd0458ae 100644
--- a/src/test/scala/leon/test/solvers/z3/FairZ3SolverTests.scala
+++ b/src/test/scala/leon/test/solvers/z3/FairZ3SolverTests.scala
@@ -1,13 +1,14 @@
package leon.test.solvers.z3
+import leon.LeonContext
+import leon.SilentReporter
+
import leon.purescala.Common._
import leon.purescala.Definitions._
import leon.purescala.Trees._
import leon.purescala.TreeOps._
import leon.purescala.TypeTrees._
-import leon.SilentReporter
-
import leon.solvers.Solver
import leon.solvers.z3.FairZ3Solver
@@ -38,7 +39,7 @@ class FairZ3SolverTests extends FunSuite {
"Solver should not be able to decide the formula " + expr + "."
)
- private val silentReporter = new SilentReporter
+ private val silentContext = LeonContext(reporter = new SilentReporter)
// def f(fx : Int) : Int = fx + 1
private val fx : Identifier = FreshIdentifier("x").setType(Int32Type)
@@ -56,7 +57,7 @@ class FairZ3SolverTests extends FunSuite {
private val y : Expr = Variable(FreshIdentifier("y").setType(Int32Type))
private def f(e : Expr) : Expr = FunctionInvocation(fDef, e :: Nil)
- private val solver = new FairZ3Solver(silentReporter)
+ private val solver = new FairZ3Solver(silentContext)
solver.setProgram(minimalProgram)
private val tautology1 : Expr = BooleanLiteral(true)
diff --git a/src/test/scala/leon/test/solvers/z3/UninterpretedZ3SolverTests.scala b/src/test/scala/leon/test/solvers/z3/UninterpretedZ3SolverTests.scala
index 1ae79ce1d..2a68caa85 100644
--- a/src/test/scala/leon/test/solvers/z3/UninterpretedZ3SolverTests.scala
+++ b/src/test/scala/leon/test/solvers/z3/UninterpretedZ3SolverTests.scala
@@ -1,13 +1,14 @@
package leon.test.solvers.z3
+import leon.LeonContext
+import leon.SilentReporter
+
import leon.purescala.Common._
import leon.purescala.Definitions._
import leon.purescala.Trees._
import leon.purescala.TreeOps._
import leon.purescala.TypeTrees._
-import leon.SilentReporter
-
import leon.solvers.Solver
import leon.solvers.z3.UninterpretedZ3Solver
@@ -38,7 +39,7 @@ class UninterpretedZ3SolverTests extends FunSuite {
"Solver should not be able to decide the formula " + expr + "."
)
- private val silentReporter = new SilentReporter
+ private val silentContext = LeonContext(reporter = new SilentReporter)
// def f(fx : Int) : Int = fx + 1
private val fx : Identifier = FreshIdentifier("x").setType(Int32Type)
@@ -61,7 +62,7 @@ class UninterpretedZ3SolverTests extends FunSuite {
private def f(e : Expr) : Expr = FunctionInvocation(fDef, e :: Nil)
private def g(e : Expr) : Expr = FunctionInvocation(gDef, e :: Nil)
- private val solver = new UninterpretedZ3Solver(silentReporter)
+ private val solver = new UninterpretedZ3Solver(silentContext)
solver.setProgram(minimalProgram)
private val tautology1 : Expr = BooleanLiteral(true)
--
GitLab