diff --git a/src/main/scala/leon/synthesis/DerivationTree.scala b/src/main/scala/leon/synthesis/DerivationTree.scala
index 62fea60b1341ed39acd4248b56782c4769987e7e..370b10f79590ed031d6fcf987fb23e917d0e1b7e 100644
--- a/src/main/scala/leon/synthesis/DerivationTree.scala
+++ b/src/main/scala/leon/synthesis/DerivationTree.scala
@@ -2,17 +2,20 @@ package leon
package synthesis
class DerivationTree(root: RootTask) {
- var store = Map[DecomposedTask, Map[Problem, DecomposedTask]]().withDefaultValue(Map())
+ var store = Map[SimpleTask, Map[Problem, SimpleTask]]().withDefaultValue(Map())
var solutions = Map[Task, Solution]()
def recordSolutionFor(task: Task, solution: Solution) = task match {
- case dt: DecomposedTask =>
+ /*
+ case dt: SimpleTask =>
if (dt.parent ne null) {
store += dt.parent -> (store(dt.parent) + (task.problem -> dt))
}
solutions += dt -> solution
case _ =>
+ */
+ case _ =>
}
private[this] var _nextID = 0
@@ -41,12 +44,13 @@ class DerivationTree(root: RootTask) {
}
}
- def printTask(t: DecomposedTask) {
+ def printTask(t: SimpleTask) {
val node = nameFor(t, "task");
+ /*
res append " "+node+" [ label = <<TABLE BORDER=\"0\" CELLBORDER=\"1\" CELLSPACING=\"0\"><TR><TD BORDER=\"0\">"+t.rule.name+"</TD></TR><TR><TD BGCOLOR=\"indianred1\">"+t.problem+"</TD></TR><TR><TD BGCOLOR=\"greenyellow\">"+solutions.getOrElse(t, "?")+"</TD></TR></TABLE>> shape = \"none\" ];\n"
-
+ */
for ((_, task) <- store(t)) {
res append nameFor(task, "task") +" -> " + " "+node+";\n"
diff --git a/src/main/scala/leon/synthesis/Rules.scala b/src/main/scala/leon/synthesis/Rules.scala
index b8ea78b0dcbe786e8d649afdae9b62a441250de9..ea1220929dd39531aeffe8d18942498d50d4ebf4 100644
--- a/src/main/scala/leon/synthesis/Rules.scala
+++ b/src/main/scala/leon/synthesis/Rules.scala
@@ -21,9 +21,14 @@ object Rules {
)
}
+abstract class RuleResult
+case object RuleInapplicable extends RuleResult
+case class RuleSuccess(solution: Solution) extends RuleResult
+case class RuleDecomposed(subProblems: List[Problem], onSuccess: List[Solution] => Solution) extends RuleResult
+
abstract class Rule(val name: String, val synth: Synthesizer) {
- def isApplicable(task: Task): List[DecomposedTask]
+ def applyOn(task: Task): RuleResult
def subst(what: Tuple2[Identifier, Expr], in: Expr): Expr = replace(Map(Variable(what._1) -> what._2), in)
@@ -36,7 +41,7 @@ abstract class Rule(val name: String, val synth: Synthesizer) {
}
class OnePoint(synth: Synthesizer) extends Rule("One-point", synth) {
- def isApplicable(task: Task): List[DecomposedTask] = {
+ def applyOn(task: Task): RuleResult = {
val p = task.problem
@@ -67,15 +72,15 @@ class OnePoint(synth: Synthesizer) extends Rule("One-point", synth) {
case _ => Solution.none
}
- List(task.decompose(this, List(newProblem), onSuccess, 100))
+ RuleDecomposed(List(newProblem), onSuccess)
} else {
- Nil
+ RuleInapplicable
}
}
}
class Ground(synth: Synthesizer) extends Rule("Ground", synth) {
- def isApplicable(task: Task): List[DecomposedTask] = {
+ def applyOn(task: Task): RuleResult = {
val p = task.problem
if (p.as.isEmpty) {
@@ -84,20 +89,20 @@ class Ground(synth: Synthesizer) extends Rule("Ground", synth) {
synth.solveSAT(p.phi) match {
case (Some(true), model) =>
- List(task.solveUsing(this, Solution(BooleanLiteral(true), Tuple(p.xs.map(id => model.getOrElse(id, simplestValue(Variable(id))))).setType(tpe), 200), 200))
+ RuleSuccess(Solution(BooleanLiteral(true), Tuple(p.xs.map(id => model.getOrElse(id, simplestValue(Variable(id))))).setType(tpe)))
case (Some(false), model) =>
- List(task.solveUsing(this, Solution(BooleanLiteral(false), Error(p.phi+" is UNSAT!").setType(tpe), 200), 200))
+ RuleSuccess(Solution(BooleanLiteral(false), Error(p.phi+" is UNSAT!").setType(tpe)))
case _ =>
- Nil
+ RuleInapplicable
}
} else {
- Nil
+ RuleInapplicable
}
}
}
class CaseSplit(synth: Synthesizer) extends Rule("Case-Split", synth) {
- def isApplicable(task: Task): List[DecomposedTask] = {
+ def applyOn(task: Task): RuleResult = {
val p = task.problem
p.phi match {
case Or(Seq(o1, o2)) =>
@@ -109,15 +114,15 @@ class CaseSplit(synth: Synthesizer) extends Rule("Case-Split", synth) {
case _ => Solution.none
}
- List(task.decompose(this, List(sub1, sub2), onSuccess, 100))
+ RuleDecomposed(List(sub1, sub2), onSuccess)
case _ =>
- Nil
+ RuleInapplicable
}
}
}
class Assert(synth: Synthesizer) extends Rule("Assert", synth) {
- def isApplicable(task: Task): List[DecomposedTask] = {
+ def applyOn(task: Task): RuleResult = {
val p = task.problem
p.phi match {
@@ -128,7 +133,7 @@ class Assert(synth: Synthesizer) extends Rule("Assert", synth) {
if (!exprsA.isEmpty) {
if (others.isEmpty) {
- List(task.solveUsing(this, Solution(And(exprsA), Tuple(p.xs.map(id => simplestValue(Variable(id))))), 150))
+ RuleSuccess(Solution(And(exprsA), Tuple(p.xs.map(id => simplestValue(Variable(id))))))
} else {
val onSuccess: List[Solution] => Solution = {
case List(s) => Solution(And(s.pre +: exprsA), s.term, 150)
@@ -137,34 +142,34 @@ class Assert(synth: Synthesizer) extends Rule("Assert", synth) {
val sub = p.copy(phi = And(others))
- List(task.decompose(this, List(sub), onSuccess, 150))
+ RuleDecomposed(List(sub), onSuccess)
}
} else {
- Nil
+ RuleInapplicable
}
case _ =>
- Nil
+ RuleInapplicable
}
}
}
class UnusedInput(synth: Synthesizer) extends Rule("UnusedInput", synth) {
- def isApplicable(task: Task): List[DecomposedTask] = {
+ def applyOn(task: Task): RuleResult = {
val p = task.problem
val unused = p.as.toSet -- variablesOf(p.phi)
if (!unused.isEmpty) {
val sub = p.copy(as = p.as.filterNot(unused))
- List(task.decompose(this, List(sub), forward, 300))
+ RuleDecomposed(List(sub), forward)
} else {
- Nil
+ RuleInapplicable
}
}
}
class UnconstrainedOutput(synth: Synthesizer) extends Rule("Unconstr.Output", synth) {
- def isApplicable(task: Task): List[DecomposedTask] = {
+ def applyOn(task: Task): RuleResult = {
val p = task.problem
val unconstr = p.xs.toSet -- variablesOf(p.phi)
@@ -178,10 +183,9 @@ class UnconstrainedOutput(synth: Synthesizer) extends Rule("Unconstr.Output", sy
Solution.none
}
- List(task.decompose(this, List(sub), onSuccess, 300))
-
+ RuleDecomposed(List(sub), onSuccess)
} else {
- Nil
+ RuleInapplicable
}
}
@@ -189,7 +193,7 @@ class UnconstrainedOutput(synth: Synthesizer) extends Rule("Unconstr.Output", sy
object Unification {
class DecompTrivialClash(synth: Synthesizer) extends Rule("Unif Dec./Clash/Triv.", synth) {
- def isApplicable(task: Task): List[DecomposedTask] = {
+ def applyOn(task: Task): RuleResult = {
val p = task.problem
val TopLevelAnds(exprs) = p.phi
@@ -209,15 +213,15 @@ object Unification {
val sub = p.copy(phi = And((exprs.toSet -- toRemove ++ toAdd.flatten).toSeq))
- List(task.decompose(this, List(sub), forward, 100))
+ RuleDecomposed(List(sub), forward)
} else {
- Nil
+ RuleInapplicable
}
}
}
class OccursCheck(synth: Synthesizer) extends Rule("Unif OccursCheck", synth) {
- def isApplicable(task: Task): List[DecomposedTask] = {
+ def applyOn(task: Task): RuleResult = {
val p = task.problem
val TopLevelAnds(exprs) = p.phi
@@ -234,9 +238,9 @@ object Unification {
if (isImpossible) {
val tpe = TupleType(p.xs.map(_.getType))
- List(task.solveUsing(this, Solution(BooleanLiteral(false), Error(p.phi+" is UNSAT!").setType(tpe), 200), 200))
+ RuleSuccess(Solution(BooleanLiteral(false), Error(p.phi+" is UNSAT!").setType(tpe)))
} else {
- Nil
+ RuleInapplicable
}
}
}
@@ -244,7 +248,7 @@ object Unification {
class ADTDual(synth: Synthesizer) extends Rule("ADTDual", synth) {
- def isApplicable(task: Task): List[DecomposedTask] = {
+ def applyOn(task: Task): RuleResult = {
val p = task.problem
val xs = p.xs.toSet
@@ -263,9 +267,9 @@ class ADTDual(synth: Synthesizer) extends Rule("ADTDual", synth) {
if (!toRemove.isEmpty) {
val sub = p.copy(phi = And((exprs.toSet -- toRemove ++ toAdd.flatten).toSeq))
- List(task.decompose(this, List(sub), forward, 80))
+ RuleDecomposed(List(sub), forward)
} else {
- Nil
+ RuleInapplicable
}
}
}
diff --git a/src/main/scala/leon/synthesis/Synthesizer.scala b/src/main/scala/leon/synthesis/Synthesizer.scala
index 295b6e143516deae9dbe3b2d85d262644facc1d2..b1c443494e44e849fa02b8375663014680f7fb19 100644
--- a/src/main/scala/leon/synthesis/Synthesizer.scala
+++ b/src/main/scala/leon/synthesis/Synthesizer.scala
@@ -28,6 +28,7 @@ class Synthesizer(val r: Reporter, val solvers: List[Solver], generateDerivation
workList += rootTask
solution = None
+
if (generateDerivationTrees) {
derivationTree = new DerivationTree(rootTask)
}
@@ -35,26 +36,11 @@ class Synthesizer(val r: Reporter, val solvers: List[Solver], generateDerivation
while (!workList.isEmpty && solution.isEmpty) {
val task = workList.dequeue()
- info("Now handling: "+task.problem)
-
- val alternatives = rules.flatMap(_.isApplicable(task))
-
- alternatives.find(_.isSuccess) match {
- case Some(ss) =>
- info(" => Rule "+ss.rule+" succeeded")
- ss.succeeded()
- case None =>
- info(" => Possible Next Steps:")
- alternatives.foreach(t => info(" - "+t.description))
- workList ++= alternatives.flatMap(_.subTasks)
- }
+ println("Running "+task+"...")
+ val subtasks = task.run
+ println(subtasks)
- // We are stuck
- if (alternatives.isEmpty) {
- val sol = Solution.choose(task.problem)
- warning(" => I give up: "+task.problem+" ⊢ "+sol)
- onTaskSucceeded(task, sol)
- }
+ workList ++= subtasks
}
@@ -68,15 +54,19 @@ class Synthesizer(val r: Reporter, val solvers: List[Solver], generateDerivation
def onTaskSucceeded(task: Task, solution: Solution) {
info(" => Solved "+task.problem+" ⊢ "+solution)
+
if (generateDerivationTrees) {
derivationTree.recordSolutionFor(task, solution)
}
- if (task.parent eq null) {
- info(" SUCCESS!")
- this.solution = Some(solution)
- } else {
- task.parent.subSucceeded(task.problem, solution)
+ task match {
+ case rt: RootTask =>
+ info(" SUCCESS!")
+ this.solution = Some(solution)
+ case d: ApplyRuleTask =>
+ d.parent.succeeded(solution)
+ case s: SimpleTask =>
+ s.parent.subSucceeded(task.problem, solution)
}
}
@@ -93,12 +83,13 @@ class Synthesizer(val r: Reporter, val solvers: List[Solver], generateDerivation
(None, Map())
}
+ val rules = Rules.all(this)
+
import purescala.Trees._
def synthesizeAll(program: Program): Map[Choose, Solution] = {
solvers.foreach(_.setProgram(program))
- val rules = Rules.all(this)
def noop(u:Expr, u2: Expr) = u
diff --git a/src/main/scala/leon/synthesis/Task.scala b/src/main/scala/leon/synthesis/Task.scala
index d73a7f58a93b47e7663bbd46b85ae698845c7450..d971b8ac00140abeed0ba8296f0b92db8474cdae 100644
--- a/src/main/scala/leon/synthesis/Task.scala
+++ b/src/main/scala/leon/synthesis/Task.scala
@@ -1,13 +1,14 @@
package leon
package synthesis
-class Task(val synth: Synthesizer,
- val parent: DecomposedTask,
+abstract class Task(val synth: Synthesizer,
+ val parent: Task,
val problem: Problem,
- val score: Score) extends Ordered[Task] {
+ val priority: Priority) extends Ordered[Task] {
- def compare(that: Task) = this.score - that.score
+ def compare(that: Task) = this.priority - that.priority
+ /*
def decompose(rule: Rule, subProblems: List[Problem], onSuccess: List[Solution] => Solution, score: Score): DecomposedTask = {
new DecomposedTask(this.synth, this.parent, this.problem, score, rule, subProblems, onSuccess)
}
@@ -15,31 +16,46 @@ class Task(val synth: Synthesizer,
def solveUsing(rule: Rule, onSuccess: => Solution, score: Score): DecomposedTask = {
new DecomposedTask(this.synth, this.parent, this.problem, 1000, rule, Nil, { case _ => onSuccess })
}
+ */
- override def toString = " Task("+score+"): " +problem
+ def run: List[Task]
+
+ override def toString = " Task("+priority+"): " +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) {
+class SimpleTask(synth: Synthesizer,
+ override val parent: ApplyRuleTask,
+ problem: Problem,
+ priority: Priority) extends Task(synth, parent, problem, priority) {
- def subTasks = subProblems.map(new Task(synth, this, _, score))
+ def succeeded(solution: Solution) {
+ synth.onTaskSucceeded(this, solution)
+ }
- var subSolutions = Map[Problem, Solution]()
+ def run: List[Task] = {
+ synth.rules.map(r => new ApplyRuleTask(synth, this, problem, priority, r))
+ }
- def isSuccess = subProblems.isEmpty
+ var failed = Set[Rule]()
+ def notifyInapplicable(r: Rule) = {
+ failed += r
+ if (failed.size == synth.rules.size) {
+ synth.onTaskSucceeded(this, Solution.choose(problem))
+ }
+ }
+}
- def succeeded() {
- assert(isSuccess)
+class RootTask(synth: Synthesizer, problem: Problem) extends SimpleTask(synth, null, problem, 0)
- val solution = onSuccess(Nil)
+class ApplyRuleTask(synth: Synthesizer,
+ override val parent: SimpleTask,
+ problem: Problem,
+ priority: Priority,
+ val rule: Rule) extends Task(synth, parent, problem, priority) {
- synth.onTaskSucceeded(this, solution)
- }
+ var subProblems: List[Problem] = _
+ var onSuccess: List[Solution] => Solution = _
+ var subSolutions : Map[Problem, Solution] = _
def subSucceeded(p: Problem, s: Solution) {
assert(subProblems contains p, "Problem "+p+" is unknown to me ?!?")
@@ -49,14 +65,30 @@ class DecomposedTask(synth: Synthesizer,
if (subSolutions.size == subProblems.size) {
- val solution = onSuccess(subProblems map subSolutions)
+ val solution = onSuccess(subProblems map subSolutions)
synth.onTaskSucceeded(this, solution)
}
}
}
- def description = "by "+rule.name+"("+score+"): "+problem +" ⟿ "+subProblems.mkString(" ; ")
-}
+ def run: List[Task] = {
+ rule.applyOn(this) match {
+ case RuleSuccess(solution) =>
+ // Solved
+ synth.onTaskSucceeded(this, solution)
+ Nil
+ case RuleDecomposed(subProblems, onSuccess) =>
+ this.subProblems = subProblems
+ this.onSuccess = onSuccess
+ this.subSolutions = Map()
+
+ subProblems.map(new SimpleTask(synth, this, _, 42))
+ case RuleInapplicable =>
+ parent.notifyInapplicable(rule)
+ Nil
+ }
+ }
-class RootTask(synth: Synthesizer, p: Problem) extends Task(synth, null, p, 0)
+ override def toString = "Trying "+rule+" on "+problem
+}
diff --git a/src/main/scala/leon/synthesis/package.scala b/src/main/scala/leon/synthesis/package.scala
index 30c04b2f5f3eaaabcde5f3765c7000597fccbd3e..fbef6f0ea621521aaec07596f274740c78dda956 100644
--- a/src/main/scala/leon/synthesis/package.scala
+++ b/src/main/scala/leon/synthesis/package.scala
@@ -2,4 +2,5 @@ package leon
package object synthesis {
type Score = Int
+ type Priority = Int
}