From ebd264dc15d7b1167c6af59e5ad710f7cd92bfc0 Mon Sep 17 00:00:00 2001
From: Etienne Kneuss <ekneuss@gmail.com>
Date: Thu, 6 Dec 2012 01:41:10 +0100
Subject: [PATCH] Fix parallel search with FairZ3Solver
---
.../scala/leon/synthesis/Heuristics.scala | 22 +++++++++++--------
.../scala/leon/synthesis/ParallelSearch.scala | 16 +++++++++-----
2 files changed, 23 insertions(+), 15 deletions(-)
diff --git a/src/main/scala/leon/synthesis/Heuristics.scala b/src/main/scala/leon/synthesis/Heuristics.scala
index b03e01667..f8dc04423 100644
--- a/src/main/scala/leon/synthesis/Heuristics.scala
+++ b/src/main/scala/leon/synthesis/Heuristics.scala
@@ -23,15 +23,19 @@ trait Heuristic {
object HeuristicStep {
def verifyPre(sctx: SynthesisContext, problem: Problem)(s: Solution): Solution = {
- sctx.solver.solveSAT(And(Not(s.pre), problem.phi)) match {
- case (Some(true), model) =>
- sctx.reporter.warning("Heuristic failed to produce weakest precondition:")
- sctx.reporter.warning(" - problem: "+problem)
- sctx.reporter.warning(" - precondition: "+s.pre)
- s
- case _ =>
- s
- }
+ //sctx here is unsafe to use in parallel. onSuccess should take a sctx for
+ //this to be possible
+
+ //sctx.solver.solveSAT(And(Not(s.pre), problem.phi)) match {
+ // case (Some(true), model) =>
+ // sctx.reporter.warning("Heuristic failed to produce weakest precondition:")
+ // sctx.reporter.warning(" - problem: "+problem)
+ // sctx.reporter.warning(" - precondition: "+s.pre)
+ // s
+ // case _ =>
+ // s
+ //}
+ s
}
def apply(sctx: SynthesisContext, problem: Problem, subProblems: List[Problem], onSuccess: List[Solution] => Solution) = {
diff --git a/src/main/scala/leon/synthesis/ParallelSearch.scala b/src/main/scala/leon/synthesis/ParallelSearch.scala
index 7fa8a62de..31ddf1fbb 100644
--- a/src/main/scala/leon/synthesis/ParallelSearch.scala
+++ b/src/main/scala/leon/synthesis/ParallelSearch.scala
@@ -28,15 +28,19 @@ class ParallelSearch(synth: Synthesizer,
t.app.apply(sctx) match {
case RuleSuccess(sol) =>
- info(prefix+"Got: "+t.problem)
- info(prefix+"Solved with: "+sol)
+ synth.synchronized {
+ info(prefix+"Got: "+t.problem)
+ info(prefix+"Solved with: "+sol)
+ }
ExpandSuccess(sol)
case RuleDecomposed(sub, onSuccess) =>
- info(prefix+"Got: "+t.problem)
- info(prefix+"Decomposed into:")
- for(p <- sub) {
- info(prefix+" - "+p)
+ synth.synchronized {
+ info(prefix+"Got: "+t.problem)
+ info(prefix+"Decomposed into:")
+ for(p <- sub) {
+ info(prefix+" - "+p)
+ }
}
Expanded(sub.map(TaskTryRules(_)))
--
GitLab