From 921978f792b5d288988d95950d18702149775a09 Mon Sep 17 00:00:00 2001
From: Etienne Kneuss <ekneuss@gmail.com>
Date: Tue, 23 Oct 2012 15:18:43 +0200
Subject: [PATCH] Simplify task decomposition by going via task methods
---
src/main/scala/leon/synthesis/Rules.scala | 27 ++++++-----------------
src/main/scala/leon/synthesis/Task.scala | 8 +++++++
2 files changed, 15 insertions(+), 20 deletions(-)
diff --git a/src/main/scala/leon/synthesis/Rules.scala b/src/main/scala/leon/synthesis/Rules.scala
index c1b392774..fa641566b 100644
--- a/src/main/scala/leon/synthesis/Rules.scala
+++ b/src/main/scala/leon/synthesis/Rules.scala
@@ -56,7 +56,7 @@ class OnePoint(synth: Synthesizer) extends Rule("One-point", synth) {
case _ => Solution.none
}
- List(new DecomposedTask(synth, task.parent, p, 100, this, List(newProblem), onSuccess))
+ List(task.decompose(this, List(newProblem), onSuccess, 100))
} else {
Nil
}
@@ -78,17 +78,9 @@ class Ground(synth: Synthesizer) extends Rule("Ground", synth) {
synth.solveSAT(p.phi) match {
case (Some(true), model) =>
- val onSuccess: List[Solution] => Solution = {
- case Nil => Solution(BooleanLiteral(true), Tuple(p.xs.map(model)).setType(tpe), 200)
- }
-
- List(new DecomposedTask(synth, task.parent, p, 200, this, Nil, onSuccess))
+ List(task.solveUsing(this, Solution(BooleanLiteral(true), Tuple(p.xs.map(model)).setType(tpe), 200), 200))
case (Some(false), model) =>
- val onSuccess: List[Solution] => Solution = {
- case Nil => Solution(BooleanLiteral(false), Error(p.phi+" is UNSAT!").setType(tpe), 200)
- }
-
- List(new DecomposedTask(synth, task.parent, p, 200, this, Nil, onSuccess))
+ List(task.solveUsing(this, Solution(BooleanLiteral(false), Error(p.phi+" is UNSAT!").setType(tpe), 200), 200))
case _ =>
Nil
}
@@ -111,7 +103,7 @@ class CaseSplit(synth: Synthesizer) extends Rule("Case-Split", synth) {
case _ => Solution.none
}
- List(new DecomposedTask(synth, task.parent, p, 100, this, List(sub1, sub2), onSuccess))
+ List(task.decompose(this, List(sub1, sub2), onSuccess, 100))
case _ =>
Nil
}
@@ -130,12 +122,7 @@ class Assert(synth: Synthesizer) extends Rule("Assert", synth) {
if (!exprsA.isEmpty) {
if (others.isEmpty) {
- val onSuccess: List[Solution] => Solution = {
- case Nil => Solution(And(exprsA), BooleanLiteral(true), 150)
- case _ => Solution.none
- }
-
- List(new DecomposedTask(synth, task.parent, p, 150, this, Nil, onSuccess))
+ List(task.solveUsing(this, Solution(And(exprsA), BooleanLiteral(true), 150), 150))
} else {
val onSuccess: List[Solution] => Solution = {
case List(s) => Solution(And(s.pre +: exprsA), s.term, 150)
@@ -144,7 +131,7 @@ class Assert(synth: Synthesizer) extends Rule("Assert", synth) {
val sub = p.copy(phi = And(others))
- List(new DecomposedTask(synth, task.parent, p, 150, this, List(sub), onSuccess))
+ List(task.decompose(this, List(sub), onSuccess, 150))
}
} else {
Nil
@@ -168,7 +155,7 @@ class UnusedInput(synth: Synthesizer) extends Rule("UnusedInput", synth) {
case _ => Solution.none
}
- List(new DecomposedTask(synth, task.parent, p, 300, this, List(sub), onSuccess))
+ List(task.decompose(this, List(sub), onSuccess, 300))
} else {
Nil
}
diff --git a/src/main/scala/leon/synthesis/Task.scala b/src/main/scala/leon/synthesis/Task.scala
index 53e09bc98..73858e295 100644
--- a/src/main/scala/leon/synthesis/Task.scala
+++ b/src/main/scala/leon/synthesis/Task.scala
@@ -8,6 +8,14 @@ class Task(val synth: Synthesizer,
def compare(that: Task) = this.score - that.score
+ 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)
+ }
+
+ 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
}
--
GitLab