From 510168a811ef0b3c7e9230e5cc4d775fa71f314d Mon Sep 17 00:00:00 2001
From: Philippe Suter <philippe.suter@gmail.com>
Date: Tue, 11 Dec 2012 15:29:28 +0100
Subject: [PATCH] Solvers are LeonComponents.
---
.../scala/leon/solvers/ParallelSolver.scala | 18 +++++++++---------
src/main/scala/leon/solvers/RandomSolver.scala | 2 +-
src/main/scala/leon/solvers/Solver.scala | 6 +-----
.../scala/leon/solvers/TrivialSolver.scala | 2 +-
.../scala/leon/solvers/z3/FairZ3Solver.scala | 15 +++++++--------
.../solvers/z3/UninterpretedZ3Solver.scala | 2 +-
.../leon/verification/AnalysisPhase.scala | 4 ++--
.../verification/VerificationCondition.scala | 2 +-
8 files changed, 23 insertions(+), 28 deletions(-)
diff --git a/src/main/scala/leon/solvers/ParallelSolver.scala b/src/main/scala/leon/solvers/ParallelSolver.scala
index 3ecf8df6f..b6e66ff07 100644
--- a/src/main/scala/leon/solvers/ParallelSolver.scala
+++ b/src/main/scala/leon/solvers/ParallelSolver.scala
@@ -22,8 +22,8 @@ class ParallelSolver(solvers : Solver*) extends Solver(solvers(0).context) with
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
+ override val name = solvers.map(_.name).mkString("//")
+ override val superseeds : Seq[String] = solvers.map(_.name).toSeq
case class Solve(expr: Expr)
case object Init
@@ -39,10 +39,10 @@ class ParallelSolver(solvers : Solver*) extends Solver(solvers(0).context) with
while(true) {
receive {
case Solve(expr) => {
- reporter.info("Starting solver " + s.shortDescription)
+ reporter.info("Starting solver " + s.name)
val res = s.solve(expr)
that ! Result(res)
- reporter.info("Ending solver " + s.shortDescription)
+ reporter.info("Ending solver " + s.name)
}
}
}
@@ -54,15 +54,15 @@ class ParallelSolver(solvers : Solver*) extends Solver(solvers(0).context) with
while(true) {
receive {
case Init => {
- reporter.info("Init solver " + s.shortDescription)
+ reporter.info("Init solver " + s.name)
s.init
coordinator ! Ready
}
case Solve(expr) => {
- reporter.info("Starting solver " + s.shortDescription)
+ reporter.info("Starting solver " + s.name)
val res = s.solve(expr)
coordinator ! Result(res)
- reporter.info("Ending solver " + s.shortDescription)
+ reporter.info("Ending solver " + s.name)
}
}
}
@@ -140,7 +140,7 @@ class ParallelSolver(solvers : Solver*) extends Solver(solvers(0).context) with
class SolverRunner(s: Solver, expr: Expr) extends Actor {
def act() {
- reporter.info("Starting solver " + s.shortDescription)
+ reporter.info("Starting solver " + s.name)
s.solve(expr) match {
case Some(b) => {
lock.acquire
@@ -162,7 +162,7 @@ class ParallelSolver(solvers : Solver*) extends Solver(solvers(0).context) with
if(nbResponses >= nbSolvers)
resultNotReady = false
lock.release
- reporter.info("Ending solver " + s.shortDescription)
+ reporter.info("Ending solver " + s.name)
}
}
*/
diff --git a/src/main/scala/leon/solvers/RandomSolver.scala b/src/main/scala/leon/solvers/RandomSolver.scala
index fead03a79..f7c8ee3e9 100644
--- a/src/main/scala/leon/solvers/RandomSolver.scala
+++ b/src/main/scala/leon/solvers/RandomSolver.scala
@@ -17,8 +17,8 @@ class RandomSolver(context: LeonContext, val nbTrial: Option[Int] = None) extend
private val reporter = context.reporter
+ val name = "QC"
val description = "Solver applying random testing (QuickCheck-like)"
- override val shortDescription = "QC"
private val random = new Random()
diff --git a/src/main/scala/leon/solvers/Solver.scala b/src/main/scala/leon/solvers/Solver.scala
index 0cd3dcac0..777e4dc1c 100644
--- a/src/main/scala/leon/solvers/Solver.scala
+++ b/src/main/scala/leon/solvers/Solver.scala
@@ -6,11 +6,7 @@ import purescala.Definitions._
import purescala.TreeOps._
import purescala.Trees._
-abstract class Solver(val context : LeonContext) extends IncrementalSolverBuilder {
- // This used to be in Extension
- val description : String
- val shortDescription : String
-
+abstract class Solver(val context : LeonContext) extends IncrementalSolverBuilder with LeonComponent {
// 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/TrivialSolver.scala b/src/main/scala/leon/solvers/TrivialSolver.scala
index bd8edcf50..3451aa759 100644
--- a/src/main/scala/leon/solvers/TrivialSolver.scala
+++ b/src/main/scala/leon/solvers/TrivialSolver.scala
@@ -7,8 +7,8 @@ import purescala.Trees._
import purescala.TypeTrees._
class TrivialSolver(context: LeonContext) extends Solver(context) with NaiveIncrementalSolver {
+ val name = "trivial"
val description = "Solver for syntactically trivial formulas"
- override val shortDescription = "trivial"
def solve(expression: Expr) : Option[Boolean] = expression match {
case BooleanLiteral(v) => Some(v)
diff --git a/src/main/scala/leon/solvers/z3/FairZ3Solver.scala b/src/main/scala/leon/solvers/z3/FairZ3Solver.scala
index e572bab23..5990c7165 100644
--- a/src/main/scala/leon/solvers/z3/FairZ3Solver.scala
+++ b/src/main/scala/leon/solvers/z3/FairZ3Solver.scala
@@ -15,23 +15,22 @@ import purescala.TypeTrees._
import scala.collection.mutable.{Map => MutableMap}
import scala.collection.mutable.{Set => MutableSet}
-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)
-
- private val UNKNOWNASSAT : Boolean = !Settings.noForallAxioms
+class FairZ3Solver(context : LeonContext)
+ extends Solver(context)
+ with AbstractZ3Solver
+ with Z3ModelReconstruction
+ with LeonComponent {
+ val name = "Z3-f"
val description = "Fair Z3 Solver"
- override val shortDescription = "Z3-f"
// this is fixed
protected[leon] val z3cfg = new Z3Config(
"MODEL" -> true,
"MBQI" -> false,
- // "SOFT_TIMEOUT" -> 100,
"TYPE_CHECK" -> true,
"WELL_SORTED_CHECK" -> true
- )
+ )
toggleWarningMessages(true)
def isKnownDef(funDef: FunDef) : Boolean = functionMap.isDefinedAt(funDef)
diff --git a/src/main/scala/leon/solvers/z3/UninterpretedZ3Solver.scala b/src/main/scala/leon/solvers/z3/UninterpretedZ3Solver.scala
index 87ef4ecd2..d0024b737 100644
--- a/src/main/scala/leon/solvers/z3/UninterpretedZ3Solver.scala
+++ b/src/main/scala/leon/solvers/z3/UninterpretedZ3Solver.scala
@@ -20,8 +20,8 @@ import purescala.TypeTrees._
* Results should come back very quickly.
*/
class UninterpretedZ3Solver(context : LeonContext) extends Solver(context) with AbstractZ3Solver with Z3ModelReconstruction {
+ val name = "Z3-u"
val description = "Uninterpreted Z3 Solver"
- override val shortDescription = "Z3-u"
// this is fixed
protected[leon] val z3cfg = new Z3Config(
diff --git a/src/main/scala/leon/verification/AnalysisPhase.scala b/src/main/scala/leon/verification/AnalysisPhase.scala
index e8bb9791c..d4a2b71b7 100644
--- a/src/main/scala/leon/verification/AnalysisPhase.scala
+++ b/src/main/scala/leon/verification/AnalysisPhase.scala
@@ -89,8 +89,8 @@ object AnalysisPhase extends LeonPhase[Program,VerificationReport] {
// try all solvers until one returns a meaningful answer
var superseeded : Set[String] = Set.empty[String]
solvers.find(se => {
- reporter.info("Trying with solver: " + se.shortDescription)
- if(superseeded(se.shortDescription) || superseeded(se.description)) {
+ reporter.info("Trying with solver: " + se.name)
+ if(superseeded(se.name) || superseeded(se.description)) {
reporter.info("Solver was superseeded. Skipping.")
false
} else {
diff --git a/src/main/scala/leon/verification/VerificationCondition.scala b/src/main/scala/leon/verification/VerificationCondition.scala
index 217eb94b7..573bcd699 100644
--- a/src/main/scala/leon/verification/VerificationCondition.scala
+++ b/src/main/scala/leon/verification/VerificationCondition.scala
@@ -27,7 +27,7 @@ class VerificationCondition(val condition: Expr, val funDef: FunDef, val kind: V
}
def solverStr = solvedWith match {
- case Some(s) => s.shortDescription
+ case Some(s) => s.name
case None => ""
}
--
GitLab