-
Etienne Kneuss authoredEtienne Kneuss authored
SimpleSearch.scala 2.08 KiB
package leon
package synthesis
import synthesis.search._
case class TaskRunRule(problem: Problem, rule: Rule, app: RuleApplication) extends AOAndTask[Solution] {
val cost = RuleApplicationCost(rule, app)
def composeSolution(sols: List[Solution]): Solution = {
app.onSuccess(sols)
}
override def toString = rule.name
}
case class TaskTryRules(p: Problem) extends AOOrTask[Solution] {
val cost = ProblemCost(p)
override def toString = p.toString
}
class SimpleSearch(synth: Synthesizer,
problem: Problem,
rules: Set[Rule]) extends AndOrGraphSearch[TaskRunRule, TaskTryRules, Solution](new AndOrGraph(TaskTryRules(problem))) {
import synth.reporter._
val sctx = SynthesisContext.fromSynthesizer(synth)
def expandAndTask(t: TaskRunRule): ExpandResult[TaskTryRules] = {
val prefix = "[%-20s] ".format(Option(t.rule).getOrElse("?"))
t.app.apply() match {
case RuleSuccess(sol) =>
info(prefix+"Got: "+t.problem)
info(prefix+"Solved with: "+sol)
ExpandSuccess(sol)
case RuleDecomposed(sub, onSuccess) =>
info(prefix+"Got: "+t.problem)
info(prefix+"Decomposed into:")
for(p <- sub) {
info(prefix+" - "+p)
}
Expanded(sub.map(TaskTryRules(_)))
case RuleApplicationImpossible =>
ExpandFailure()
}
}
def expandOrTask(t: TaskTryRules): ExpandResult[TaskRunRule] = {
val sub = rules.flatMap ( r => r.attemptToApplyOn(sctx, t.p).alternatives.map(TaskRunRule(t.p, r, _)) )
if (!sub.isEmpty) {
Expanded(sub.toList)
} else {
ExpandFailure()
}
}
def search(): Option[Solution] = {
while (!g.tree.isSolved && continue) {
nextLeaf() match {
case Some(l) =>
l match {
case al: g.AndLeaf =>
val sub = expandAndTask(al.task)
onExpansion(al, sub)
case ol: g.OrLeaf =>
val sub = expandOrTask(ol.task)
onExpansion(ol, sub)
}
case None =>
continue = false
}
}
g.tree.solution
}
}