From aad51002d8e49853ece43c1485f01d13f220e913 Mon Sep 17 00:00:00 2001
From: Philippe Suter <philippe.suter@gmail.com>
Date: Fri, 23 Nov 2012 18:32:11 +0100
Subject: [PATCH] No more extensions.
---
src/main/scala/leon/Extensions.scala | 86 -------------------
src/main/scala/leon/Settings.scala | 2 +-
src/main/scala/leon/isabelle/Main.scala | 4 +-
.../isabelle/StrongConnectedComponents.scala | 1 -
.../scala/leon/solvers/ParallelSolver.scala | 1 -
.../scala/leon/solvers/RandomSolver.scala | 1 -
src/main/scala/leon/solvers/Solver.scala | 8 +-
.../scala/leon/solvers/TimeoutSolver.scala | 1 -
.../scala/leon/solvers/TrivialSolver.scala | 1 -
.../leon/solvers/z3/AbstractZ3Solver.scala | 1 -
.../scala/leon/solvers/z3/FairZ3Solver.scala | 1 -
.../solvers/z3/UninterpretedZ3Solver.scala | 1 -
.../solvers/z3/Z3ModelReconstruction.scala | 1 -
.../scala/leon/testgen/TestGeneration.scala | 3 +-
.../scala/leon/verification/Analyser.scala | 4 +-
.../scala/leon/verification/Analysis.scala | 25 +++---
src/main/scala/leon/verification/Tactic.scala | 7 +-
17 files changed, 26 insertions(+), 122 deletions(-)
delete mode 100644 src/main/scala/leon/Extensions.scala
diff --git a/src/main/scala/leon/Extensions.scala b/src/main/scala/leon/Extensions.scala
deleted file mode 100644
index acc1707eb..000000000
--- a/src/main/scala/leon/Extensions.scala
+++ /dev/null
@@ -1,86 +0,0 @@
-package leon
-
-import purescala.Common._
-import purescala.Trees._
-import purescala.TreeOps._
-import purescala.Definitions._
-
-object Extensions {
- import leon.verification.{Analyser,Tactic}
- import leon.solvers.Solver
-
- abstract class Extension(reporter: Reporter) {
- def description: String
- def shortDescription: String = description
- }
-
- // The rest of the code is for dynamically loading extensions
-
- private var allLoaded : Seq[Extension] = Nil
- private var analysisExtensions : Seq[Analyser] = Nil
- private var solverExtensions : Seq[Solver] = Nil
-
- // Returns the list of the newly loaded.
- def loadAll(extensionsReporter : Reporter = Settings.reporter) : Seq[Extension] = {
- val allNames: Seq[String] = Settings.extensionNames
- val loaded = (if(!allNames.isEmpty) {
- val classLoader = Extensions.getClass.getClassLoader
-
- val classes: Seq[Class[_]] = (for(name <- allNames) yield {
- try {
- classLoader.loadClass(name)
- } catch {
- case _ => {
- Settings.reporter.error("Couldn't load extension class " + name)
- null
- }
- }
- }).filter(_ != null)
-
- classes.map(cl => {
- try {
- val cons = cl.getConstructor(classOf[Reporter])
- cons.newInstance(extensionsReporter).asInstanceOf[Extension]
- } catch {
- case _ => {
- Settings.reporter.error("Extension class " + cl.getName + " does not seem to be of a proper type.")
- null
- }
- }
- }).filter(_ != null)
- } else {
- Nil
- })
- if(!loaded.isEmpty) {
- Settings.reporter.info("The following extensions are loaded:\n" + loaded.toList.map(_.description).mkString(" ", "\n ", ""))
- }
- // these extensions are always loaded, unless specified otherwise
- val defaultExtensions: Seq[Extension] = if(Settings.runDefaultExtensions) {
- val z3 : Solver = new solvers.z3.FairZ3Solver(extensionsReporter)
- z3 :: Nil
- } else {
- Nil
- }
-
- allLoaded = defaultExtensions ++ loaded
- analysisExtensions = allLoaded.filter(_.isInstanceOf[Analyser]).map(_.asInstanceOf[Analyser])
- //analysisExtensions = new TestGeneration(extensionsReporter) +: analysisExtensions
-
- val solverExtensions0 = allLoaded.filter(_.isInstanceOf[Solver]).map(_.asInstanceOf[Solver])
- val solverExtensions1 = if(Settings.useQuickCheck) new solvers.RandomSolver(extensionsReporter) +: solverExtensions0 else solverExtensions0
- val solverExtensions2 = if(Settings.useParallel) Seq(new solvers.ParallelSolver(solverExtensions1: _*)) else solverExtensions1
- val solverExtensions3 =
- if(Settings.solverTimeout == None) {
- solverExtensions2
- } else {
- val t = Settings.solverTimeout.get
- solverExtensions2.map(s => new solvers.TimeoutSolver(s, t))
- }
- solverExtensions = solverExtensions3
- loaded
- }
-
- def loadedExtensions : Seq[Extension] = allLoaded
- def loadedAnalysisExtensions : Seq[Analyser] = analysisExtensions
- def loadedSolverExtensions : Seq[Solver] = solverExtensions
-}
diff --git a/src/main/scala/leon/Settings.scala b/src/main/scala/leon/Settings.scala
index f643c3a24..5e2585eb5 100644
--- a/src/main/scala/leon/Settings.scala
+++ b/src/main/scala/leon/Settings.scala
@@ -18,7 +18,7 @@ object Settings {
var useCores : Boolean = false
var pruneBranches : Boolean = false
var solverTimeout : Option[Int] = None
- //var luckyTest : Boolean = true
+ var luckyTest : Boolean = true
var verifyModel : Boolean = true
var useQuickCheck : Boolean = false
var useParallel : Boolean = false
diff --git a/src/main/scala/leon/isabelle/Main.scala b/src/main/scala/leon/isabelle/Main.scala
index 3db02146e..080e7d038 100644
--- a/src/main/scala/leon/isabelle/Main.scala
+++ b/src/main/scala/leon/isabelle/Main.scala
@@ -1,6 +1,5 @@
package leon.isabelle
-import leon.Extensions._
import leon.Reporter
import leon.Settings._
@@ -20,7 +19,8 @@ import scala.collection.mutable.ListMap
class Main(reporter: Reporter) extends Analyser(reporter) {
val description = "Generates Isabelle source"
- override val shortDescription = "isabelle"
+ val shortDescription = "isabelle"
+
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/isabelle/StrongConnectedComponents.scala b/src/main/scala/leon/isabelle/StrongConnectedComponents.scala
index 78eb355ff..497e16884 100644
--- a/src/main/scala/leon/isabelle/StrongConnectedComponents.scala
+++ b/src/main/scala/leon/isabelle/StrongConnectedComponents.scala
@@ -1,6 +1,5 @@
package leon.isabelle
-import leon.Extensions._
import leon.Reporter
import leon.Settings._
diff --git a/src/main/scala/leon/solvers/ParallelSolver.scala b/src/main/scala/leon/solvers/ParallelSolver.scala
index 9a9e39829..6ac173414 100644
--- a/src/main/scala/leon/solvers/ParallelSolver.scala
+++ b/src/main/scala/leon/solvers/ParallelSolver.scala
@@ -5,7 +5,6 @@ import purescala.Common._
import purescala.Definitions._
import purescala.Trees._
import purescala.TypeTrees._
-import Extensions._
import Evaluator._
diff --git a/src/main/scala/leon/solvers/RandomSolver.scala b/src/main/scala/leon/solvers/RandomSolver.scala
index 89c0c6752..3b44cae39 100644
--- a/src/main/scala/leon/solvers/RandomSolver.scala
+++ b/src/main/scala/leon/solvers/RandomSolver.scala
@@ -6,7 +6,6 @@ import purescala.Definitions._
import purescala.Trees._
import purescala.TreeOps._
import purescala.TypeTrees._
-import Extensions._
import Evaluator._
diff --git a/src/main/scala/leon/solvers/Solver.scala b/src/main/scala/leon/solvers/Solver.scala
index 947f4ce28..b31a083be 100644
--- a/src/main/scala/leon/solvers/Solver.scala
+++ b/src/main/scala/leon/solvers/Solver.scala
@@ -1,14 +1,16 @@
package leon
package solvers
-import Extensions.Extension
-
import purescala.Common._
import purescala.Definitions._
import purescala.TreeOps._
import purescala.Trees._
-abstract class Solver(val reporter: Reporter) extends Extension(reporter) {
+abstract class Solver(val reporter: Reporter) {
+ // This used to be in Extension
+ val description : String
+ val shortDescription : String
+
// This can be used by solvers to "see" the programs from which the
// formulas come. (e.g. to set up some datastructures for the defined
// ADTs, etc.)
diff --git a/src/main/scala/leon/solvers/TimeoutSolver.scala b/src/main/scala/leon/solvers/TimeoutSolver.scala
index 6b08a36f7..6fa76d0bf 100644
--- a/src/main/scala/leon/solvers/TimeoutSolver.scala
+++ b/src/main/scala/leon/solvers/TimeoutSolver.scala
@@ -5,7 +5,6 @@ import purescala.Common._
import purescala.Definitions._
import purescala.Trees._
import purescala.TypeTrees._
-import Extensions._
import scala.sys.error
diff --git a/src/main/scala/leon/solvers/TrivialSolver.scala b/src/main/scala/leon/solvers/TrivialSolver.scala
index 054ae3f93..b75c157d8 100644
--- a/src/main/scala/leon/solvers/TrivialSolver.scala
+++ b/src/main/scala/leon/solvers/TrivialSolver.scala
@@ -5,7 +5,6 @@ import purescala.Common._
import purescala.Definitions._
import purescala.Trees._
import purescala.TypeTrees._
-import Extensions._
class TrivialSolver(reporter: Reporter) extends Solver(reporter) {
val description = "Solver for syntactically trivial formulas"
diff --git a/src/main/scala/leon/solvers/z3/AbstractZ3Solver.scala b/src/main/scala/leon/solvers/z3/AbstractZ3Solver.scala
index 414e8e1a4..20992d2e3 100644
--- a/src/main/scala/leon/solvers/z3/AbstractZ3Solver.scala
+++ b/src/main/scala/leon/solvers/z3/AbstractZ3Solver.scala
@@ -7,7 +7,6 @@ import purescala.Definitions._
import purescala.Trees._
import purescala.TreeOps._
import purescala.TypeTrees._
-import Extensions._
import scala.collection.mutable.{Map => MutableMap}
import scala.collection.mutable.{Set => MutableSet}
diff --git a/src/main/scala/leon/solvers/z3/FairZ3Solver.scala b/src/main/scala/leon/solvers/z3/FairZ3Solver.scala
index 3659bb668..20341ff93 100644
--- a/src/main/scala/leon/solvers/z3/FairZ3Solver.scala
+++ b/src/main/scala/leon/solvers/z3/FairZ3Solver.scala
@@ -11,7 +11,6 @@ import purescala.Trees._
import purescala.Extractors._
import purescala.TreeOps._
import purescala.TypeTrees._
-import Extensions._
import scala.collection.mutable.{Map => MutableMap}
import scala.collection.mutable.{Set => MutableSet}
diff --git a/src/main/scala/leon/solvers/z3/UninterpretedZ3Solver.scala b/src/main/scala/leon/solvers/z3/UninterpretedZ3Solver.scala
index 2e2a7cf6f..74aef6fcd 100644
--- a/src/main/scala/leon/solvers/z3/UninterpretedZ3Solver.scala
+++ b/src/main/scala/leon/solvers/z3/UninterpretedZ3Solver.scala
@@ -11,7 +11,6 @@ import purescala.Trees._
import purescala.Extractors._
import purescala.TreeOps._
import purescala.TypeTrees._
-import Extensions._
/** This is a rather direct mapping to Z3, where all functions are left uninterpreted.
* It reports the results as follows (based on the negation of the formula):
diff --git a/src/main/scala/leon/solvers/z3/Z3ModelReconstruction.scala b/src/main/scala/leon/solvers/z3/Z3ModelReconstruction.scala
index 5fc00acd0..2e65ca7e5 100644
--- a/src/main/scala/leon/solvers/z3/Z3ModelReconstruction.scala
+++ b/src/main/scala/leon/solvers/z3/Z3ModelReconstruction.scala
@@ -7,7 +7,6 @@ import purescala.Definitions._
import purescala.Trees._
import purescala.TreeOps._
import purescala.TypeTrees._
-import Extensions._
trait Z3ModelReconstruction {
self: AbstractZ3Solver =>
diff --git a/src/main/scala/leon/testgen/TestGeneration.scala b/src/main/scala/leon/testgen/TestGeneration.scala
index 3b76352b2..0502be540 100644
--- a/src/main/scala/leon/testgen/TestGeneration.scala
+++ b/src/main/scala/leon/testgen/TestGeneration.scala
@@ -8,7 +8,6 @@ import leon.purescala.Trees._
import leon.purescala.TreeOps._
import leon.purescala.TypeTrees._
import leon.purescala.ScalaPrinter
-import leon.Extensions._
import leon.solvers.z3.FairZ3Solver
import leon.Reporter
@@ -17,7 +16,7 @@ import scala.collection.mutable.{Set => MutableSet}
class TestGeneration(reporter: Reporter) extends Analyser(reporter) {
def description: String = "Generate random testcases"
- override def shortDescription: String = "test"
+ def shortDescription: String = "test"
private val z3Solver = new FairZ3Solver(reporter)
diff --git a/src/main/scala/leon/verification/Analyser.scala b/src/main/scala/leon/verification/Analyser.scala
index 84a2d8722..708a3a756 100644
--- a/src/main/scala/leon/verification/Analyser.scala
+++ b/src/main/scala/leon/verification/Analyser.scala
@@ -1,12 +1,10 @@
package leon
package verification
-import Extensions.Extension
-
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) extends Extension(reporter) {
+abstract class Analyser(reporter: Reporter) {
// 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 1521ad8e1..77cebb211 100644
--- a/src/main/scala/leon/verification/Analysis.scala
+++ b/src/main/scala/leon/verification/Analysis.scala
@@ -7,22 +7,20 @@ import purescala.Trees._
import purescala.TreeOps._
import purescala.TypeTrees._
-import Extensions._
-
import solvers.{Solver,TrivialSolver}
+import solvers.z3.FairZ3Solver
import scala.collection.mutable.{Set => MutableSet}
class Analysis(val program : Program, val reporter: Reporter) {
- Extensions.loadAll(reporter)
- val analysisExtensions: Seq[Analyser] = loadedAnalysisExtensions
+ val trivialSolver = new TrivialSolver(reporter)
- val trivialSolver = new TrivialSolver(reporter) // This one you can't disable :D
+ val fairZ3 = new FairZ3Solver(reporter)
- val solverExtensions: Seq[Solver] = trivialSolver +: loadedSolverExtensions
+ val solvers : Seq[Solver] = trivialSolver :: fairZ3 :: Nil
- solverExtensions.foreach(_.setProgram(program))
+ solvers.foreach(_.setProgram(program))
val defaultTactic = new DefaultTactic(reporter)
defaultTactic.setProgram(program)
@@ -40,7 +38,7 @@ class Analysis(val program : Program, val reporter: Reporter) {
FunctionTemplate.mkTemplate(funDef)
}
- val report = if(solverExtensions.size > 1) {
+ val report = if(solvers.size > 1) {
reporter.info("Running verification condition generation...")
checkVerificationConditions(generateVerificationConditions)
} else {
@@ -48,10 +46,11 @@ class Analysis(val program : Program, val reporter: Reporter) {
VerificationReport.emptyReport
}
- analysisExtensions.foreach(ae => {
- reporter.info("Running analysis from extension: " + ae.description)
- ae.analyse(program)
- })
+ // This used to be for additional analyses. They should now just be different phases.
+ // analysisExtensions.foreach(ae => {
+ // reporter.info("Running analysis from extension: " + ae.description)
+ // ae.analyse(program)
+ // })
report
}
@@ -105,7 +104,7 @@ class Analysis(val program : Program, val reporter: Reporter) {
// try all solvers until one returns a meaningful answer
var superseeded : Set[String] = Set.empty[String]
- solverExtensions.find(se => {
+ solvers.find(se => {
reporter.info("Trying with solver: " + se.shortDescription)
if(superseeded(se.shortDescription) || superseeded(se.description)) {
reporter.info("Solver was superseeded. Skipping.")
diff --git a/src/main/scala/leon/verification/Tactic.scala b/src/main/scala/leon/verification/Tactic.scala
index d19752949..3a00f2ab7 100644
--- a/src/main/scala/leon/verification/Tactic.scala
+++ b/src/main/scala/leon/verification/Tactic.scala
@@ -1,11 +1,12 @@
package leon
package verification
-import Extensions.Extension
-
import purescala.Definitions._
-abstract class Tactic(reporter: Reporter) extends Extension(reporter) {
+abstract class Tactic(reporter: Reporter) {
+ val description : String
+ val shortDescription : String
+
def setProgram(program: Program) : Unit = {}
def generatePostconditions(function: FunDef) : Seq[VerificationCondition]
def generatePreconditions(function: FunDef) : Seq[VerificationCondition]
--
GitLab