From 0ad6920486c6f8a3c438536e09092f3023d9a879 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?R=C3=A9gis=20Blanc?= <regwblanc@gmail.com>
Date: Thu, 9 Jun 2011 22:14:55 +0000
Subject: [PATCH] changed interface of Solver to prevent halt before solve
problem. Added a init method to be called before solve
---
src/multisets/Main.scala | 6 ------
src/orderedsets/Main.scala | 5 -----
src/orderedsets/UnifierMain.scala | 5 -----
src/purescala/Analysis.scala | 1 +
src/purescala/Extensions.scala | 13 ++++++++++---
src/purescala/FairZ3Solver.scala | 10 ++++------
src/purescala/ParallelSolver.scala | 27 ++++++++++++++++++++-------
src/purescala/RandomSolver.scala | 16 ++++------------
src/purescala/TimeoutSolver.scala | 7 +++++--
src/purescala/Timer.scala | 1 +
src/purescala/TrivialSolver.scala | 3 ---
src/purescala/Z3Solver.scala | 4 ----
12 files changed, 45 insertions(+), 53 deletions(-)
diff --git a/src/multisets/Main.scala b/src/multisets/Main.scala
index af0c03690..6019d42cf 100644
--- a/src/multisets/Main.scala
+++ b/src/multisets/Main.scala
@@ -12,12 +12,6 @@ class Main(reporter: Reporter) extends Solver(reporter) {
val description = "Multiset Solver"
Global.reporter = reporter
- //TODO
- def halt() {
- error("TODO halt in multiset Solver")
- }
-
-
def createFormulaThatSomethingsIsSet(s:String):FormulaIn = {
val a1 = FIAtom(AIEq(TIMultiplicity(s), TIConstant(1)))
val a0 = FIAtom(AIEq(TIMultiplicity(s), TIConstant(0)))
diff --git a/src/orderedsets/Main.scala b/src/orderedsets/Main.scala
index c9cf22d8b..e338e059a 100644
--- a/src/orderedsets/Main.scala
+++ b/src/orderedsets/Main.scala
@@ -13,11 +13,6 @@ class Main(reporter: Reporter) extends Solver(reporter) {
val description = "BAPA with ordering"
override val shortDescription = "BAPA<"
- //TODO
- def halt() {
- error("TODO halt in multiset Solver")
- }
-
// checks for V-A-L-I-D-I-T-Y !
// Some(true) means formula is valid (negation is unsat)
// Some(false) means formula is not valid (negation is sat)
diff --git a/src/orderedsets/UnifierMain.scala b/src/orderedsets/UnifierMain.scala
index f512759ed..eec35bcd2 100644
--- a/src/orderedsets/UnifierMain.scala
+++ b/src/orderedsets/UnifierMain.scala
@@ -26,11 +26,6 @@ class UnifierMain(reporter: Reporter) extends Solver(reporter) {
var program: Program = null
- //TODO
- def halt() {
- error("TODO halt in multiset Solver")
- }
-
override def setProgram(p: Program) = program = p
// checks for V-A-L-I-D-I-T-Y !
diff --git a/src/purescala/Analysis.scala b/src/purescala/Analysis.scala
index 5fe5ce718..7f2bfad06 100644
--- a/src/purescala/Analysis.scala
+++ b/src/purescala/Analysis.scala
@@ -98,6 +98,7 @@ class Analysis(val program: Program, val reporter: Reporter = Settings.reporter)
superseeded = superseeded ++ Set(se.superseeds: _*)
val t1 = System.nanoTime
+ se.init()
val solverResult = se.solve(vc)
val t2 = System.nanoTime
val dt = ((t2 - t1) / 1000000) / 1000.0
diff --git a/src/purescala/Extensions.scala b/src/purescala/Extensions.scala
index a5618f64b..2653bffab 100644
--- a/src/purescala/Extensions.scala
+++ b/src/purescala/Extensions.scala
@@ -17,14 +17,21 @@ object Extensions {
// Returns Some(true) if valid, Some(false) if invalid,
// None if unknown.
+ // should halt as soon as possible with any result (Unknown is ok) as soon as forceStop is true
def solve(expression: Expr) : Option[Boolean]
def isUnsat(expression: Expr) : Option[Boolean] = solve(negate(expression))
def superseeds : Seq[String] = Nil
- //once this is called, the solver should halt and return a value (probably Unknown) from the
- //solve method as soon as possible
- def halt() : Unit
+ private var _forceStop = false
+ def halt() : Unit = {
+ _forceStop = true
+ }
+ def init() : Unit = {
+ _forceStop = false
+ }
+ protected def forceStop = _forceStop
+
}
abstract class Analyser(reporter: Reporter) extends Extension(reporter) {
diff --git a/src/purescala/FairZ3Solver.scala b/src/purescala/FairZ3Solver.scala
index 28ed00ec0..ca20e8d9a 100644
--- a/src/purescala/FairZ3Solver.scala
+++ b/src/purescala/FairZ3Solver.scala
@@ -414,11 +414,10 @@ class FairZ3Solver(reporter: Reporter) extends Solver(reporter) with AbstractZ3S
decideWithModel(vc, forValidity)._1
}
- private var forceStop : Boolean = false
private var foundDefinitiveAnswer : Boolean = false
- def halt() {
+ override def halt() {
if(!foundDefinitiveAnswer) {
- forceStop = true
+ super.halt
if(z3 != null)
z3.softCheckCancel
}
@@ -438,16 +437,15 @@ class FairZ3Solver(reporter: Reporter) extends Solver(reporter) with AbstractZ3S
initializationStopwatch.start
- forceStop = false
-
foundDefinitiveAnswer = false
+ /*
def stopCallback() : Unit = {
if(!foundDefinitiveAnswer) {
reporter.error(" - Timeout reached.")
forceStop = true
z3.softCheckCancel
}
- }
+ }*/
//val timer : Option[Timer] = Settings.solverTimeout.map(t => new Timer(stopCallback, t))
//timer.foreach(_.start())
diff --git a/src/purescala/ParallelSolver.scala b/src/purescala/ParallelSolver.scala
index 8870d10c4..63b04c76c 100644
--- a/src/purescala/ParallelSolver.scala
+++ b/src/purescala/ParallelSolver.scala
@@ -1,8 +1,5 @@
package purescala
-//TODO: what if we call halt before solve is started in every solvers
-//TODO: stopping the FairZ3Solver seems to cause an error because model is not correct
-
import Common._
import Definitions._
import Extensions._
@@ -26,9 +23,11 @@ class ParallelSolver(solvers: Solver*) extends Solver(solvers(0).reporter) {
override val superseeds : Seq[String] = solvers.map(_.shortDescription).toSeq
case class Solve(expr: Expr)
+ case object Init
+ case object Ready
case class Result(res: Option[Boolean])
- class SolverRunner(s: Solver) extends DaemonActor {
+ private class SolverRunner(s: Solver) extends DaemonActor {
/*
val that = this
@@ -51,6 +50,11 @@ class ParallelSolver(solvers: Solver*) extends Solver(solvers(0).reporter) {
def act(): Unit = {
while(true) {
receive {
+ case Init => {
+ reporter.info("Init solver " + s.shortDescription)
+ s.init
+ coordinator ! Ready
+ }
case Solve(expr) => {
reporter.info("Starting solver " + s.shortDescription)
val res = s.solve(expr)
@@ -62,15 +66,24 @@ class ParallelSolver(solvers: Solver*) extends Solver(solvers(0).reporter) {
}
}
- class Coordinator extends DaemonActor {
+ private class Coordinator extends DaemonActor {
def act(): Unit = {
while(true) {
receive {
case s@Solve(expr) => {
+ var nbResponses = 0
+
+ solverRunners.foreach(_ ! Init)
+ while(nbResponses < nbSolvers) {
+ receive {
+ case Ready => nbResponses += 1
+ }
+ }
+
+ nbResponses = 0
solverRunners.foreach(_ ! s)
var result: Option[Boolean] = None
- var nbResponses = 0
while(nbResponses < nbSolvers) {
receive {
@@ -101,7 +114,7 @@ class ParallelSolver(solvers: Solver*) extends Solver(solvers(0).reporter) {
result
}
- def halt() {
+ override def halt() {
solvers.foreach(_.halt)
}
diff --git a/src/purescala/RandomSolver.scala b/src/purescala/RandomSolver.scala
index 6bf72bed3..18623a5f7 100644
--- a/src/purescala/RandomSolver.scala
+++ b/src/purescala/RandomSolver.scala
@@ -64,19 +64,11 @@ class RandomSolver(reporter: Reporter, val nbTrial: Option[Int] = None) extends
case f : FunctionType => error("I don't know what to do")
}
- private var externalRunning = true
-
- def halt() {
- externalRunning = false
- }
-
def solve(expression: Expr) : Option[Boolean] = {
val vars = variablesOf(expression)
val nbVars = vars.size
- var running = true
- externalRunning = true
-
+ var stop = false
//bound starts at 1 since it allows to test value like 0, 1, and Leaf of class hierarchy
var bound = 1
val maxBound = Int.MaxValue
@@ -86,10 +78,10 @@ class RandomSolver(reporter: Reporter, val nbTrial: Option[Int] = None) extends
var result: Option[Boolean] = None
var iteration = 0
- while(running && externalRunning) {
+ while(!forceStop && !stop) {
nbTrial match {
- case Some(n) => running &&= (iteration < n)
+ case Some(n) => stop &&= (iteration < n)
case None => ()
}
@@ -112,7 +104,7 @@ class RandomSolver(reporter: Reporter, val nbTrial: Option[Int] = None) extends
case OK(BooleanLiteral(false)) => {
reporter.info("Found counter example to formula: " + var2val)
result = Some(false)
- running = false
+ stop = true
}
/* in any of the following case, simply continue with another assignement */
case InfiniteComputation() => {
diff --git a/src/purescala/TimeoutSolver.scala b/src/purescala/TimeoutSolver.scala
index aa1e28424..dcd2a95ad 100644
--- a/src/purescala/TimeoutSolver.scala
+++ b/src/purescala/TimeoutSolver.scala
@@ -11,7 +11,7 @@ import scala.sys.error
class TimeoutSolver(solver : Solver, timeout : Int) extends Solver(solver.reporter) {
val description = solver.description + ", with timeout"
- override val shortDescription = solver.shortDescription
+ override val shortDescription = solver.shortDescription + "+t"
override def setProgram(prog: Program): Unit = {
solver.setProgram(prog)
@@ -25,7 +25,10 @@ class TimeoutSolver(solver : Solver, timeout : Int) extends Solver(solver.report
res
}
- def halt() {
+ override def init() {
+ solver.init
+ }
+ override def halt() {
solver.halt
}
diff --git a/src/purescala/Timer.scala b/src/purescala/Timer.scala
index 0579c93fa..b72b12b3e 100644
--- a/src/purescala/Timer.scala
+++ b/src/purescala/Timer.scala
@@ -14,6 +14,7 @@ class Timer(callback : () => Unit, maxSecs : Int) extends Thread {
if(asMillis < (System.currentTimeMillis - startTime)) {
exceeded = true
}
+ Thread.sleep(100) //is needed on my (regis) machine, if not here, the loop does not stop when halt is called.
}
if(exceeded && keepRunning) {
callback()
diff --git a/src/purescala/TrivialSolver.scala b/src/purescala/TrivialSolver.scala
index cef3ca8b6..78cf3d0ef 100644
--- a/src/purescala/TrivialSolver.scala
+++ b/src/purescala/TrivialSolver.scala
@@ -19,7 +19,4 @@ class TrivialSolver(reporter: Reporter) extends Solver(reporter) {
case _ => None
}
- def halt() {
- //nothing to do
- }
}
diff --git a/src/purescala/Z3Solver.scala b/src/purescala/Z3Solver.scala
index 75350ff97..98cb563b4 100644
--- a/src/purescala/Z3Solver.scala
+++ b/src/purescala/Z3Solver.scala
@@ -49,10 +49,6 @@ class Z3Solver(reporter: Reporter) extends Solver(reporter) with AbstractZ3Solve
program = prog
}
- def halt() {
- scala.sys.error("Halt not supported")
- }
-
private def restartZ3: Unit = {
if (neverInitialized) {
neverInitialized = false
--
GitLab