Rework things around to have a better idea how things work

src/main/scala/leon/synthesis/Main.scala

@@ -3,7 +3,7 @@ package synthesis
 
 object Main {
   def main(args : Array[String]) {
-    new Synthesizer().test()
+    new Synthesizer(new DefaultReporter).test()
   }
 
 }

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

@@ -5,8 +5,8 @@ import purescala.Common._
 import purescala.Trees._
 
 object Rules {
-  def all = List(
-    OnePoint
+  def all(synth: Synthesizer) = List(
+    OnePoint(synth)
   )
 }
 
@@ -18,7 +18,7 @@ abstract class Rule(val name: String) {
   def subst(what: Tuple2[Identifier, Expr], in: Expr): Expr = replace(Map(Variable(what._1) -> what._2), in)
 }
 
-object OnePoint extends Rule("One-point") {
+case class OnePoint(synth: Synthesizer) extends Rule("One-point") {
   def isApplicable(p: Problem, parent: Task): List[Task] = {
 
     p.phi match {
@@ -54,7 +54,7 @@ object OnePoint extends Rule("One-point") {
             case _ => Solution.none
           }
 
-          List(new Task(parent, p, List(newProblem), onSuccess, 100))
+          List(new Task(synth, parent, p, List(newProblem), onSuccess, 100))
         } else {
           Nil
         }

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

@@ -5,24 +5,20 @@ import purescala.Definitions.Program
 
 import collection.mutable.PriorityQueue
 
-class Synthesizer(rules: List[Rule]) {
-  def this() = this(Rules.all)
+class Synthesizer(val r: Reporter) {
+  import r.{error,warning,info,fatalError}
 
+  private[this] var solution: Solution = null
 
-  def applyRules(p: Problem, parent: Task): List[Task] = {
-    rules.flatMap(_.isApplicable(p, parent))
-  }
+  def synthesize(p: Problem, rules: List[Rule]): Solution = {
+
+    def applyRules(p: Problem, parent: Task): List[Task] = {
+      rules.flatMap(_.isApplicable(p, parent))
+    }
 
-  def synthesize(p: Problem): Solution = {
     val workList = new PriorityQueue[Task]()
 
-    var solution: Solution = null
-
-    val rootTask = new RootTask(p) {
-      override def notifyParent(s: Solution) {
-        solution = s
-      }
-    }
+    val rootTask = new RootTask(this, p)
 
     workList += rootTask
 
@@ -34,10 +30,13 @@ class Synthesizer(rules: List[Rule]) {
           throw new Exception("Such tasks shouldbe handled immediately")
         case subProblems =>
           for (sp <- subProblems) {
+            info("Now handling: "+sp)
+
             val alternatives = applyRules(sp, task)
 
             alternatives.find(_.isSuccess) match {
               case Some(ss) =>
+                info(" => Success!")
                 ss.succeeded()
               case None =>
                 workList ++= alternatives
@@ -46,20 +45,32 @@ class Synthesizer(rules: List[Rule]) {
             // We are stuck
             if (alternatives.isEmpty) {
               // I give up
-              task.subSucceeded(sp, Solution.choose(sp))
+              val sol = Solution.choose(sp)
+              warning(" => Solved (by choose): "+sp+" ⊢  "+sol)
+              task.subSucceeded(sp, sol)
+            } else {
+              info(" => Possible Next Steps:")
+              alternatives.foreach(a => info(" -   "+a))
             }
           }
       }
 
     }
 
-    println
-    println(" ++ RESULT ++ ")
-    println("==> "+p+" ⊢  "+solution)
-
     solution
   }
 
+  def onTaskSucceeded(task: Task, solution: Solution) {
+    info(" => Solved "+task.problem+" ⊢  "+solution)
+    task match {
+      case rt: RootTask =>
+        info(" SUCCESS!")
+        this.solution = solution
+      case t: Task =>
+        t.parent.subSucceeded(t.problem, solution)
+    }
+  }
+
   def test() {
     import purescala.Common._
     import purescala.Trees._
@@ -69,11 +80,7 @@ class Synthesizer(rules: List[Rule]) {
     val y = Variable(FreshIdentifier("y").setType(Int32Type))
     val p = Problem(Nil, And(List(GreaterThan(x, y), Equals(y, IntLiteral(2)), Equals(x, IntLiteral(3)))), List(x.id, y.id))
 
-    synthesize(p)
-  }
-
-  def synthesizeAll(p: Program): Program = {
-    p
+    synthesize(p, Rules.all(this))
   }
 }
 

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

@@ -2,6 +2,7 @@ package leon
 package synthesis
 
 class Task(
+        val synth: Synthesizer, 
         val parent: Task,
         val problem: Problem,
         val subProblems: List[Problem],
@@ -20,14 +21,12 @@ class Task(
 
     val solution = onSuccess(Nil)
 
-    println("Found solution: "+problem+" ⊢  "+solution)
-
-    notifyParent(solution)
+    synth.onTaskSucceeded(this, solution)
   }
 
   def subSucceeded(p: Problem, s: Solution) {
-    assert(subProblems contains p)
-    assert(!(subSolutions contains p))
+    assert(subProblems contains p, "Problem "+p+" is unknown to me ?!?")
+    assert(!(subSolutions contains p), "I already have a solution for "+p+" ?!?")
 
     subSolutions += p -> s
 
@@ -35,19 +34,11 @@ class Task(
 
       val solution = onSuccess(subProblems map subSolutions) 
 
-      println("Found solution: "+problem+" ⊢  "+solution)
-
-      notifyParent(solution)
+      synth.onTaskSucceeded(this, solution)
     }
   }
 
-  def notifyParent(solution: Solution) {
-    parent.subSucceeded(problem, solution)
-  }
+  override def toString = subProblems.map(p => (p, !subSolutions.get(p).isEmpty)).map{ case (p, isSolved) => p+(if(isSolved) "(OK)" else "(?)") }.mkString(" ; ") 
 }
 
-class RootTask(p: Problem) extends Task(null, p, List(p), xs => xs.head, 0) {
-  override def notifyParent(solution: Solution) {
-    sys.error("You need to override this!")
-  }
-}
+class RootTask(synth: Synthesizer, p: Problem) extends Task(synth, null, p, List(p), xs => xs.head, 0)