From 6a5b1b67ca7d68eba97edeb35fb4db5b17036816 Mon Sep 17 00:00:00 2001
From: Etienne Kneuss <ekneuss@gmail.com>
Date: Thu, 6 Dec 2012 18:44:36 +0100
Subject: [PATCH] Reintroduce luckytests fix two problems arising from
parallelism of task dispatching
---
.../scala/leon/solvers/z3/FairZ3Solver.scala | 2 +-
.../leon/synthesis/search/AndOrGraph.scala | 22 +++++++++++--------
.../synthesis/search/AndOrGraphSearch.scala | 4 ++--
3 files changed, 16 insertions(+), 12 deletions(-)
diff --git a/src/main/scala/leon/solvers/z3/FairZ3Solver.scala b/src/main/scala/leon/solvers/z3/FairZ3Solver.scala
index 3646cc2d8..70368d7c8 100644
--- a/src/main/scala/leon/solvers/z3/FairZ3Solver.scala
+++ b/src/main/scala/leon/solvers/z3/FairZ3Solver.scala
@@ -447,7 +447,7 @@ class FairZ3Solver(context : LeonContext) extends Solver(context) with AbstractZ
foundAnswer(Some(false), core = z3CoreToCore(solver.getUnsatCore))
case Some(true) =>
//reporter.info("SAT WITHOUT Blockers")
- if (Settings.luckyTest && !forceStop && false) {
+ if (Settings.luckyTest && !forceStop) {
// we might have been lucky :D
val (wereWeLucky, cleanModel) = validateAndDeleteModel(solver.getModel, entireFormula, varsInVC)
if(wereWeLucky) {
diff --git a/src/main/scala/leon/synthesis/search/AndOrGraph.scala b/src/main/scala/leon/synthesis/search/AndOrGraph.scala
index 5a61217a0..48f38675a 100644
--- a/src/main/scala/leon/synthesis/search/AndOrGraph.scala
+++ b/src/main/scala/leon/synthesis/search/AndOrGraph.scala
@@ -142,15 +142,19 @@ class AndOrGraph[AT <: AOAndTask[S], OT <: AOOrTask[S], S](val root: OT, val cos
}
def unsolvable(l: AndTree) {
- triedAlternatives += l.task -> alternatives(l.task)
- alternatives -= l.task
-
-
- if (alternatives.isEmpty) {
- isUnsolvable = true
- parent.unsolvable(this)
- } else {
- updateMin()
+ if (alternatives contains l.task) {
+ triedAlternatives += l.task -> alternatives(l.task)
+ alternatives -= l.task
+
+
+ if (alternatives.isEmpty) {
+ isUnsolvable = true
+ if (parent ne null) {
+ parent.unsolvable(this)
+ }
+ } else {
+ updateMin()
+ }
}
}
diff --git a/src/main/scala/leon/synthesis/search/AndOrGraphSearch.scala b/src/main/scala/leon/synthesis/search/AndOrGraphSearch.scala
index bf3fed4e9..e8d402b4f 100644
--- a/src/main/scala/leon/synthesis/search/AndOrGraphSearch.scala
+++ b/src/main/scala/leon/synthesis/search/AndOrGraphSearch.scala
@@ -15,7 +15,7 @@ abstract class AndOrGraphSearch[AT <: AOAndTask[S],
def collectFromAnd(at: g.AndTree, costs: List[Int]) {
val newCosts = at.minCost.value :: costs
- if (!at.isSolved) {
+ if (!at.isSolved && !at.isUnsolvable) {
at match {
case l: g.Leaf =>
collectLeaf(WL(l, newCosts.reverse))
@@ -30,7 +30,7 @@ abstract class AndOrGraphSearch[AT <: AOAndTask[S],
def collectFromOr(ot: g.OrTree, costs: List[Int]) {
val newCosts = ot.minCost.value :: costs
- if (!ot.isSolved) {
+ if (!ot.isSolved && !ot.isUnsolvable) {
ot match {
case l: g.Leaf =>
collectLeaf(WL(l, newCosts.reverse))
--
GitLab