diff --git a/src/main/scala/leon/synthesis/Synthesizer.scala b/src/main/scala/leon/synthesis/Synthesizer.scala index a5e11bfb1a4e7e0874d44491d57318a877d122f3..51444a16b17b42e70acf0b48a23fcb204261a082 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 1f32265357b5c03a1e1e5e44fd815cdda16196b2..297c10fa7407f8a6443f1b06d79022802c986d96 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 fb42a64279b6a4a3a96970a3b665c10e0fe569c0..8e8da90a5ba390f6586a78e56b799f715d770077 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)