Integrate with Leon some more

src/main/scala/leon/synthesis/Rules.scala

@@ -68,7 +68,7 @@ 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), replaceFromIDs(model, p.phi))
+            case Nil => Solution(BooleanLiteral(true), Tuple(p.xs.map(model)))
           }
 
           List(new Task(synth, parent, this, p, Nil, onSuccess, 200))

src/main/scala/leon/synthesis/SynthesisPhase.scala

@@ -8,9 +8,10 @@ class SynthesisPhase(reporter: Reporter) extends plugin.TransformationPhase {
   val description = "Synthesis"
 
   def apply(program: Program): Program = {
+    val quietReporter = new QuietReporter
     val solvers  = List(
-      new TrivialSolver(reporter),
-      new FairZ3Solver(reporter)
+      new TrivialSolver(quietReporter),
+      new FairZ3Solver(quietReporter)
     )
 
     new Synthesizer(reporter, solvers).synthesizeAll(program)

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

@@ -43,6 +43,8 @@ class Synthesizer(val r: Reporter, val solvers: List[Solver]) {
                 info(" => Success!")
                 ss.succeeded()
               case None =>
+                info(" => Possible Next Steps:")
+                alternatives.foreach(t => info(" -   "+t.description))
                 workList ++= alternatives
             }
 
@@ -52,9 +54,6 @@ class Synthesizer(val r: Reporter, val solvers: List[Solver]) {
               val sol = Solution.choose(sp)
               warning(" => Solved (by choose): "+sp+" ⊢  "+sol)
               task.subSucceeded(sp, sol)
-            } else {
-              info(" => Possible Next Steps:")
-              alternatives.foreach(t => info(" -   "+t.description))
             }
           }
       }
@@ -78,12 +77,12 @@ class Synthesizer(val r: Reporter, val solvers: List[Solver]) {
   }
 
   def onTaskSucceeded(task: Task, solution: Solution) {
-    info(" => Solved "+task.problem+" ⊢  "+solution)
     task match {
       case rt: RootTask =>
         info(" SUCCESS!")
         this.solution = solution
       case t: Task =>
+        info(" => Solved "+task.problem+" ⊢  "+solution)
         t.parent.subSucceeded(t.problem, solution)
     }
   }
@@ -101,7 +100,33 @@ class Synthesizer(val r: Reporter, val solvers: List[Solver]) {
   }
 
   def synthesizeAll(program: Program) = {
+    import purescala.Trees._
+
     solvers.foreach(_.setProgram(program))
+
+    val rules = Rules.all(this)
+
+    def noop(u:Expr, u2: Expr) = u
+
+    def actOnChoose(e: Expr, a: Expr): Expr = e match {
+      case Choose(vars, pred) =>
+        val xs = vars
+        val as = (variablesOf(pred)--xs).toList
+        val phi = pred
+
+        synthesize(Problem(as, phi, xs), rules)
+
+        a
+      case _ =>
+        a
+    }
+
+    // Look for choose()
+    for (f <- program.definedFunctions if f.body.isDefined) {
+      println(f)
+      treeCatamorphism(x => x, noop, actOnChoose, f.body.get)
+    }
+
     program
   }
 }

testcases/Choose.scala

@@ -2,10 +2,12 @@ import leon.Utils._
 
 object ChooseTest {
 
-  def c1(x: Int): Int = choose{ (a1: Int) => a1 > x }
-  def c2(x: Int): (Int, Int) = choose{ (a1: Int, a2: Int) => a1 > x && a2 > x }
-  def c3(x: Int): (Int, Int, Int) = choose{ (a1: Int, a2: Int, a3: Int) => a1 > x && a2 > x }
-  def c4(x: Int): (Int, Int, Int, Int) = choose{ (a1: Int, a2: Int, a3: Int, a4: Int) => a1 > x && a2 > x }
-  def c5(x: Int): (Int, Int, Int, Int, Int) = choose{ (a1: Int, a2: Int, a3: Int, a4: Int, a5: Int) => a1 > x && a2 > x }
+  def c0(): Int = choose{ (x1: Int) => x1 > 13 }
+
+  def c1(a: Int): Int = choose{ (x1: Int) => x1 > a }
+  def c2(a: Int): (Int, Int) = choose{ (x1: Int, x2: Int) => x1 > a && x2 > a }
+  def c3(a: Int): (Int, Int, Int) = choose{ (x1: Int, x2: Int, x3: Int) => x1 > a && x2 > a }
+  def c4(a: Int): (Int, Int, Int, Int) = choose{ (x1: Int, x2: Int, x3: Int, x4: Int) => x1 > a && x2 > a }
+  def c5(a: Int): (Int, Int, Int, Int, Int) = choose{ (x1: Int, x2: Int, x3: Int, x4: Int, x5: Int) => x1 > a && x2 > a }
 
 }