diff --git a/src/main/scala/leon/synthesis/ParallelSearch.scala b/src/main/scala/leon/synthesis/ParallelSearch.scala index cbf374f7e89b8ce8f5c7b98d244ec8a48d4fd420..cd8f11d336d12f854276d28b487ac6622218b46c 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 6e677c687e52fe12ae6f2a9e8e3bde77263b83e9..be7ee349832f2c4d67f8b8ea07511474cc52a051 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 + } }