Ands get decomposed into sub-ands

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

@@ -22,7 +22,13 @@ object OnePoint extends Rule("One-point") {
   def isApplicable(p: Problem, parent: Task): List[Task] = {
 
     p.phi match {
-      case And(exprs) =>
+      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)
         val candidates = exprs.collect {
           case eq @ Equals(Variable(x), e) if (p.xs contains x) && !(variablesOf(e) contains x) =>
             (x, e, eq)

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

@@ -67,7 +67,7 @@ class Synthesizer(rules: List[Rule]) {
 
     val x = Variable(FreshIdentifier("x").setType(Int32Type))
     val y = Variable(FreshIdentifier("y").setType(Int32Type))
-    val p = Problem(Nil, And(GreaterThan(x, y), Equals(x, IntLiteral(3))), List(x.id, y.id))
+    val p = Problem(Nil, And(List(GreaterThan(x, y), Equals(y, IntLiteral(2)), Equals(x, IntLiteral(3)))), List(x.id, y.id))
 
     synthesize(p)
   }

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

@@ -17,7 +17,12 @@ class Task(
 
   def succeeded() {
     assert(isSuccess)
-    notifyParent(onSuccess(Nil))
+
+    val solution = onSuccess(Nil)
+
+    println("Found solution: "+problem+" ⊢  "+solution)
+
+    notifyParent(solution)
   }
 
   def subSucceeded(p: Problem, s: Solution) {
@@ -30,7 +35,7 @@ class Task(
 
       val solution = onSuccess(subProblems map subSolutions) 
 
-      println("Found solution to: "+problem+" ⊢  "+solution)
+      println("Found solution: "+problem+" ⊢  "+solution)
 
       notifyParent(solution)
     }
@@ -43,6 +48,6 @@ class Task(
 
 class RootTask(p: Problem) extends Task(null, p, List(p), xs => xs.head, 0) {
   override def notifyParent(solution: Solution) {
-    sys.error("You need to extend this!")
+    sys.error("You need to override this!")
   }
 }