Skip to content
Snippets Groups Projects
Commit 53df716a authored by Régis Blanc's avatar Régis Blanc
Browse files

Merge branch 'master' of laragit.epfl.ch:projects/leon-2.0

parents fa8daab1 022e7257
No related branches found
No related tags found
No related merge requests found
...@@ -62,6 +62,8 @@ class Synthesizer(val reporter: Reporter, ...@@ -62,6 +62,8 @@ class Synthesizer(val reporter: Reporter,
} }
*/ */
new AndOrGraphDotConverter(search.g).writeFile("test.dot")
res.getOrElse(Solution.choose(problem)) res.getOrElse(Solution.choose(problem))
} }
...@@ -72,16 +74,17 @@ class Synthesizer(val reporter: Reporter, ...@@ -72,16 +74,17 @@ class Synthesizer(val reporter: Reporter,
app.onSuccess(sols) app.onSuccess(sols)
} }
override def toString = rule.name+" ON "+problem override def toString = rule.name
} }
case class TaskTryRules(p: Problem) extends AOOrTask[Solution] { case class TaskTryRules(p: Problem) extends AOOrTask[Solution] {
def cost = ProblemCost(p) def cost = ProblemCost(p)
override def toString = " Splitting "+problem override def toString = p.toString
} }
class AOSearch(problem: Problem, rules: Set[Rule]) extends AndOrGraphSearch[TaskRunRule, TaskTryRules, Solution](new AndOrGraph(TaskTryRules(problem))) { class AOSearch(problem: Problem,
rules: Set[Rule]) extends AndOrGraphSearch[TaskRunRule, TaskTryRules, Solution](new AndOrGraph(TaskTryRules(problem))) {
def processAndLeaf(t: TaskRunRule) = { def processAndLeaf(t: TaskRunRule) = {
val prefix = "[%-20s] ".format(Option(t.rule).getOrElse("?")) val prefix = "[%-20s] ".format(Option(t.rule).getOrElse("?"))
......
...@@ -52,7 +52,7 @@ class AndOrGraph[AT <: AOAndTask[S], OT <: AOOrTask[S], S <: AOSolution](val roo ...@@ -52,7 +52,7 @@ class AndOrGraph[AT <: AOAndTask[S], OT <: AOOrTask[S], S <: AOSolution](val roo
} }
case class AndNode(parent: OrNode, subTasks: List[OT], task: AT) extends AndTree with Node[OrTree] { class AndNode(val parent: OrNode, val subTasks: List[OT], val task: AT) extends AndTree with Node[OrTree] {
var subProblems = Map[OT, OrTree]() var subProblems = Map[OT, OrTree]()
var subSolutions = Map[OT, S]() var subSolutions = Map[OT, S]()
...@@ -74,8 +74,8 @@ class AndOrGraph[AT <: AOAndTask[S], OT <: AOOrTask[S], S <: AOSolution](val roo ...@@ -74,8 +74,8 @@ class AndOrGraph[AT <: AOAndTask[S], OT <: AOOrTask[S], S <: AOSolution](val roo
} }
def expandLeaf(l: OrLeaf, succ: List[AT]) { def expandLeaf(l: OrLeaf, succ: List[AT]) {
val n = OrNode(this, Map(), l.task) val n = new OrNode(this, Map(), l.task)
n.alternatives = succ.map(t => t -> AndLeaf(n, t)).toMap n.alternatives = succ.map(t => t -> new AndLeaf(n, t)).toMap
n.minAlternative = n.computeMin n.minAlternative = n.computeMin
subProblems += l.task -> n subProblems += l.task -> n
...@@ -105,15 +105,15 @@ class AndOrGraph[AT <: AOAndTask[S], OT <: AOOrTask[S], S <: AOSolution](val roo ...@@ -105,15 +105,15 @@ class AndOrGraph[AT <: AOAndTask[S], OT <: AOOrTask[S], S <: AOSolution](val roo
object RootNode extends OrLeaf(null, root) { object RootNode extends OrLeaf(null, root) {
override def expandWith(succ: List[AT]) { override def expandWith(succ: List[AT]) {
val n = OrNode(null, Map(), root) val n = new OrNode(null, Map(), root)
n.alternatives = succ.map(t => t -> AndLeaf(n, t)).toMap n.alternatives = succ.map(t => t -> new AndLeaf(n, t)).toMap
n.minAlternative = n.computeMin n.minAlternative = n.computeMin
tree = n tree = n
} }
} }
case class AndLeaf(parent: OrNode, task: AT) extends AndTree with Leaf { class AndLeaf(val parent: OrNode, val task: AT) extends AndTree with Leaf {
def expandWith(succ: List[OT]) { def expandWith(succ: List[OT]) {
parent.expandLeaf(this, succ) parent.expandLeaf(this, succ)
} }
...@@ -121,7 +121,7 @@ class AndOrGraph[AT <: AOAndTask[S], OT <: AOOrTask[S], S <: AOSolution](val roo ...@@ -121,7 +121,7 @@ class AndOrGraph[AT <: AOAndTask[S], OT <: AOOrTask[S], S <: AOSolution](val roo
} }
case class OrNode(parent: AndNode, var alternatives: Map[AT, AndTree], task: OT) extends OrTree with Node[AndTree] { class OrNode(val parent: AndNode, var alternatives: Map[AT, AndTree], val task: OT) extends OrTree with Node[AndTree] {
var minAlternative: Tree = _ var minAlternative: Tree = _
def minCost: C = minAlternative.minCost def minCost: C = minAlternative.minCost
...@@ -144,8 +144,8 @@ class AndOrGraph[AT <: AOAndTask[S], OT <: AOOrTask[S], S <: AOSolution](val roo ...@@ -144,8 +144,8 @@ class AndOrGraph[AT <: AOAndTask[S], OT <: AOOrTask[S], S <: AOSolution](val roo
} }
def expandLeaf(l: AndLeaf, succ: List[OT]) { def expandLeaf(l: AndLeaf, succ: List[OT]) {
val n = AndNode(this, succ, l.task) val n = new AndNode(this, succ, l.task)
n.subProblems = succ.map(t => t -> OrLeaf(n, t)).toMap n.subProblems = succ.map(t => t -> new OrLeaf(n, t)).toMap
n.minCost = n.computeCost n.minCost = n.computeCost
alternatives += l.task -> n alternatives += l.task -> n
...@@ -177,7 +177,7 @@ class AndOrGraph[AT <: AOAndTask[S], OT <: AOOrTask[S], S <: AOSolution](val roo ...@@ -177,7 +177,7 @@ class AndOrGraph[AT <: AOAndTask[S], OT <: AOOrTask[S], S <: AOSolution](val roo
override def isUnsolvable: Boolean = alternatives.isEmpty override def isUnsolvable: Boolean = alternatives.isEmpty
} }
case class OrLeaf(parent: AndNode, task: OT) extends OrTree with Leaf { class OrLeaf(val parent: AndNode, val task: OT) extends OrTree with Leaf {
def expandWith(succ: List[AT]) { def expandWith(succ: List[AT]) {
parent.expandLeaf(this, succ) parent.expandLeaf(this, succ)
} }
......
package leon.synthesis.search
class AndOrGraphDotConverter[AT <: AOAndTask[S],
OT <: AOOrTask[S],
S <: AOSolution](val g: AndOrGraph[AT, OT, S]) {
private[this] var _nextID = 0
def freshName(prefix: String) = {
_nextID += 1
prefix+_nextID
}
override def toString: String = {
val res = new StringBuffer()
res append "digraph D {\n"
// Print all nodes
val (nodes, edges) = decomposeGraph
var nodesToNames = Map[g.Tree, String]()
for (n <- nodes) {
val name = freshName("node")
n match {
case ot: g.OrTree =>
drawOrNode(res, name, ot)
case at: g.AndTree =>
drawAndNode(res, name, at)
}
nodesToNames += n -> name
}
for ((f,t, isMin) <- edges) {
val label = f match {
case ot: g.OrTree =>
"or"
case at: g.AndTree =>
""
}
res append " "+nodesToNames(f)+" -> "+nodesToNames(t) +" [label=\""+label+"\""+(if (isMin) ", style=bold" else "")+"]\n";
}
res append "}\n"
res.toString
}
def decomposeGraph: (Set[g.Tree], Set[(g.Tree, g.Tree, Boolean)]) = {
var nodes = Set[g.Tree]()
var edges = Set[(g.Tree, g.Tree, Boolean)]()
def collect(n: g.Tree, wasMin: Boolean) {
nodes += n
n match {
case an : g.AndNode =>
for (sub <- an.subProblems.values) {
edges += ((n, sub, wasMin))
collect(sub, wasMin)
}
case on : g.OrNode =>
for (sub <- on.alternatives.values) {
val isMin = sub == on.minAlternative
edges += ((n, sub, isMin))
collect(sub, isMin)
}
case _ =>
// ignore leaves
}
}
collect(g.tree, false)
(nodes, edges)
}
def drawOrNode(res: StringBuffer, name: String, t: g.OrTree) {
val ot = t.task
val (color, style, shape) = t match {
case l: g.OrLeaf =>
(if (t.isSolved) "palegreen" else "white" , "filled,dashed", "rect")
case n: g.OrNode =>
(if (t.isSolved) "palegreen" else if (t.isUnsolvable) "indianred1" else "white", "filled", "rect")
}
res append " "+name+" [label=\"("+ot.cost.value+") "+ot.toString+"\", shape="+shape+", fillcolor=\""+color+"\", style=\""+style+"\"]\n"
}
def drawAndNode(res: StringBuffer, name: String, t: g.AndTree) {
val at = t.task
val (color, style, shape) = t match {
case l: g.AndLeaf =>
(if (t.isSolved) "palegreen" else "white" , "filled,dashed", "rect")
case n: g.AndNode =>
(if (t.isSolved) "palegreen" else "white", "filled", "rect")
}
res append " "+name+" [label=\"("+at.cost.value+") "+at.toString+"\", shape="+shape+", fillcolor=\""+color+"\", style=\""+style+"\"]\n"
}
/** Writes the graph to a file readable with GraphViz. */
def writeFile(fname: String) {
import java.io.{BufferedWriter, FileWriter}
val out = new BufferedWriter(new FileWriter(fname))
out.write(toString)
out.close()
}
}
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment