Skip to content
Snippets Groups Projects
Commit 20bc1c05 authored by Etienne Kneuss's avatar Etienne Kneuss
Browse files

Organize things

parent ba4e38ea
Branches
Tags
No related merge requests found
package leon.synthesis.search
trait Cost extends Ordered[Cost] {
def +(that: Cost): Cost = CostFixed(value + that.value)
def value: Int
def compare(that: Cost) = this.value - that.value
}
case class CostFixed(value: Int) extends Cost
object Cost {
val zero = new CostFixed(0)
}
trait AOTask[S <: AOSolution] {
def cost: Cost
}
......@@ -198,68 +184,3 @@ class AndOrGraph[AT <: AOAndTask[S], OT <: AOOrTask[S], S <: AOSolution](val roo
}
}
abstract class AndOrGraphSearch[AT <: AOAndTask[S], OT <: AOOrTask[S], S <: AOSolution](val g: AndOrGraph[AT, OT, S]) {
import collection.mutable.PriorityQueue
def nextLeaf: Option[g.Leaf] = {
var c: g.Tree = g.tree
var res: Option[g.Leaf] = None
while(res.isEmpty) {
c match {
case l: g.Leaf =>
res = Some(l)
case an: g.AndNode =>
c = (an.subProblems -- an.subSolutions.keySet).values.minBy(_.minCost)
case on: g.OrNode =>
c = on.minAlternative
}
}
res
}
abstract class ExpandResult[T <: AOTask[S]]
case class Expanded[T <: AOTask[S]](sub: List[T]) extends ExpandResult[T]
case class ExpandSuccess[T <: AOTask[S]](sol: S) extends ExpandResult[T]
case class ExpandFailure[T <: AOTask[S]]() extends ExpandResult[T]
var continue = true
def search(): Option[S] = {
while (!g.tree.isSolved && continue && !g.tree.isUnsolvable) {
nextLeaf match {
case Some(l) =>
l match {
case al: g.AndLeaf =>
processAndLeaf(al.task) match {
case Expanded(ls) =>
al.expandWith(ls)
case r @ ExpandSuccess(sol) =>
al.parent.notifySolution(al, sol)
case _ =>
al.parent.unsolvable(al)
}
case ol: g.OrLeaf =>
processOrLeaf(ol.task) match {
case Expanded(ls) =>
ol.expandWith(ls)
case r @ ExpandSuccess(sol) =>
ol.parent.notifySolution(ol, sol)
case _ =>
ol.parent.unsolvable(ol)
}
}
case None =>
continue = false
}
}
g.tree.solution
}
def processAndLeaf(l: AT): ExpandResult[OT]
def processOrLeaf(l: OT): ExpandResult[AT]
}
package leon.synthesis.search
abstract class AndOrGraphSearch[AT <: AOAndTask[S],
OT <: AOOrTask[S],
S <: AOSolution](val g: AndOrGraph[AT, OT, S]) {
def nextLeaf: Option[g.Leaf] = {
var c: g.Tree = g.tree
var res: Option[g.Leaf] = None
while(res.isEmpty) {
c match {
case l: g.Leaf =>
res = Some(l)
case an: g.AndNode =>
c = (an.subProblems -- an.subSolutions.keySet).values.minBy(_.minCost)
case on: g.OrNode =>
c = on.minAlternative
}
}
res
}
abstract class ExpandResult[T <: AOTask[S]]
case class Expanded[T <: AOTask[S]](sub: List[T]) extends ExpandResult[T]
case class ExpandSuccess[T <: AOTask[S]](sol: S) extends ExpandResult[T]
case class ExpandFailure[T <: AOTask[S]]() extends ExpandResult[T]
var continue = true
def search(): Option[S] = {
while (!g.tree.isSolved && continue && !g.tree.isUnsolvable) {
nextLeaf match {
case Some(l) =>
l match {
case al: g.AndLeaf =>
processAndLeaf(al.task) match {
case Expanded(ls) =>
al.expandWith(ls)
case r @ ExpandSuccess(sol) =>
al.parent.notifySolution(al, sol)
case _ =>
al.parent.unsolvable(al)
}
case ol: g.OrLeaf =>
processOrLeaf(ol.task) match {
case Expanded(ls) =>
ol.expandWith(ls)
case r @ ExpandSuccess(sol) =>
ol.parent.notifySolution(ol, sol)
case _ =>
ol.parent.unsolvable(ol)
}
}
case None =>
continue = false
}
}
g.tree.solution
}
def processAndLeaf(l: AT): ExpandResult[OT]
def processOrLeaf(l: OT): ExpandResult[AT]
}
package leon.synthesis.search
trait Cost extends Ordered[Cost] {
def +(that: Cost): Cost = CostFixed(value + that.value)
def value: Int
def compare(that: Cost) = this.value - that.value
}
case class CostFixed(value: Int) extends Cost
object Cost {
val zero = new CostFixed(0)
}
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment