From 0471287b88c26b8e16a255e9c37cd3c70d8f48c7 Mon Sep 17 00:00:00 2001
From: Etienne Kneuss <ekneuss@gmail.com>
Date: Wed, 21 Nov 2012 01:42:45 +0100
Subject: [PATCH] Simplify various things
---
.../scala/leon/synthesis/Synthesizer.scala | 4 +--
.../leon/synthesis/search/AndOrGraph.scala | 5 +--
.../search/AndOrGraphDotConverter.scala | 2 +-
.../synthesis/search/AndOrGraphSearch.scala | 34 +++++++++++++------
4 files changed, 28 insertions(+), 17 deletions(-)
diff --git a/src/main/scala/leon/synthesis/Synthesizer.scala b/src/main/scala/leon/synthesis/Synthesizer.scala
index c5a5d448a..ae3717d3c 100644
--- a/src/main/scala/leon/synthesis/Synthesizer.scala
+++ b/src/main/scala/leon/synthesis/Synthesizer.scala
@@ -62,7 +62,7 @@ class Synthesizer(val reporter: Reporter,
}
case class TaskRunRule(problem: Problem, rule: Rule, app: RuleApplication) extends AOAndTask[Solution] {
- def cost = RuleApplicationCost(rule, app)
+ val cost = RuleApplicationCost(rule, app)
def composeSolution(sols: List[Solution]): Solution = {
app.onSuccess(sols)
@@ -72,7 +72,7 @@ class Synthesizer(val reporter: Reporter,
}
case class TaskTryRules(p: Problem) extends AOOrTask[Solution] {
- def cost = ProblemCost(p)
+ val cost = ProblemCost(p)
override def toString = p.toString
}
diff --git a/src/main/scala/leon/synthesis/search/AndOrGraph.scala b/src/main/scala/leon/synthesis/search/AndOrGraph.scala
index 6b5dc3aa7..918efbca9 100644
--- a/src/main/scala/leon/synthesis/search/AndOrGraph.scala
+++ b/src/main/scala/leon/synthesis/search/AndOrGraph.scala
@@ -35,8 +35,6 @@ class AndOrGraph[AT <: AOAndTask[S], OT <: AOOrTask[S], S <: AOSolution](val roo
abstract class OrTree extends Tree {
override val task: OT
-
- def isUnsolvable: Boolean = false
}
@@ -170,6 +168,7 @@ class AndOrGraph[AT <: AOAndTask[S], OT <: AOOrTask[S], S <: AOSolution](val roo
minAlternative = sub
notifyParent(solution.get)
+
case None =>
solution = Some(sol)
minAlternative = sub
@@ -183,8 +182,6 @@ class AndOrGraph[AT <: AOAndTask[S], OT <: AOOrTask[S], S <: AOSolution](val roo
parent.notifySolution(this, sol)
}
}
-
- override def isUnsolvable: Boolean = alternatives.isEmpty
}
class OrLeaf(val parent: AndNode, val task: OT) extends OrTree with Leaf {
diff --git a/src/main/scala/leon/synthesis/search/AndOrGraphDotConverter.scala b/src/main/scala/leon/synthesis/search/AndOrGraphDotConverter.scala
index 3b8577a83..d55039aa1 100644
--- a/src/main/scala/leon/synthesis/search/AndOrGraphDotConverter.scala
+++ b/src/main/scala/leon/synthesis/search/AndOrGraphDotConverter.scala
@@ -86,7 +86,7 @@ package leon.synthesis.search
case l: g.OrLeaf =>
(if (t.isSolved) "palegreen" else "white" , "filled,dashed")
case n: g.OrNode =>
- (if (t.isSolved) "palegreen" else if (t.isUnsolvable) "indianred1" else "white", "filled")
+ (if (t.isSolved) "palegreen" else "white", "filled")
}
drawNode(res, name, ot.cost, ot.toString, color, style)
diff --git a/src/main/scala/leon/synthesis/search/AndOrGraphSearch.scala b/src/main/scala/leon/synthesis/search/AndOrGraphSearch.scala
index a99a5be71..2125097c4 100644
--- a/src/main/scala/leon/synthesis/search/AndOrGraphSearch.scala
+++ b/src/main/scala/leon/synthesis/search/AndOrGraphSearch.scala
@@ -5,19 +5,34 @@ abstract class AndOrGraphSearch[AT <: AOAndTask[S],
S <: AOSolution](val g: AndOrGraph[AT, OT, S]) {
def nextLeaf: Option[g.Leaf] = {
- var c: g.Tree = g.tree
+ import collection.mutable.PriorityQueue
+
+ case class WT(t: g.Tree, prefixCost: Cost) extends Ordered[WT] {
+ val cost = t.minCost + prefixCost
+
+ def compare(that: WT) = that.cost.compare(this.cost) // DESC
+ }
+
+ val q = new PriorityQueue[WT]()
+ q += WT(g.tree, Cost.zero)
+
var res: Option[g.Leaf] = None
- while(res.isEmpty) {
- c match {
- case l: g.Leaf =>
+ while(res.isEmpty && !q.isEmpty) {
+ q.dequeue() match {
+ case WT(l: g.Leaf, c) =>
res = Some(l)
- case an: g.AndNode =>
- c = (an.subProblems -- an.subSolutions.keySet).values.minBy(_.minCost)
+ case WT(an: g.AndNode, c) =>
+ if (!an.isSolved) {
+ q ++= (an.subProblems -- an.subSolutions.keySet).values.map(n => WT(n, c + an.minCost))
+ }
+
+ case WT(on: g.OrNode, c) =>
+ if (!on.isSolved) {
+ q ++= on.alternatives.values.map(n => WT(n, c + on.minCost))
+ }
- case on: g.OrNode =>
- c = on.minAlternative
}
}
@@ -32,7 +47,7 @@ abstract class AndOrGraphSearch[AT <: AOAndTask[S],
var continue = true
def search(): Option[S] = {
- while (!g.tree.isSolved && continue && !g.tree.isUnsolvable) {
+ while (!g.tree.isSolved && continue) {
nextLeaf match {
case Some(l) =>
l match {
@@ -61,7 +76,6 @@ abstract class AndOrGraphSearch[AT <: AOAndTask[S],
continue = false
}
}
-
g.tree.solution
}
--
GitLab