From 7d2512e7d2d7ab4cf1698938130ef7d7871f85bf Mon Sep 17 00:00:00 2001
From: Etienne Kneuss <ekneuss@gmail.com>
Date: Fri, 2 Nov 2012 19:50:59 +0100
Subject: [PATCH] Rework minComplexity of task based on real onSuccess
---
src/main/scala/leon/synthesis/Solution.scala | 4 +++-
src/main/scala/leon/synthesis/Synthesizer.scala | 6 +++---
src/main/scala/leon/synthesis/Task.scala | 10 +++++++---
3 files changed, 13 insertions(+), 7 deletions(-)
diff --git a/src/main/scala/leon/synthesis/Solution.scala b/src/main/scala/leon/synthesis/Solution.scala
index 573ff7c56..b948d3cf8 100644
--- a/src/main/scala/leon/synthesis/Solution.scala
+++ b/src/main/scala/leon/synthesis/Solution.scala
@@ -2,7 +2,7 @@ package leon
package synthesis
import leon.purescala.Trees._
-import leon.purescala.TreeOps.simplifyLets
+import leon.purescala.TreeOps._
// Defines a synthesis solution of the form:
// ⟨ P | T ⟩
@@ -26,6 +26,8 @@ object Solution {
def choose(p: Problem): Solution =
new Solution(BooleanLiteral(true), Choose(p.xs, p.phi))
+ def basic(p: Problem): Solution = new Solution(BooleanLiteral(true), Tuple(p.xs.map(id => simplestValue(id.getType))))
+
def none: Solution = throw new Exception("Unexpected failure to construct solution")
def simplify(e: Expr) = simplifyLets(e)
diff --git a/src/main/scala/leon/synthesis/Synthesizer.scala b/src/main/scala/leon/synthesis/Synthesizer.scala
index 936862fd4..90d444ee8 100644
--- a/src/main/scala/leon/synthesis/Synthesizer.scala
+++ b/src/main/scala/leon/synthesis/Synthesizer.scala
@@ -45,11 +45,11 @@ class Synthesizer(val r: Reporter,
while (!workList.isEmpty && !(firstOnly && rootTask.solution.isDefined)) {
val task = workList.dequeue()
+ val subProblems = task.run
+
// Check if solving this task has the slightest chance of improving the
// current solution
- if (task.minSolutionComplexity < bestSolutionSoFar().complexity) {
- val subProblems = task.run
-
+ if (task.minComplexity < bestSolutionSoFar().complexity) {
for (p <- subProblems; r <- rules) yield {
workList += new Task(this, task, p, r)
}
diff --git a/src/main/scala/leon/synthesis/Task.scala b/src/main/scala/leon/synthesis/Task.scala
index 4db32fd42..f931018a5 100644
--- a/src/main/scala/leon/synthesis/Task.scala
+++ b/src/main/scala/leon/synthesis/Task.scala
@@ -10,6 +10,7 @@ class Task(synth: Synthesizer,
val cproblem = -(this.problem.complexity compare that.problem.complexity) // problem DESC
if (cproblem == 0) {
+ // On equal complexity, order tasks by rule priority
this.rule.priority-that.rule.priority
} else {
cproblem
@@ -62,6 +63,10 @@ class Task(synth: Synthesizer,
case RuleDecomposed(subProblems, onSuccess) =>
this.subProblems = subProblems
this.onSuccess = onSuccess
+
+ val simplestSolution = onSuccess(subProblems.map(Solution.basic _))
+ minComplexity = new FixedSolutionComplexity(parent.minComplexity.value + simplestSolution.complexity.value)
+
subProblems
case RuleInapplicable =>
@@ -70,7 +75,7 @@ class Task(synth: Synthesizer,
}
}
- lazy val minSolutionComplexity: FixedSolutionComplexity = new FixedSolutionComplexity(rule.cost+parent.minSolutionComplexity.value)
+ var minComplexity: SolutionComplexity = new FixedSolutionComplexity(0)
override def toString = "Applying "+rule+" on "+problem
}
@@ -78,8 +83,6 @@ class Task(synth: Synthesizer,
class RootTask(synth: Synthesizer, problem: Problem) extends Task(synth, null, problem, null) {
var solver: Option[Task] = None
- override lazy val minSolutionComplexity = new FixedSolutionComplexity(0)
-
override def partlySolvedBy(t: Task, s: Solution) {
if (isBetterSolutionThan(s, solution)) {
solution = Some(s)
@@ -101,4 +104,5 @@ class RootTask(synth: Synthesizer, problem: Problem) extends Task(synth, null, p
override def run: List[Problem] = {
List(problem)
}
+
}
--
GitLab