From c5e13beb937b1c8d6b523a91e4b11722921d74ce Mon Sep 17 00:00:00 2001
From: Etienne Kneuss <ekneuss@gmail.com>
Date: Thu, 6 Dec 2012 18:08:06 +0100
Subject: [PATCH] Provide reliable way to shutdown long-lasting rules
---
src/main/scala/leon/solvers/z3/FairZ3Solver.scala | 4 ++--
src/main/scala/leon/synthesis/ParallelSearch.scala | 2 +-
src/main/scala/leon/synthesis/SynthesisContext.scala | 7 +++++--
src/main/scala/leon/synthesis/Synthesizer.scala | 6 ++++--
src/main/scala/leon/synthesis/rules/Cegis.scala | 4 ++--
.../leon/synthesis/search/AndOrGraphParallelSearch.scala | 9 ++++++---
6 files changed, 20 insertions(+), 12 deletions(-)
diff --git a/src/main/scala/leon/solvers/z3/FairZ3Solver.scala b/src/main/scala/leon/solvers/z3/FairZ3Solver.scala
index f91fa5d2e..3646cc2d8 100644
--- a/src/main/scala/leon/solvers/z3/FairZ3Solver.scala
+++ b/src/main/scala/leon/solvers/z3/FairZ3Solver.scala
@@ -432,7 +432,7 @@ class FairZ3Solver(context : LeonContext) extends Solver(context) with AbstractZ
reporter.info("UNSAT BECAUSE: "+core.mkString(" AND "))
if (!forceStop) {
- if (Settings.luckyTest) {
+ if (Settings.luckyTest && false) {
// we need the model to perform the additional test
reporter.info(" - Running search without blocked literals (w/ lucky test)")
} else {
@@ -447,7 +447,7 @@ class FairZ3Solver(context : LeonContext) extends Solver(context) with AbstractZ
foundAnswer(Some(false), core = z3CoreToCore(solver.getUnsatCore))
case Some(true) =>
//reporter.info("SAT WITHOUT Blockers")
- if (Settings.luckyTest && !forceStop) {
+ if (Settings.luckyTest && !forceStop && false) {
// we might have been lucky :D
val (wereWeLucky, cleanModel) = validateAndDeleteModel(solver.getModel, entireFormula, varsInVC)
if(wereWeLucky) {
diff --git a/src/main/scala/leon/synthesis/ParallelSearch.scala b/src/main/scala/leon/synthesis/ParallelSearch.scala
index 0c48bd42a..befe0ee2a 100644
--- a/src/main/scala/leon/synthesis/ParallelSearch.scala
+++ b/src/main/scala/leon/synthesis/ParallelSearch.scala
@@ -20,7 +20,7 @@ class ParallelSearch(synth: Synthesizer,
solver.initZ3
- SynthesisContext(solver = solver, reporter = synth.reporter)
+ SynthesisContext(solver = solver, reporter = synth.reporter, shouldStop = synth.shouldStop)
}
def expandAndTask(ref: ActorRef, sctx: SynthesisContext)(t: TaskRunRule) = {
diff --git a/src/main/scala/leon/synthesis/SynthesisContext.scala b/src/main/scala/leon/synthesis/SynthesisContext.scala
index 831bd5450..d23f4df29 100644
--- a/src/main/scala/leon/synthesis/SynthesisContext.scala
+++ b/src/main/scala/leon/synthesis/SynthesisContext.scala
@@ -3,12 +3,15 @@ package synthesis
import solvers.Solver
+import java.util.concurrent.atomic.AtomicBoolean
+
case class SynthesisContext(
solver: Solver,
- reporter: Reporter
+ reporter: Reporter,
+ shouldStop: AtomicBoolean
)
object SynthesisContext {
- def fromSynthesizer(synth: Synthesizer) = SynthesisContext(synth.solver, synth.reporter)
+ def fromSynthesizer(synth: Synthesizer) = SynthesisContext(synth.solver, synth.reporter, new AtomicBoolean(false))
}
diff --git a/src/main/scala/leon/synthesis/Synthesizer.scala b/src/main/scala/leon/synthesis/Synthesizer.scala
index ccf4be6d1..aa054774a 100644
--- a/src/main/scala/leon/synthesis/Synthesizer.scala
+++ b/src/main/scala/leon/synthesis/Synthesizer.scala
@@ -15,6 +15,8 @@ import collection.mutable.PriorityQueue
import synthesis.search._
+import java.util.concurrent.atomic.AtomicBoolean
+
class Synthesizer(val context : LeonContext,
val solver: Solver,
val program: Program,
@@ -26,7 +28,7 @@ class Synthesizer(val context : LeonContext,
import reporter.{error,warning,info,fatalError}
- var continue = true
+ var shouldStop = new AtomicBoolean(false)
def synthesize(): (Solution, Boolean) = {
@@ -43,7 +45,7 @@ class Synthesizer(val context : LeonContext,
println
reporter.info("Aborting...")
- continue = false
+ shouldStop.set(true)
search.stop()
Signal.handle(sigINT, oldHandler)
diff --git a/src/main/scala/leon/synthesis/rules/Cegis.scala b/src/main/scala/leon/synthesis/rules/Cegis.scala
index c1029c5db..6dd2b83b6 100644
--- a/src/main/scala/leon/synthesis/rules/Cegis.scala
+++ b/src/main/scala/leon/synthesis/rules/Cegis.scala
@@ -163,7 +163,7 @@ case object CEGIS extends Rule("CEGIS", 150) {
//println("Unrolling #"+unrolings+" bss size: "+bss.size)
- while (result.isEmpty && continue) {
+ while (result.isEmpty && continue && !sctx.shouldStop.get) {
//println("Looking for CE...")
//println("-"*80)
//println(basePhi)
@@ -262,7 +262,7 @@ case object CEGIS extends Rule("CEGIS", 150) {
}
unrolings += 1
- } while(unrolings < maxUnrolings && result.isEmpty)
+ } while(unrolings < maxUnrolings && result.isEmpty && !sctx.shouldStop.get)
result.getOrElse(RuleApplicationImpossible)
diff --git a/src/main/scala/leon/synthesis/search/AndOrGraphParallelSearch.scala b/src/main/scala/leon/synthesis/search/AndOrGraphParallelSearch.scala
index a9a3201ae..d0f32ccee 100644
--- a/src/main/scala/leon/synthesis/search/AndOrGraphParallelSearch.scala
+++ b/src/main/scala/leon/synthesis/search/AndOrGraphParallelSearch.scala
@@ -4,6 +4,7 @@ import akka.actor._
import akka.util.duration._
import akka.util.Timeout
import akka.pattern.ask
+import akka.pattern.AskTimeoutException
import akka.dispatch.Await
abstract class AndOrGraphParallelSearch[WC,
@@ -27,7 +28,11 @@ abstract class AndOrGraphParallelSearch[WC,
system.actorOf(Props(new Worker(master)), name = "Worker"+i)
}
- Await.result(master.ask(Protocol.BeginSearch)(timeout), timeout)
+ try {
+ Await.result(master.ask(Protocol.BeginSearch)(timeout), timeout)
+ } catch {
+ case e: AskTimeoutException =>
+ }
if (system ne null) {
system.shutdown
@@ -92,8 +97,6 @@ abstract class AndOrGraphParallelSearch[WC,
w ! RequestOrTask(ol.task)
}
}
-
-
}
}
--
GitLab