From 578139b4869892a0bd287263dd355b7b1ac4161e Mon Sep 17 00:00:00 2001
From: Etienne Kneuss <ekneuss@gmail.com>
Date: Mon, 12 Nov 2012 02:50:00 +0100
Subject: [PATCH] Filter based on best solution so far (reimplemented with new
 multi-steps rules)

---
 src/main/scala/leon/synthesis/Synthesizer.scala |  6 +++++-
 src/main/scala/leon/synthesis/Task.scala        | 17 +++++++++++++----
 2 files changed, 18 insertions(+), 5 deletions(-)

diff --git a/src/main/scala/leon/synthesis/Synthesizer.scala b/src/main/scala/leon/synthesis/Synthesizer.scala
index cb945337d..ba8ec79c4 100644
--- a/src/main/scala/leon/synthesis/Synthesizer.scala
+++ b/src/main/scala/leon/synthesis/Synthesizer.scala
@@ -52,7 +52,11 @@ class Synthesizer(val reporter: Reporter,
     while (!workList.isEmpty && !(firstOnly && rootTask.solution.isDefined)) {
       val task = workList.dequeue()
 
-      task.run()
+      val subProblems = task.run()
+
+      if (task.minComplexity <= bestSolutionSoFar.complexity) {
+        addProblems(task, subProblems)
+      }
 
       if (timeoutExpired()) {
         warning("Timeout reached")
diff --git a/src/main/scala/leon/synthesis/Task.scala b/src/main/scala/leon/synthesis/Task.scala
index a1632ec33..ed3bd980d 100644
--- a/src/main/scala/leon/synthesis/Task.scala
+++ b/src/main/scala/leon/synthesis/Task.scala
@@ -25,6 +25,7 @@ class Task(synth: Synthesizer,
   }
 
   var solution: Option[Solution] = None
+  var minComplexity: AbsSolComplexity = new FixedSolComplexity(0)
 
   class TaskStep(val subProblems: List[Problem]) {
     var subSolutions = Map[Problem, Solution]()
@@ -71,7 +72,7 @@ class Task(synth: Synthesizer,
     }
   }
 
-  def run() {
+  def run(): List[Problem] = {
     rule.applyOn(this) match {
       case RuleSuccess(solution) =>
         // Solved
@@ -81,12 +82,19 @@ class Task(synth: Synthesizer,
         val prefix = "[%-20s] ".format(Option(rule).map(_.toString).getOrElse("root"))
         println(prefix+"Got: "+problem)
         println(prefix+"Solved with: "+solution)
+        Nil
 
       case RuleMultiSteps(subProblems, interSteps, onSuccess) =>
         this.steps = new TaskStep(subProblems) :: Nil
         this.nextSteps = interSteps
         this.onSuccess = onSuccess
 
+        // Compute simplest solution possible to evaluate whether this rule is worth it
+        // To each problem we assign the most basic solution, fold on all inner
+        // steps, and then reconstruct final solution
+        val simplestSubSolutions  = interSteps.foldLeft(subProblems.map(Solution.basic(_))){ (sols, step) => step(sols).map(Solution.basic(_)) }
+        val simplestSolution = onSuccess(simplestSubSolutions)
+        minComplexity = new FixedSolComplexity(parent.minComplexity.value + simplestSolution.complexity.value)
         val prefix = "[%-20s] ".format(Option(rule).map(_.toString).getOrElse("root"))
         println(prefix+"Got: "+problem)
         println(prefix+"Decomposed into:")
@@ -94,10 +102,11 @@ class Task(synth: Synthesizer,
           println(prefix+" - "+p)
         }
 
-        synth.addProblems(this, subProblems)
+        subProblems
 
       case RuleInapplicable =>
         parent.unsolvedBy(this)
+        Nil
     }
   }
 
@@ -107,8 +116,8 @@ class Task(synth: Synthesizer,
 class RootTask(synth: Synthesizer, problem: Problem) extends Task(synth, null, problem, null) {
   var solver: Option[Task] = None
 
-  override def run() {
-    synth.addProblems(this, List(problem))
+  override def run() = {
+    List(problem)
   }
 
   override def partlySolvedBy(t: Task, s: Solution) {
-- 
GitLab