From 45985e1bdcdd50b7f0f9a625fbec483ae65c6cb7 Mon Sep 17 00:00:00 2001
From: Etienne Kneuss <ekneuss@gmail.com>
Date: Thu, 6 Dec 2012 18:30:52 +0100
Subject: [PATCH] More reliable shutdown
---
src/main/scala/leon/synthesis/ParallelSearch.scala | 5 +++++
src/main/scala/leon/synthesis/SimpleSearch.scala | 2 +-
.../search/AndOrGraphParallelSearch.scala | 8 +++++---
.../leon/synthesis/search/AndOrGraphSearch.scala | 14 +++++++++++---
4 files changed, 22 insertions(+), 7 deletions(-)
diff --git a/src/main/scala/leon/synthesis/ParallelSearch.scala b/src/main/scala/leon/synthesis/ParallelSearch.scala
index befe0ee2a..a6d436509 100644
--- a/src/main/scala/leon/synthesis/ParallelSearch.scala
+++ b/src/main/scala/leon/synthesis/ParallelSearch.scala
@@ -23,6 +23,11 @@ class ParallelSearch(synth: Synthesizer,
SynthesisContext(solver = solver, reporter = synth.reporter, shouldStop = synth.shouldStop)
}
+ override def stop() = {
+ synth.shouldStop.set(true)
+ super.stop()
+ }
+
def expandAndTask(ref: ActorRef, sctx: SynthesisContext)(t: TaskRunRule) = {
val prefix = "[%-20s] ".format(Option(t.rule).getOrElse("?"))
diff --git a/src/main/scala/leon/synthesis/SimpleSearch.scala b/src/main/scala/leon/synthesis/SimpleSearch.scala
index bc254e2fa..88a51b805 100644
--- a/src/main/scala/leon/synthesis/SimpleSearch.scala
+++ b/src/main/scala/leon/synthesis/SimpleSearch.scala
@@ -69,7 +69,7 @@ class SimpleSearch(synth: Synthesizer,
}
def search(): Option[Solution] = {
- while (!g.tree.isSolved && !isStopped) {
+ while (!g.tree.isSolved) {
nextLeaf() match {
case Some(l) =>
l match {
diff --git a/src/main/scala/leon/synthesis/search/AndOrGraphParallelSearch.scala b/src/main/scala/leon/synthesis/search/AndOrGraphParallelSearch.scala
index d0f32ccee..0f126660e 100644
--- a/src/main/scala/leon/synthesis/search/AndOrGraphParallelSearch.scala
+++ b/src/main/scala/leon/synthesis/search/AndOrGraphParallelSearch.scala
@@ -14,7 +14,7 @@ abstract class AndOrGraphParallelSearch[WC,
def initWorkerContext(w: ActorRef): WC
- val nWorkers = 5
+ val nWorkers = 7
val timeout = 600.seconds
var system: ActorSystem = _
@@ -128,8 +128,10 @@ abstract class AndOrGraphParallelSearch[WC,
sendWork()
case Terminated(w) =>
- processing -= workers(w).get
- workers -= w
+ if (workers contains w) {
+ processing -= workers(w).get
+ workers -= w
+ }
}
}
diff --git a/src/main/scala/leon/synthesis/search/AndOrGraphSearch.scala b/src/main/scala/leon/synthesis/search/AndOrGraphSearch.scala
index 1291babe9..bf3fed4e9 100644
--- a/src/main/scala/leon/synthesis/search/AndOrGraphSearch.scala
+++ b/src/main/scala/leon/synthesis/search/AndOrGraphSearch.scala
@@ -60,10 +60,8 @@ abstract class AndOrGraphSearch[AT <: AOAndTask[S],
case class ExpandSuccess[T <: AOTask[S]](sol: S) extends ExpandResult[T]
case class ExpandFailure[T <: AOTask[S]]() extends ExpandResult[T]
- var isStopped = false
-
def stop() {
- isStopped = true
+
}
def search(): Option[S]
@@ -79,6 +77,11 @@ abstract class AndOrGraphSearch[AT <: AOAndTask[S],
al.isUnsolvable = true
al.parent.unsolvable(al)
}
+
+ if (g.tree.isSolved) {
+ stop()
+ }
+
processing -= al
}
@@ -93,6 +96,11 @@ abstract class AndOrGraphSearch[AT <: AOAndTask[S],
ol.isUnsolvable = true
ol.parent.unsolvable(ol)
}
+
+ if (g.tree.isSolved) {
+ stop()
+ }
+
processing -= ol
}
}
--
GitLab