Simplify cost model, fix various issues

src/main/scala/leon/synthesis/Cost.scala

@@ -16,12 +16,12 @@ case class SolutionCost(s: Solution) extends Cost {
 }
 
 case class ProblemCost(p: Problem) extends Cost {
-  val value = math.pow(2, p.xs.size).toInt + formulaSize(p.phi)*1000
+  val value = math.pow(2, p.xs.size).toInt + formulaSize(p.phi)
 }
 
 case class RuleApplicationCost(rule: Rule, app: RuleApplication) extends Cost {
   val subSols = (1 to app.subProblemsCount).map {i => Solution.simplest }.toList
   val simpleSol = app.onSuccess(subSols)
 
-  val value = SolutionCost(simpleSol).value*1000 + 1000-rule.priority
+  val value = SolutionCost(simpleSol).value
 }

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

@@ -54,15 +54,9 @@ class Synthesizer(val reporter: Reporter,
     val diff = System.currentTimeMillis()-ts
     reporter.info("Finished in "+diff+"ms")
 
-    /*
     if (generateDerivationTrees) {
-      val deriv = new DerivationTree(rootTask)
-      deriv.toDotFile("derivation"+derivationCounter+".dot")
-      derivationCounter += 1
+      new AndOrGraphDotConverter(search.g).writeFile("derivation.dot")
     }
-    */
-
-    new AndOrGraphDotConverter(search.g).writeFile("test.dot")
 
     res.getOrElse(Solution.choose(problem))
   }

src/main/scala/leon/synthesis/search/AndOrGraph.scala

@@ -16,15 +16,13 @@ trait AOSolution {
 }
 
 class AndOrGraph[AT <: AOAndTask[S], OT <: AOOrTask[S], S <: AOSolution](val root: OT) {
-  type C = Cost
-
   var tree: OrTree = RootNode
 
   trait Tree {
     val task : AOTask[S]
     val parent: Node[_]
 
-    def minCost: C
+    def minCost: Cost
 
     var solution: Option[S] = None
 
@@ -43,7 +41,7 @@ class AndOrGraph[AT <: AOAndTask[S], OT <: AOOrTask[S], S <: AOSolution](val roo
 
 
   trait Leaf extends Tree {
-    def minCost: C = task.cost
+    def minCost = task.cost
   }
 
   trait Node[T <: Tree] extends Tree {
@@ -56,8 +54,11 @@ class AndOrGraph[AT <: AOAndTask[S], OT <: AOOrTask[S], S <: AOSolution](val roo
     var subProblems         = Map[OT, OrTree]()
     var subSolutions        = Map[OT, S]()
 
-    def computeCost = {
-      solution match {
+    var minCost = Cost.zero
+
+    def updateMin() {
+      val old = minCost
+      minCost = solution match {
         case Some(s) =>
           s.cost
         case _ =>
@@ -65,9 +66,11 @@ class AndOrGraph[AT <: AOAndTask[S], OT <: AOOrTask[S], S <: AOSolution](val roo
 
           subCosts.foldLeft(task.cost)(_ + _)
       }
+      if (minCost != old) {
+        Option(parent).foreach(_.updateMin())
+      }
     }
 
-    var minCost = computeCost
 
     def unsolvable(l: OrTree) {
       parent.unsolvable(this)
@@ -76,7 +79,7 @@ class AndOrGraph[AT <: AOAndTask[S], OT <: AOOrTask[S], S <: AOSolution](val roo
     def expandLeaf(l: OrLeaf, succ: List[AT]) {
       val n = new OrNode(this, Map(), l.task)
       n.alternatives = succ.map(t => t -> new AndLeaf(n, t)).toMap
-      n.minAlternative = n.computeMin
+      n.updateMin()
 
       subProblems += l.task -> n
     }
@@ -86,19 +89,17 @@ class AndOrGraph[AT <: AOAndTask[S], OT <: AOOrTask[S], S <: AOSolution](val roo
 
       if (subSolutions.size == subProblems.size) {
         solution = Some(task.composeSolution(subTasks.map(subSolutions)))
-        minCost = computeCost
+        updateMin()
 
         notifyParent(solution.get)
       } else {
-        minCost = computeCost
+        updateMin()
       }
 
     }
 
     def notifyParent(sol: S) {
-      if (parent ne null) {
-        parent.notifySolution(this, sol)
-      }
+      Option(parent).foreach(_.notifySolution(this, sol))
     }
   }
 
@@ -107,7 +108,7 @@ class AndOrGraph[AT <: AOAndTask[S], OT <: AOOrTask[S], S <: AOSolution](val roo
     override def expandWith(succ: List[AT]) {
       val n = new OrNode(null, Map(), root)
       n.alternatives = succ.map(t => t -> new AndLeaf(n, t)).toMap
-      n.minAlternative = n.computeMin
+      n.updateMin()
 
       tree = n
     }
@@ -122,14 +123,20 @@ class AndOrGraph[AT <: AOAndTask[S], OT <: AOOrTask[S], S <: AOSolution](val roo
 
 
   class OrNode(val parent: AndNode, var alternatives: Map[AT, AndTree], val task: OT) extends OrTree with Node[AndTree] {
-    var minAlternative: Tree    = _
-    def minCost: C              = minAlternative.minCost
+    var minAlternative: Tree = _
+    var minCost              = Cost.zero
 
-    def computeMin = {
+    def updateMin() {
       if (!alternatives.isEmpty) {
-        alternatives.values.minBy(_.minCost)
+        minAlternative = alternatives.values.minBy(_.minCost)
+        val old = minCost 
+        minCost        = minAlternative.minCost
+        if (minCost != old) {
+          Option(parent).foreach(_.updateMin())
+        }
       } else {
-        null
+        minAlternative = null
+        minCost        = Cost.zero
       }
     }
 
@@ -139,18 +146,18 @@ class AndOrGraph[AT <: AOAndTask[S], OT <: AOOrTask[S], S <: AOSolution](val roo
       if (alternatives.isEmpty) {
         parent.unsolvable(this)
       } else {
-        minAlternative = computeMin
+        updateMin()
       }
     }
 
     def expandLeaf(l: AndLeaf, succ: List[OT]) {
       val n = new AndNode(this, succ, l.task)
       n.subProblems = succ.map(t => t -> new OrLeaf(n, t)).toMap
-      n.minCost     = n.computeCost
+      n.updateMin()
 
       alternatives += l.task -> n
 
-      minAlternative = computeMin
+      updateMin()
     }
 
     def notifySolution(sub: AndTree, sol: S) {

src/main/scala/leon/synthesis/search/AndOrGraphSearch.scala

@@ -41,6 +41,7 @@ abstract class AndOrGraphSearch[AT <: AOAndTask[S],
                 case Expanded(ls) =>
                   al.expandWith(ls)
                 case r @ ExpandSuccess(sol) =>
+                  al.solution = Some(sol)
                   al.parent.notifySolution(al, sol)
                 case _ =>
                   al.parent.unsolvable(al)
@@ -50,6 +51,7 @@ abstract class AndOrGraphSearch[AT <: AOAndTask[S],
                 case Expanded(ls) =>
                   ol.expandWith(ls)
                 case r @ ExpandSuccess(sol) =>
+                  ol.solution = Some(sol)
                   ol.parent.notifySolution(ol, sol)
                 case _ =>
                   ol.parent.unsolvable(ol)

src/main/scala/leon/synthesis/search/Cost.scala

@@ -11,6 +11,6 @@ trait Cost extends Ordered[Cost] {
 case class CostFixed(value: Int) extends Cost
 
 object Cost {
-  val zero = new CostFixed(0)
+  val zero: Cost = new CostFixed(0)
 }