From ae93c20412fd7e630db4475408ba8c3d4edef9f7 Mon Sep 17 00:00:00 2001
From: Etienne Kneuss <ekneuss@gmail.com>
Date: Thu, 29 Nov 2012 16:55:25 +0100
Subject: [PATCH] Implement partial solution reconstruction
---
.../scala/leon/synthesis/SimpleSearch.scala | 4 +-
.../scala/leon/synthesis/Synthesizer.scala | 7 +++-
.../search/AndOrGraphDotConverter.scala | 6 +--
.../search/AndOrGraphPartialSolution.scala | 37 +++++++++++++++++++
.../synthesis/search/AndOrGraphSearch.scala | 4 +-
5 files changed, 50 insertions(+), 8 deletions(-)
create mode 100644 src/main/scala/leon/synthesis/search/AndOrGraphPartialSolution.scala
diff --git a/src/main/scala/leon/synthesis/SimpleSearch.scala b/src/main/scala/leon/synthesis/SimpleSearch.scala
index 6b5f47c0a..b58d15cee 100644
--- a/src/main/scala/leon/synthesis/SimpleSearch.scala
+++ b/src/main/scala/leon/synthesis/SimpleSearch.scala
@@ -61,7 +61,7 @@ class SimpleSearch(synth: Synthesizer,
}
def search(): Option[Solution] = {
- while (!g.tree.isSolved && continue) {
+ while (!g.tree.isSolved && !isStopped) {
nextLeaf() match {
case Some(l) =>
l match {
@@ -73,7 +73,7 @@ class SimpleSearch(synth: Synthesizer,
onExpansion(ol, sub)
}
case None =>
- continue = false
+ stop()
}
}
g.tree.solution
diff --git a/src/main/scala/leon/synthesis/Synthesizer.scala b/src/main/scala/leon/synthesis/Synthesizer.scala
index b669335b9..97fc75e77 100644
--- a/src/main/scala/leon/synthesis/Synthesizer.scala
+++ b/src/main/scala/leon/synthesis/Synthesizer.scala
@@ -64,7 +64,12 @@ class Synthesizer(val context : LeonContext,
new AndOrGraphDotConverter(search.g, firstOnly).writeFile("derivation.dot")
}
- res.getOrElse(Solution.choose(problem))
+ res match {
+ case Some(solution) =>
+ solution
+ case None =>
+ new AndOrGraphPartialSolution(search.g, (task: TaskRunRule) => Solution.choose(task.problem)).getSolution
+ }
}
}
diff --git a/src/main/scala/leon/synthesis/search/AndOrGraphDotConverter.scala b/src/main/scala/leon/synthesis/search/AndOrGraphDotConverter.scala
index 8e8da90a5..03bb85e40 100644
--- a/src/main/scala/leon/synthesis/search/AndOrGraphDotConverter.scala
+++ b/src/main/scala/leon/synthesis/search/AndOrGraphDotConverter.scala
@@ -1,9 +1,9 @@
package leon.synthesis.search
- class AndOrGraphDotConverter[AT <: AOAndTask[S],
- OT <: AOOrTask[S],
- S <: AOSolution](val g: AndOrGraph[AT, OT, S], firstOnly: Boolean) {
+class AndOrGraphDotConverter[AT <: AOAndTask[S],
+ OT <: AOOrTask[S],
+ S <: AOSolution](val g: AndOrGraph[AT, OT, S], firstOnly: Boolean) {
private[this] var _nextID = 0
diff --git a/src/main/scala/leon/synthesis/search/AndOrGraphPartialSolution.scala b/src/main/scala/leon/synthesis/search/AndOrGraphPartialSolution.scala
new file mode 100644
index 000000000..151f40ae5
--- /dev/null
+++ b/src/main/scala/leon/synthesis/search/AndOrGraphPartialSolution.scala
@@ -0,0 +1,37 @@
+package leon.synthesis.search
+
+class AndOrGraphPartialSolution[AT <: AOAndTask[S],
+ OT <: AOOrTask[S],
+ S <: AOSolution](val g: AndOrGraph[AT, OT, S], missing: AT => S) {
+
+
+ def getSolution: S = {
+ solveOr(g.tree)
+ }
+
+ def solveAnd(t: g.AndTree): S = {
+ if (t.isSolved) {
+ t.solution.get
+ } else {
+ t match {
+ case l: g.AndLeaf =>
+ missing(t.task)
+ case n: g.AndNode =>
+ n.task.composeSolution(n.subProblems.values.map(solveOr(_)).toList)
+ }
+ }
+ }
+
+ def solveOr(t: g.OrTree): S = {
+ if (t.isSolved) {
+ t.solution.get
+ } else {
+ t match {
+ case l: g.OrLeaf =>
+ missing(l.parent.task)
+ case n: g.OrNode =>
+ solveAnd(n.minAlternative)
+ }
+ }
+ }
+}
diff --git a/src/main/scala/leon/synthesis/search/AndOrGraphSearch.scala b/src/main/scala/leon/synthesis/search/AndOrGraphSearch.scala
index f0116e1f4..01aff5047 100644
--- a/src/main/scala/leon/synthesis/search/AndOrGraphSearch.scala
+++ b/src/main/scala/leon/synthesis/search/AndOrGraphSearch.scala
@@ -56,10 +56,10 @@ abstract class AndOrGraphSearch[AT <: AOAndTask[S],
case class ExpandSuccess[T <: AOTask[S]](sol: S) extends ExpandResult[T]
case class ExpandFailure[T <: AOTask[S]]() extends ExpandResult[T]
- var continue = true
+ var isStopped = false
def stop() {
- continue = false
+ isStopped = true
}
def search(): Option[S]
--
GitLab