diff --git a/src/main/scala/leon/LeonContext.scala b/src/main/scala/leon/LeonContext.scala
index e2145ed872e5cb3c397104b30b8538cad7f4a127..d41a4136ffa7d7d597bd6a4a6e447885d3aa79fd 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 a2ceda071014c39319323b067db1b6c3a65dcb56..4678772d2468775867998cc045613be94081f882 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 080e7d03862507899d97d9e288e04041a304ec89..9cf1040b3163d24d7f445023ada714bd00423e0a 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 6ac173414f6b483c83cd0372e3b1d02f1ecf5c8f..3bc724c68873238e6ef8195cb5410b1ee83c6ffe 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 3b44cae39cc712763670dd332b97e453d26a085d..f5e37ca29936f7bd874416674996930eb02f3ab7 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 b31a083be787ac6d663b839e228b3bda300d709d..f6c546306b96398a6eab4785ca8e3c671dfe6929 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 6fa76d0bf9328f983ec2fd6de4fd27bbed6b5e6d..2c1de0e4b2be7603d7b9a42c1bc6eeca857f505d 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 b75c157d84d013ea57b4b6d39dadebc2997d49b1..17fac01f03f856d487d1d393c16aaa5dce355a52 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 20992d2e342348a76bf8324a55d8f09f2daf8546..e0de253ce804186d80fd9f692b765c4042d6be09 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 20341ff939c00c785024c249c92cd07c3c7ae3e7..9087c942cc82b129d46ea30b2c6caa46ae8e1403 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 74aef6fcda4d54622fb1ccbf0412b8cee8e3d7d8..08b27c9ed72f54fcbab108f3c25644280c95a8e7 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 cd8f11d336d12f854276d28b487ac6622218b46c..f11526f3c2c7c1af909909cce4120c9621c9962c 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 a6ea6b654397376802d8c98c8010bc7645f9cd65..2901bb3827846116cc7f2021974b7c6c6823e141 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 0502be54025994358d0141f98d908df134befb25..0876e17219def0126a1ac5bc18999b8e0fa06136 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 708a3a7564f3366fbc8ce6849f891b91e5abee3f..5885531e8c0c9733c1b6cf8c16667923f1423c29 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 77cebb21160c472b0d64f0d7ec3fb90b5943e47d..2d4b29f7e9e084202196e672fda749b65728aa3e 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 12953a93b1abf88af4eea0765ce4dfbc3a71032a..1ec1084e0b978a6b1227595e3a53f223a610953b 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 ae3be5513adca026f6ad5e28ac70425864c5a62c..c77406e25c833685e370603f80067146e4fd12b9 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 c650efe8863d1a86eedbe7e3bc0c35932e7a0b40..569dba2a4f131e395c9d86294f170ea1c19b4afc 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 1902dbab52ad7135254e70fcc5effda9aefee241..8fd0458ae436246582436e016775c93039194f45 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 1ae79ce1d04505eabfe7c49c57463864d9735c6d..2a68caa854c00ad471811ee54e544617512f9d45 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)