From 9b9c91dcb9bc3909884b3bc4d6da225f95b54758 Mon Sep 17 00:00:00 2001
From: Philippe Suter <philippe.suter@gmail.com>
Date: Mon, 12 Jul 2010 14:05:59 +0000
Subject: [PATCH] moved list of extensions to, well, Extensions
---
src/purescala/Analysis.scala | 25 +++--------------------
src/purescala/Extensions.scala | 36 +++++++++++++++++++++++++++++++---
2 files changed, 36 insertions(+), 25 deletions(-)
diff --git a/src/purescala/Analysis.scala b/src/purescala/Analysis.scala
index e7f958345..221de1145 100644
--- a/src/purescala/Analysis.scala
+++ b/src/purescala/Analysis.scala
@@ -10,30 +10,11 @@ class Analysis(val program: Program) {
// we always use the global reporter for this class
val reporter = Settings.reporter
// ...but not always for the extensions
- val extensionsReporter =
- if(Settings.quietExtensions) {
- Settings.quietReporter
- } else {
- Settings.reporter
- }
- // these extensions are always loaded, unless specified otherwise
- val defaultExtensions: Seq[Extension] =
- if(Settings.runDefaultExtensions) {
- (new Z3Solver(extensionsReporter)) :: Nil
- } else {
- Nil
- }
+ Extensions.loadAll
- // we load additional extensions
- val moreExtensions: Seq[Extension] = loadAll(extensionsReporter)
- if(!moreExtensions.isEmpty) {
- reporter.info("The following extensions are loaded:\n" + moreExtensions.toList.map(_.description).mkString(" ", "\n ", ""))
- }
- // ...and split the final list between solvers and analysers
- val extensions: Seq[Extension] = defaultExtensions ++ moreExtensions
- val analysisExtensions: Seq[Analyser] = extensions.filter(_.isInstanceOf[Analyser]).map(_.asInstanceOf[Analyser])
- val solverExtensions: Seq[Solver] = extensions.filter(_.isInstanceOf[Solver]).map(_.asInstanceOf[Solver])
+ val analysisExtensions: Seq[Analyser] = loadedAnalysisExtensions
+ val solverExtensions: Seq[Solver] = loadedSolverExtensions
// Calling this method will run all analyses on the program passed at
// construction time. If at least one solver is loaded, verification
diff --git a/src/purescala/Extensions.scala b/src/purescala/Extensions.scala
index 62b8eb25e..a7744567f 100644
--- a/src/purescala/Extensions.scala
+++ b/src/purescala/Extensions.scala
@@ -18,6 +18,8 @@ object Extensions {
// Returns Some(true) if valid, Some(false) if invalid,
// None if unknown.
def solve(expression: Expr) : Option[Boolean]
+
+ def isSat(expression: Expr) : Option[Boolean] = solve(expression).map(!_)
}
abstract class Analyser(reporter: Reporter) extends Extension(reporter) {
@@ -28,9 +30,20 @@ object Extensions {
// The rest of the code is for dynamically loading extensions
- def loadAll(reporter: Reporter) : Seq[Extension] = {
+ 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 : Seq[Extension] = {
+ val extensionsReporter =
+ if(Settings.quietExtensions) {
+ Settings.quietReporter
+ } else {
+ Settings.reporter
+ }
val allNames: Seq[String] = Settings.extensionNames
- if(!allNames.isEmpty) {
+ val loaded = (if(!allNames.isEmpty) {
val classLoader = Extensions.getClass.getClassLoader
val classes: Seq[Class[_]] = (for(name <- allNames) yield {
@@ -47,7 +60,7 @@ object Extensions {
classes.map(cl => {
try {
val cons = cl.getConstructor(classOf[Reporter])
- cons.newInstance(reporter).asInstanceOf[Extension]
+ cons.newInstance(extensionsReporter).asInstanceOf[Extension]
} catch {
case _ => {
Settings.reporter.error("Extension class " + cl.getName + " does not seem to be of a proper type.")
@@ -57,6 +70,23 @@ object Extensions {
}).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) {
+ (new Z3Solver(extensionsReporter)) :: Nil
+ } else {
+ Nil
}
+ allLoaded = defaultExtensions ++ loaded
+ analysisExtensions = allLoaded.filter(_.isInstanceOf[Analyser]).map(_.asInstanceOf[Analyser])
+ solverExtensions = allLoaded.filter(_.isInstanceOf[Solver]).map(_.asInstanceOf[Solver])
+ loaded
}
+
+ def loadedExtensions : Seq[Extension] = allLoaded
+ def loadedAnalysisExtensions : Seq[Analyser] = analysisExtensions
+ def loadedSolverExtensions : Seq[Solver] = solverExtensions
}
--
GitLab