Fix derivation generations, genreate dot files

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

@@ -14,14 +14,19 @@ class Synthesizer(val r: Reporter, val solvers: List[Solver]) {
   import r.{error,warning,info,fatalError}
 
   private[this] var solution: Option[Solution] = None
+  private[this] var derivationTree: DerivationTree = _
+
+  var derivationCounter = 1;
 
   def synthesize(p: Problem, rules: List[Rule]): Solution = {
 
     val workList = new PriorityQueue[Task]()
     val rootTask = new RootTask(this, p)
 
+
     workList += rootTask
     solution = None
+    derivationTree = new DerivationTree(rootTask)
 
     while (!workList.isEmpty && solution.isEmpty) {
       val task = workList.dequeue()
@@ -48,9 +53,25 @@ class Synthesizer(val r: Reporter, val solvers: List[Solver]) {
       }
     }
 
+
+    derivationTree.toDotFile("derivation"+derivationCounter+".dot")
+    derivationCounter += 1
+
     solution.getOrElse(Solution.none)
   }
 
+  def onTaskSucceeded(task: Task, solution: Solution) {
+    info(" => Solved "+task.problem+" ⊢  "+solution)
+    derivationTree.recordSolutionFor(task, solution)
+
+    if (task.parent eq null) {
+      info(" SUCCESS!")
+      this.solution = Some(solution)
+    } else {
+      task.parent.subSucceeded(task.problem, solution)
+    }
+  }
+
   def solveSAT(phi: Expr): (Option[Boolean], Map[Identifier, Expr]) = {
     for (s <- solvers) {
       s.solveOrGetCounterexample(Not(phi)) match {
@@ -64,16 +85,6 @@ class Synthesizer(val r: Reporter, val solvers: List[Solver]) {
     (None, Map())
   }
 
-  def onTaskSucceeded(task: Task, solution: Solution) {
-    info(" => Solved "+task.problem+" ⊢  "+solution)
-    if (task.parent eq null) {
-      info(" SUCCESS!")
-      this.solution = Some(solution)
-    } else {
-      task.parent.subSucceeded(task.problem, solution)
-    }
-  }
-
   def synthesizeAll(program: Program) = {
     import purescala.Trees._
 

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

@@ -29,7 +29,7 @@ class DecomposedTask(synth: Synthesizer,
 
   def subTasks = subProblems.map(new Task(synth, this, _, score))
 
-  var subSolutions = Map[Problem, Solution]()
+  var subSolutions   = Map[Problem, Solution]()
 
   def isSuccess = subProblems.isEmpty
 

testcases/synthesis/Spt.scala

@@ -15,6 +15,8 @@ object SynthesisProceduresToolkit {
 
   def e6(a: Nat, b: Nat): (Nat, NatList) = choose( (x: Nat, y: NatList) => a == Succ(b))
 
+  def e7(a1 : NatList, a2 : Nat, a3 : NatList): (Nat, NatList, Nat, NatList) = choose( (x1 : Nat, x2 : NatList, x3 : Nat, x4 : NatList) => Cons(Succ(x1), x2) == a1 && Succ(x1) != a2 && a3 == Cons(x3, Cons(x3,  x4)) || (a1 == a3 && x1 == x3))
+
   abstract class Nat
   case class Z() extends Nat
   case class Succ(n: Nat) extends Nat