diff --git a/src/main/scala/leon/synthesis/Rules.scala b/src/main/scala/leon/synthesis/Rules.scala
index e835637a49d32d5c2035e3925186134c15c4673f..c1b392774c2f61bd88a7d395691c1c44fdf8deed 100644
--- a/src/main/scala/leon/synthesis/Rules.scala
+++ b/src/main/scala/leon/synthesis/Rules.scala
@@ -17,7 +17,7 @@ object Rules {
abstract class Rule(val name: String, val synth: Synthesizer) {
- def isApplicable(p: Problem, parent: Task): List[Task]
+ def isApplicable(task: Task): List[DecomposedTask]
def subst(what: Tuple2[Identifier, Expr], in: Expr): Expr = replace(Map(Variable(what._1) -> what._2), in)
@@ -25,7 +25,9 @@ abstract class Rule(val name: String, val synth: Synthesizer) {
}
class OnePoint(synth: Synthesizer) extends Rule("One-point", synth) {
- def isApplicable(p: Problem, parent: Task): List[Task] = {
+ def isApplicable(task: Task): List[DecomposedTask] = {
+
+ val p = task.problem
p.phi match {
case TopLevelAnds(exprs) =>
@@ -54,7 +56,7 @@ class OnePoint(synth: Synthesizer) extends Rule("One-point", synth) {
case _ => Solution.none
}
- List(new Task(synth, parent, this, p, List(newProblem), onSuccess, 100))
+ List(new DecomposedTask(synth, task.parent, p, 100, this, List(newProblem), onSuccess))
} else {
Nil
}
@@ -67,7 +69,9 @@ class OnePoint(synth: Synthesizer) extends Rule("One-point", synth) {
}
class Ground(synth: Synthesizer) extends Rule("Ground", synth) {
- def isApplicable(p: Problem, parent: Task): List[Task] = {
+ def isApplicable(task: Task): List[DecomposedTask] = {
+ val p = task.problem
+
if (p.as.isEmpty) {
val tpe = TupleType(p.xs.map(_.getType))
@@ -78,13 +82,13 @@ class Ground(synth: Synthesizer) extends Rule("Ground", synth) {
case Nil => Solution(BooleanLiteral(true), Tuple(p.xs.map(model)).setType(tpe), 200)
}
- List(new Task(synth, parent, this, p, Nil, onSuccess, 200))
+ List(new DecomposedTask(synth, task.parent, p, 200, this, Nil, onSuccess))
case (Some(false), model) =>
val onSuccess: List[Solution] => Solution = {
case Nil => Solution(BooleanLiteral(false), Error(p.phi+" is UNSAT!").setType(tpe), 200)
}
- List(new Task(synth, parent, this, p, Nil, onSuccess, 200))
+ List(new DecomposedTask(synth, task.parent, p, 200, this, Nil, onSuccess))
case _ =>
Nil
}
@@ -95,7 +99,8 @@ class Ground(synth: Synthesizer) extends Rule("Ground", synth) {
}
class CaseSplit(synth: Synthesizer) extends Rule("Case-Split", synth) {
- def isApplicable(p: Problem, parent: Task): List[Task] = {
+ def isApplicable(task: Task): List[DecomposedTask] = {
+ val p = task.problem
p.phi match {
case Or(Seq(o1, o2)) =>
val sub1 = Problem(p.as, o1, p.xs)
@@ -106,7 +111,7 @@ class CaseSplit(synth: Synthesizer) extends Rule("Case-Split", synth) {
case _ => Solution.none
}
- List(new Task(synth, parent, this, p, List(sub1, sub2), onSuccess, 100))
+ List(new DecomposedTask(synth, task.parent, p, 100, this, List(sub1, sub2), onSuccess))
case _ =>
Nil
}
@@ -114,7 +119,9 @@ class CaseSplit(synth: Synthesizer) extends Rule("Case-Split", synth) {
}
class Assert(synth: Synthesizer) extends Rule("Assert", synth) {
- def isApplicable(p: Problem, parent: Task): List[Task] = {
+ def isApplicable(task: Task): List[DecomposedTask] = {
+ val p = task.problem
+
p.phi match {
case TopLevelAnds(exprs) =>
val xsSet = p.xs.toSet
@@ -128,14 +135,16 @@ class Assert(synth: Synthesizer) extends Rule("Assert", synth) {
case _ => Solution.none
}
- List(new Task(synth, parent, this, p, Nil, onSuccess, 150))
+ List(new DecomposedTask(synth, task.parent, p, 150, this, Nil, onSuccess))
} else {
val onSuccess: List[Solution] => Solution = {
case List(s) => Solution(And(s.pre +: exprsA), s.term, 150)
case _ => Solution.none
}
- List(new Task(synth, parent, this, p, List(p.copy(phi = And(others))), onSuccess, 150))
+ val sub = p.copy(phi = And(others))
+
+ List(new DecomposedTask(synth, task.parent, p, 150, this, List(sub), onSuccess))
}
} else {
Nil
@@ -147,7 +156,8 @@ class Assert(synth: Synthesizer) extends Rule("Assert", synth) {
}
class UnusedInput(synth: Synthesizer) extends Rule("UnusedInput", synth) {
- def isApplicable(p: Problem, parent: Task): List[Task] = {
+ def isApplicable(task: Task): List[DecomposedTask] = {
+ val p = task.problem
val unused = p.as.toSet -- variablesOf(p.phi)
if (!unused.isEmpty) {
@@ -158,7 +168,7 @@ class UnusedInput(synth: Synthesizer) extends Rule("UnusedInput", synth) {
case _ => Solution.none
}
- List(new Task(synth, parent, this, p, List(sub), onSuccess, 300))
+ List(new DecomposedTask(synth, task.parent, p, 300, this, List(sub), onSuccess))
} else {
Nil
}
diff --git a/src/main/scala/leon/synthesis/Synthesizer.scala b/src/main/scala/leon/synthesis/Synthesizer.scala
index e17b34683ebf446ba17f2d1dbd71eed2566e1609..754c740f079f648724e5bb0af4720644ba345d9e 100644
--- a/src/main/scala/leon/synthesis/Synthesizer.scala
+++ b/src/main/scala/leon/synthesis/Synthesizer.scala
@@ -17,49 +17,34 @@ class Synthesizer(val r: Reporter, val solvers: List[Solver]) {
def synthesize(p: Problem, rules: List[Rule]): Solution = {
- def applyRules(p: Problem, parent: Task): List[Task] = {
- rules.flatMap(_.isApplicable(p, parent))
- }
-
val workList = new PriorityQueue[Task]()
-
val rootTask = new RootTask(this, p)
workList += rootTask
-
solution = None
while (!workList.isEmpty && solution.isEmpty) {
val task = workList.dequeue()
- task.subProblems match {
- case Nil =>
- throw new Exception("Such tasks shouldbe handled immediately")
- case subProblems =>
- for (sp <- subProblems) {
- info("Now handling: "+sp)
-
- val alternatives = applyRules(sp, task)
-
- alternatives.find(_.isSuccess) match {
- case Some(ss) =>
- ss.succeeded()
- case None =>
- info(" => Possible Next Steps:")
- alternatives.foreach(t => info(" - "+t.description))
- workList ++= alternatives
- }
-
- // We are stuck
- if (alternatives.isEmpty) {
- // I give up
- val sol = Solution.choose(sp)
- warning(" => Solved (by choose): "+sp+" ⊢ "+sol)
- task.subSucceeded(sp, sol)
- }
- }
+ info("Now handling: "+task.problem)
+
+ val alternatives = rules.flatMap(_.isApplicable(task))
+
+ alternatives.find(_.isSuccess) match {
+ case Some(ss) =>
+ ss.succeeded()
+ case None =>
+ info(" => Possible Next Steps:")
+ alternatives.foreach(t => info(" - "+t.description))
+ workList ++= alternatives.flatMap(_.subTasks)
}
+ // We are stuck
+ if (alternatives.isEmpty) {
+ val sol = Solution.choose(task.problem)
+ warning(" => I give up: "+task+" ⊢ "+sol)
+ onTaskSucceeded(task, sol)
+ }
}
solution.getOrElse(Solution.none)
@@ -79,13 +64,12 @@ class Synthesizer(val r: Reporter, val solvers: List[Solver]) {
}
def onTaskSucceeded(task: Task, solution: Solution) {
- task match {
- case rt: RootTask =>
- info(" SUCCESS!")
- this.solution = Some(solution)
- case t: Task =>
- info(" => Solved "+task.problem+" ⊢ "+solution)
- t.parent.subSucceeded(t.problem, solution)
+ if (task.parent eq null) {
+ info(" SUCCESS!")
+ this.solution = Some(solution)
+ } else {
+ info(" => Solved "+task.problem+" ⊢ "+solution)
+ task.parent.subSucceeded(task.problem, solution)
}
}
diff --git a/src/main/scala/leon/synthesis/Task.scala b/src/main/scala/leon/synthesis/Task.scala
index fd6702c812e695882e77e2609da77ae6aaa9dbc5..71e0f4f18bc72cb464e4e85593ae366772e06aaa 100644
--- a/src/main/scala/leon/synthesis/Task.scala
+++ b/src/main/scala/leon/synthesis/Task.scala
@@ -1,20 +1,28 @@
package leon
package synthesis
-class Task(
- val synth: Synthesizer,
- val parent: Task,
- val rule: Rule,
- val problem: Problem,
- val subProblems: List[Problem],
- val onSuccess: List[Solution] => Solution,
- val score: Score
- ) extends Ordered[Task] {
-
- var subSolutions = Map[Problem, Solution]()
+class Task(val synth: Synthesizer,
+ val parent: DecomposedTask,
+ val problem: Problem,
+ val score: Score) extends Ordered[Task] {
def compare(that: Task) = this.score - that.score
+ override def toString = "("+score+") " +problem
+}
+
+class DecomposedTask(synth: Synthesizer,
+ parent: DecomposedTask,
+ problem: Problem,
+ score: Score,
+ val rule: Rule,
+ val subProblems: List[Problem],
+ val onSuccess: List[Solution] => Solution) extends Task(synth, parent, problem, score) {
+
+ def subTasks = subProblems.map(new Task(synth, this, _, score))
+
+ var subSolutions = Map[Problem, Solution]()
+
def isSuccess = subProblems.isEmpty
def succeeded() {
@@ -40,9 +48,7 @@ class Task(
}
}
- override def toString = description
-
def description = "by "+rule.name+"("+score+"): "+problem +" ⟿ "+subProblems.mkString(" ; ")
}
-class RootTask(synth: Synthesizer, p: Problem) extends Task(synth, null, null, p, List(p), xs => xs.head, 0)
+class RootTask(synth: Synthesizer, p: Problem) extends Task(synth, null, p, 0)