From 7f9a3874ca5e01c254b0e46c42a61a52b9734ae6 Mon Sep 17 00:00:00 2001
From: Etienne Kneuss <ekneuss@gmail.com>
Date: Mon, 26 Nov 2012 15:46:45 +0100
Subject: [PATCH] Implement --firstonly for new dotconverter
---
src/main/scala/leon/synthesis/Synthesizer.scala | 2 +-
src/main/scala/leon/synthesis/search/AndOrGraph.scala | 6 +++---
.../leon/synthesis/search/AndOrGraphDotConverter.scala | 10 ++++++++--
3 files changed, 12 insertions(+), 6 deletions(-)
diff --git a/src/main/scala/leon/synthesis/Synthesizer.scala b/src/main/scala/leon/synthesis/Synthesizer.scala
index a5e11bfb1..51444a16b 100644
--- a/src/main/scala/leon/synthesis/Synthesizer.scala
+++ b/src/main/scala/leon/synthesis/Synthesizer.scala
@@ -59,7 +59,7 @@ class Synthesizer(val reporter: Reporter,
reporter.info("Finished in "+diff+"ms")
if (generateDerivationTrees) {
- new AndOrGraphDotConverter(search.g).writeFile("derivation.dot")
+ new AndOrGraphDotConverter(search.g, firstOnly).writeFile("derivation.dot")
}
res.getOrElse(Solution.choose(problem))
diff --git a/src/main/scala/leon/synthesis/search/AndOrGraph.scala b/src/main/scala/leon/synthesis/search/AndOrGraph.scala
index 1f3226535..297c10fa7 100644
--- a/src/main/scala/leon/synthesis/search/AndOrGraph.scala
+++ b/src/main/scala/leon/synthesis/search/AndOrGraph.scala
@@ -123,9 +123,9 @@ class AndOrGraph[AT <: AOAndTask[S], OT <: AOOrTask[S], S <: AOSolution](val roo
class OrNode(val parent: AndNode, var alternatives: Map[AT, AndTree], val task: OT) extends OrTree with Node[AndTree] {
- var triedAlternatives = Map[AT, AndTree]()
- var minAlternative: Tree = _
- var minCost = task.cost
+ var triedAlternatives = Map[AT, AndTree]()
+ var minAlternative: AndTree = _
+ var minCost = task.cost
def updateMin() {
if (!alternatives.isEmpty) {
diff --git a/src/main/scala/leon/synthesis/search/AndOrGraphDotConverter.scala b/src/main/scala/leon/synthesis/search/AndOrGraphDotConverter.scala
index fb42a6427..8e8da90a5 100644
--- a/src/main/scala/leon/synthesis/search/AndOrGraphDotConverter.scala
+++ b/src/main/scala/leon/synthesis/search/AndOrGraphDotConverter.scala
@@ -3,7 +3,7 @@ package leon.synthesis.search
class AndOrGraphDotConverter[AT <: AOAndTask[S],
OT <: AOOrTask[S],
- S <: AOSolution](val g: AndOrGraph[AT, OT, S]) {
+ S <: AOSolution](val g: AndOrGraph[AT, OT, S], firstOnly: Boolean) {
private[this] var _nextID = 0
@@ -65,7 +65,13 @@ package leon.synthesis.search
collect(sub, wasMin)
}
case on : g.OrNode =>
- for (sub <- (on.alternatives ++ on.triedAlternatives).values) {
+ val alternatives:Traversable[g.AndTree] = if (firstOnly) {
+ Option(on.minAlternative)
+ } else {
+ on.alternatives.values
+ }
+
+ for (sub <- alternatives) {
val isMin = sub == on.minAlternative
edges += ((n, sub, isMin))
collect(sub, isMin)
--
GitLab