diff --git a/src/main/scala/leon/synthesis/ParallelSearch.scala b/src/main/scala/leon/synthesis/ParallelSearch.scala index b526d9bedc398ea21c1e9ca3a7235462f6b3c3e0..befda36d9c3b16b89e6dd5763da42dfdd5453dd5 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 75913701ce175c2d2da747b04ad09047b2127f13..1f32265357b5c03a1e1e5e44fd815cdda16196b2 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 c7d3ec896d58dd907cfb8013ee46e6fe8c1cbb6a..6e677c687e52fe12ae6f2a9e8e3bde77263b83e9 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)