Rework minComplexity of task based on real onSuccess

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)

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)
         }

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)
   }
+
 }