With --firstonly we stop as soon as possible, and stop propagating choose() down in the tree

src/main/scala/leon/synthesis/Heuristics.scala

@@ -10,7 +10,7 @@ import purescala.Definitions._
 
 object Heuristics {
   def all = Set[Synthesizer => Rule](
-    new IntInduction(_),
+    //new IntInduction(_),
     new OptimisticInjection(_),
     new ADTInduction(_)
   )

src/main/scala/leon/synthesis/Synthesizer.scala

@@ -51,13 +51,33 @@ class Synthesizer(val reporter: Reporter,
       }
     }
 
-    while (!workList.isEmpty && !(firstOnly && rootTask.solution.isDefined)) {
+    while (!workList.isEmpty) {
       val task = workList.dequeue()
 
-      val subProblems = task.run()
-
-      if (task.minComplexity <= bestSolutionSoFar.complexity) {
-        addProblems(task, subProblems)
+      val prefix = "[%-20s] ".format(Option(task.rule).map(_.toString).getOrElse("root"))
+
+      if (!(firstOnly && (task.parent ne null) && task.parent.isSolved)) {
+        val subProblems = task.run()
+
+        if (task.minComplexity <= bestSolutionSoFar.complexity) {
+          if (task.solution.isDefined || !subProblems.isEmpty) {
+            if (task.solution.isDefined) {
+              info(prefix+"Got: "+task.problem)
+              info(prefix+"Solved with: "+task.solution.get)
+            } else {
+              info(prefix+"Got: "+task.problem)
+              info(prefix+"Decomposed into:")
+              for(p <- subProblems) {
+                info(prefix+" - "+p)
+              }
+            }
+          }
+          addProblems(task, subProblems)
+        } else {
+          info(prefix+"Skip (worse): "+task.problem)
+        }
+      } else {
+        info(prefix+"Skip (done): "+task.problem)
       }
 
       if (timeoutExpired()) {

src/main/scala/leon/synthesis/Task.scala

@@ -24,6 +24,7 @@ class Task(synth: Synthesizer,
     }
   }
 
+
   var solution: Option[Solution] = None
   var minComplexity: AbsSolComplexity = new FixedSolComplexity(0)
 
@@ -39,6 +40,8 @@ class Task(synth: Synthesizer,
 
   def currentStep                 = steps.head
 
+  def isSolved: Boolean = parent.isSolved || (nextSteps.isEmpty && (currentStep.subSolutions.size == currentStep.subProblems.size))
+
   def partlySolvedBy(t: Task, s: Solution) {
     if (isBetterSolutionThan(s, currentStep.subSolutions.get(t.problem))) {
       currentStep.subSolutions += t.problem -> s
@@ -62,7 +65,7 @@ class Task(synth: Synthesizer,
               parent.partlySolvedBy(this, solution.get)
             case _ =>
               // solution is there, but it is incomplete (precondition not strongest)
-              parent.partlySolvedBy(this, Solution.choose(problem))
+              //parent.partlySolvedBy(this, Solution.choose(problem))
           }
         }
       }
@@ -75,7 +78,7 @@ class Task(synth: Synthesizer,
     if (currentStep.failures.size == synth.rules.size) {
       // We might want to report unsolved instead of solvedByChoose, depending
       // on the cases
-      parent.partlySolvedBy(this, Solution.choose(problem))
+      //parent.partlySolvedBy(this, Solution.choose(problem))
     }
   }
 
@@ -86,9 +89,6 @@ class Task(synth: Synthesizer,
         this.solution = Some(solution)
         parent.partlySolvedBy(this, solution)
 
-        val prefix = "[%-20s] ".format(Option(rule).map(_.toString).getOrElse("root"))
-        synth.reporter.info(prefix+"Got: "+problem)
-        synth.reporter.info(prefix+"Solved with: "+solution)
         Nil
 
       case RuleMultiSteps(subProblems, interSteps, onSuccess) =>
@@ -102,12 +102,6 @@ class Task(synth: Synthesizer,
         val simplestSubSolutions  = interSteps.foldLeft(subProblems.map(Solution.basic(_))){ (sols, step) => step(sols).map(Solution.basic(_)) }
         val simplestSolution = onSuccess(simplestSubSolutions)._1
         minComplexity = new FixedSolComplexity(parent.minComplexity.value + simplestSolution.complexity.value)
-        val prefix = "[%-20s] ".format(Option(rule).map(_.toString).getOrElse("root"))
-        synth.reporter.info(prefix+"Got: "+problem)
-        synth.reporter.info(prefix+"Decomposed into:")
-        for(p <- subProblems) {
-          synth.reporter.info(prefix+" - "+p)
-        }
 
         subProblems
 
@@ -127,6 +121,8 @@ class RootTask(synth: Synthesizer, problem: Problem) extends Task(synth, null, p
     List(problem)
   }
 
+  override def isSolved = solver.isDefined
+
   override def partlySolvedBy(t: Task, s: Solution) {
     if (isBetterSolutionThan(s, solution)) {
       solution = Some(s)