Simplify various things

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

@@ -62,7 +62,7 @@ class Synthesizer(val reporter: Reporter,
   }
 
   case class TaskRunRule(problem: Problem, rule: Rule, app: RuleApplication) extends AOAndTask[Solution] {
-    def cost = RuleApplicationCost(rule, app)
+    val cost = RuleApplicationCost(rule, app)
 
     def composeSolution(sols: List[Solution]): Solution = {
       app.onSuccess(sols)
@@ -72,7 +72,7 @@ class Synthesizer(val reporter: Reporter,
   }
 
   case class TaskTryRules(p: Problem) extends AOOrTask[Solution] {
-    def cost = ProblemCost(p)
+    val cost = ProblemCost(p)
 
     override def toString = p.toString
   }

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

@@ -35,8 +35,6 @@ class AndOrGraph[AT <: AOAndTask[S], OT <: AOOrTask[S], S <: AOSolution](val roo
 
   abstract class OrTree extends Tree {
     override val task: OT
-
-    def isUnsolvable: Boolean = false
   }
 
 
@@ -170,6 +168,7 @@ class AndOrGraph[AT <: AOAndTask[S], OT <: AOOrTask[S], S <: AOSolution](val roo
           minAlternative = sub
 
           notifyParent(solution.get)
+
         case None =>
           solution       = Some(sol)
           minAlternative = sub
@@ -183,8 +182,6 @@ class AndOrGraph[AT <: AOAndTask[S], OT <: AOOrTask[S], S <: AOSolution](val roo
         parent.notifySolution(this, sol)
       }
     }
-
-    override def isUnsolvable: Boolean = alternatives.isEmpty
   }
 
   class OrLeaf(val parent: AndNode, val task: OT) extends OrTree with Leaf {

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

@@ -86,7 +86,7 @@ package leon.synthesis.search
       case l: g.OrLeaf =>
         (if (t.isSolved) "palegreen" else "white" , "filled,dashed")
       case n: g.OrNode =>
-        (if (t.isSolved) "palegreen" else if (t.isUnsolvable) "indianred1" else "white", "filled")
+        (if (t.isSolved) "palegreen" else "white", "filled")
     }
 
     drawNode(res, name, ot.cost, ot.toString, color, style)

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

@@ -5,19 +5,34 @@ abstract class AndOrGraphSearch[AT <: AOAndTask[S],
                                 S <: AOSolution](val g: AndOrGraph[AT, OT, S]) {
 
   def nextLeaf: Option[g.Leaf] = {
-    var c: g.Tree = g.tree
+    import collection.mutable.PriorityQueue
+
+    case class WT(t: g.Tree, prefixCost: Cost) extends Ordered[WT] {
+      val cost = t.minCost + prefixCost
+
+      def compare(that: WT) = that.cost.compare(this.cost) // DESC
+    }
+
+    val q = new PriorityQueue[WT]()
+    q += WT(g.tree, Cost.zero)
+
     var res: Option[g.Leaf] = None
 
-    while(res.isEmpty) {
-      c match {
-        case l: g.Leaf =>
+    while(res.isEmpty && !q.isEmpty) {
+      q.dequeue() match {
+        case WT(l: g.Leaf, c) =>
           res = Some(l)
 
-        case an: g.AndNode =>
-          c = (an.subProblems -- an.subSolutions.keySet).values.minBy(_.minCost)
+        case WT(an: g.AndNode, c) =>
+          if (!an.isSolved) {
+            q ++= (an.subProblems -- an.subSolutions.keySet).values.map(n => WT(n, c + an.minCost))
+          }
+
+        case WT(on: g.OrNode, c) =>
+          if (!on.isSolved) {
+            q ++= on.alternatives.values.map(n => WT(n, c + on.minCost))
+          }
 
-        case on: g.OrNode =>
-          c = on.minAlternative
       }
     }
 
@@ -32,7 +47,7 @@ abstract class AndOrGraphSearch[AT <: AOAndTask[S],
   var continue = true
 
   def search(): Option[S] = {
-    while (!g.tree.isSolved && continue && !g.tree.isUnsolvable) {
+    while (!g.tree.isSolved && continue) {
       nextLeaf match {
         case Some(l) =>
           l match {
@@ -61,7 +76,6 @@ abstract class AndOrGraphSearch[AT <: AOAndTask[S],
           continue = false
       }
     }
-    
     g.tree.solution
   }