From c4dbcb7e4658760109babd42c14dd8b36e4c2373 Mon Sep 17 00:00:00 2001
From: Etienne Kneuss <ekneuss@gmail.com>
Date: Fri, 23 Nov 2012 20:08:26 +0100
Subject: [PATCH] Better organization and handling for Ctrl^C
---
.../scala/leon/synthesis/ParallelSearch.scala | 2 +-
.../search/AndOrGraphParallelSearch.scala | 20 ++++++++++++++-----
2 files changed, 16 insertions(+), 6 deletions(-)
diff --git a/src/main/scala/leon/synthesis/ParallelSearch.scala b/src/main/scala/leon/synthesis/ParallelSearch.scala
index cbf374f7e..cd8f11d33 100644
--- a/src/main/scala/leon/synthesis/ParallelSearch.scala
+++ b/src/main/scala/leon/synthesis/ParallelSearch.scala
@@ -14,7 +14,7 @@ class ParallelSearch(synth: Synthesizer,
def initWorkerContext(wr: ActorRef) = {
val reporter = new SilentReporter
- val solver = new FairZ3Solver(synth.reporter)
+ val solver = new FairZ3Solver(reporter)
solver.setProgram(synth.program)
SynthesisContext(solver = solver, reporter = synth.reporter)
diff --git a/src/main/scala/leon/synthesis/search/AndOrGraphParallelSearch.scala b/src/main/scala/leon/synthesis/search/AndOrGraphParallelSearch.scala
index 6e677c687..be7ee3498 100644
--- a/src/main/scala/leon/synthesis/search/AndOrGraphParallelSearch.scala
+++ b/src/main/scala/leon/synthesis/search/AndOrGraphParallelSearch.scala
@@ -13,20 +13,26 @@ abstract class AndOrGraphParallelSearch[WC,
def initWorkerContext(w: ActorRef): WC
- val system = ActorSystem("ParallelSearch")
+ val nWorkers = 5
+ val timeout = 600.seconds
- val master = system.actorOf(Props(new Master), name = "Master")
+ var system: ActorSystem = _
def search(): Option[S] = {
+ system = ActorSystem("ParallelSearch")
- val workers = for (i <- 0 to 5) yield {
+ val master = system.actorOf(Props(new Master), name = "Master")
+
+ val workers = for (i <- 1 to nWorkers) yield {
system.actorOf(Props(new Worker(master)), name = "Worker"+i)
}
- val timeout = 600.seconds
Await.result(master.ask(Protocol.BeginSearch)(timeout), timeout)
- system.shutdown
+ if (system ne null) {
+ system.shutdown
+ system = null
+ }
g.tree.solution
}
@@ -34,6 +40,10 @@ abstract class AndOrGraphParallelSearch[WC,
override def stop() {
super.stop()
+ if(system ne null) {
+ system.shutdown
+ system = null
+ }
}
--
GitLab