From 6475e73df982d8e170a91e1022cebd35ac40e6dc Mon Sep 17 00:00:00 2001
From: Etienne Kneuss <ekneuss@gmail.com>
Date: Fri, 23 Nov 2012 19:57:20 +0100
Subject: [PATCH] Graceful init and termination of the search in parallel
---
src/main/scala/leon/synthesis/ParallelSearch.scala | 3 ++-
src/main/scala/leon/synthesis/search/AndOrGraph.scala | 2 ++
.../leon/synthesis/search/AndOrGraphParallelSearch.scala | 6 ++++++
3 files changed, 10 insertions(+), 1 deletion(-)
diff --git a/src/main/scala/leon/synthesis/ParallelSearch.scala b/src/main/scala/leon/synthesis/ParallelSearch.scala
index b526d9bed..befda36d9 100644
--- a/src/main/scala/leon/synthesis/ParallelSearch.scala
+++ b/src/main/scala/leon/synthesis/ParallelSearch.scala
@@ -4,6 +4,7 @@ package synthesis
import synthesis.search._
import akka.actor._
import solvers.z3.FairZ3Solver
+import solvers.TrivialSolver
class ParallelSearch(synth: Synthesizer,
problem: Problem,
@@ -13,7 +14,7 @@ class ParallelSearch(synth: Synthesizer,
def initWorkerContext(wr: ActorRef) = {
val reporter = new SilentReporter
- val solver = new FairZ3Solver(synth.reporter)
+ val solver = new TrivialSolver(synth.reporter)
solver.setProgram(synth.program)
SynthesisContext(solver = solver, reporter = synth.reporter)
diff --git a/src/main/scala/leon/synthesis/search/AndOrGraph.scala b/src/main/scala/leon/synthesis/search/AndOrGraph.scala
index 75913701c..1f3226535 100644
--- a/src/main/scala/leon/synthesis/search/AndOrGraph.scala
+++ b/src/main/scala/leon/synthesis/search/AndOrGraph.scala
@@ -177,6 +177,8 @@ class AndOrGraph[AT <: AOAndTask[S], OT <: AOOrTask[S], S <: AOSolution](val roo
minAlternative = sub
notifyParent(solution.get)
+
+ case _ =>
}
}
diff --git a/src/main/scala/leon/synthesis/search/AndOrGraphParallelSearch.scala b/src/main/scala/leon/synthesis/search/AndOrGraphParallelSearch.scala
index c7d3ec896..6e677c687 100644
--- a/src/main/scala/leon/synthesis/search/AndOrGraphParallelSearch.scala
+++ b/src/main/scala/leon/synthesis/search/AndOrGraphParallelSearch.scala
@@ -26,6 +26,8 @@ abstract class AndOrGraphParallelSearch[WC,
val timeout = 600.seconds
Await.result(master.ask(Protocol.BeginSearch)(timeout), timeout)
+ system.shutdown
+
g.tree.solution
}
@@ -70,6 +72,7 @@ abstract class AndOrGraphParallelSearch[WC,
case ls =>
for ((w, leaf) <- idleWorkers.keySet zip ls) {
+ processing += leaf
leaf match {
case al: g.AndLeaf =>
workers += w -> Some(al)
@@ -85,6 +88,9 @@ abstract class AndOrGraphParallelSearch[WC,
}
def receive = {
+ case BeginSearch =>
+ outer = sender
+
case WorkerNew(w) =>
workers += w -> None
context.watch(w)
--
GitLab