Plop

src/main/scala/leon/purescala/Trees.scala

@@ -179,6 +179,15 @@ object Trees {
     val fixedType = BooleanType
   }
 
+  object TopLevelAnds { // expr1 AND (expr2 AND (expr3 AND ..)) => List(expr1, expr2, expr3)
+    def unapply(e: Expr): Option[Seq[Expr]] = e match {
+      case And(exprs) =>
+        Some(exprs.flatMap(unapply(_).flatten))
+      case e =>
+        Some(Seq(e))
+    }
+  }
+
   object Or {
     def apply(l: Expr, r: Expr) : Expr = (l,r) match {
       case (BooleanLiteral(false),_) => r

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

@@ -3,7 +3,10 @@ package synthesis
 
 object Main {
   def main(args : Array[String]) {
-    new Synthesizer(new DefaultReporter).test()
+    val reporter = new DefaultReporter
+    val solvers  = List(new TrivialSolver(reporter))
+
+    new Synthesizer(reporter, solvers).test()
   }
 
 }

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

@@ -6,29 +6,25 @@ import purescala.Trees._
 
 object Rules {
   def all(synth: Synthesizer) = List(
-    OnePoint(synth)
+    new OnePoint(synth),
+    new Ground(synth)
   )
 }
 
 
-abstract class Rule(val name: String) {
+abstract class Rule(val name: String, val synth: Synthesizer) {
   def isApplicable(p: Problem, parent: Task): List[Task]
 
-
   def subst(what: Tuple2[Identifier, Expr], in: Expr): Expr = replace(Map(Variable(what._1) -> what._2), in)
+
+  override def toString = name
 }
 
-case class OnePoint(synth: Synthesizer) extends Rule("One-point") {
+class OnePoint(synth: Synthesizer) extends Rule("One-point", synth) {
   def isApplicable(p: Problem, parent: Task): List[Task] = {
 
     p.phi match {
-      case a : And =>
-        def collectAnds(e: Expr): List[Expr] = e match {
-          case And(exs) => exs.toList.flatMap(collectAnds)
-          case e => List(e)
-        }
-
-        val exprs = collectAnds(a)
+      case TopLevelAnds(exprs) =>
         val candidates = exprs.collect {
           case eq @ Equals(Variable(x), e) if (p.xs contains x) && !(variablesOf(e) contains x) =>
             (x, e, eq)
@@ -54,7 +50,7 @@ case class OnePoint(synth: Synthesizer) extends Rule("One-point") {
             case _ => Solution.none
           }
 
-          List(new Task(synth, parent, p, List(newProblem), onSuccess, 100))
+          List(new Task(synth, parent, this, p, List(newProblem), onSuccess, 100))
         } else {
           Nil
         }
@@ -65,3 +61,9 @@ case class OnePoint(synth: Synthesizer) extends Rule("One-point") {
     }
   }
 }
+
+class Ground(synth: Synthesizer) extends Rule("Ground", synth) {
+  def isApplicable(p: Problem, parent: Task): List[Task] = {
+    Nil
+  }
+}

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

@@ -2,10 +2,11 @@ package leon
 package synthesis
 
 import purescala.Definitions.Program
+import Extensions.Solver
 
 import collection.mutable.PriorityQueue
 
-class Synthesizer(val r: Reporter) {
+class Synthesizer(val r: Reporter, val solvers: List[Solver]) {
   import r.{error,warning,info,fatalError}
 
   private[this] var solution: Solution = null
@@ -50,7 +51,7 @@ class Synthesizer(val r: Reporter) {
               task.subSucceeded(sp, sol)
             } else {
               info(" => Possible Next Steps:")
-              alternatives.foreach(a => info(" -   "+a))
+              alternatives.foreach(t => info(" -   "+t.description))
             }
           }
       }

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

@@ -4,6 +4,7 @@ package synthesis
 class Task(
         val synth: Synthesizer, 
         val parent: Task,
+        val rule: Rule,
         val problem: Problem,
         val subProblems: List[Problem],
         val onSuccess: List[Solution] => Solution,
@@ -38,7 +39,9 @@ class Task(
     }
   }
 
-  override def toString = subProblems.map(p => (p, !subSolutions.get(p).isEmpty)).map{ case (p, isSolved) => p+(if(isSolved) "(OK)" else "(?)") }.mkString(" ; ") 
+  override def toString = description 
+
+  def description = "by "+rule.name+"("+score+"): "+problem +" ⟿    "+subProblems.mkString(" ; ")
 }
 
-class RootTask(synth: Synthesizer, p: Problem) extends Task(synth, null, p, List(p), xs => xs.head, 0)
+class RootTask(synth: Synthesizer, p: Problem) extends Task(synth, null, null, p, List(p), xs => xs.head, 0)