Improve search by making it more deterministic

src/main/scala/leon/synthesis/SimpleSearch.scala

@@ -42,14 +42,13 @@ class SimpleSearch(synth: Synthesizer,
   def expandAndTask(t: TaskRunRule): ExpandResult[TaskTryRules] = {
     val prefix = "[%-20s] ".format(Option(t.rule).getOrElse("?"))
 
+    info(prefix+"Got: "+t.problem)
     t.app.apply(sctx) match {
       case RuleSuccess(sol) =>
-        info(prefix+"Got: "+t.problem)
         info(prefix+"Solved with: "+sol)
 
         ExpandSuccess(sol)
       case RuleDecomposed(sub) =>
-        info(prefix+"Got: "+t.problem)
         info(prefix+"Decomposed into:")
         for(p <- sub) {
           info(prefix+" - "+p)
@@ -58,6 +57,8 @@ class SimpleSearch(synth: Synthesizer,
         Expanded(sub.map(TaskTryRules(_)))
 
       case RuleApplicationImpossible =>
+        info(prefix+"Failed")
+
         ExpandFailure()
     }
   }

src/main/scala/leon/synthesis/heuristics/ADTInduction.scala

@@ -40,7 +40,7 @@ case object ADTInduction extends Rule("ADT Induction") with Heuristic {
         val innerPhi = substAll(residualMap + (origId -> Variable(inductOn)), p.phi)
         val innerPC  = substAll(residualMap + (origId -> Variable(inductOn)), p.pc)
 
-        val subProblemsInfo = for (dcd <- cd.knownDescendents) yield dcd match {
+        val subProblemsInfo = for (dcd <- cd.knownDescendents.sortBy(_.id.name)) yield dcd match {
           case ccd : CaseClassDef =>
             var recCalls = Map[List[Identifier], List[Expr]]()
             var postFs   = List[Expr]()

src/main/scala/leon/synthesis/rules/ADTSplit.scala

@@ -14,7 +14,7 @@ case object ADTSplit extends Rule("ADT Split.") {
     val candidates = p.as.collect {
       case IsTyped(id, AbstractClassType(cd)) =>
 
-        val optCases = for (dcd <- cd.knownDescendents) yield dcd match {
+        val optCases = for (dcd <- cd.knownDescendents.sortBy(_.id.name)) yield dcd match {
           case ccd : CaseClassDef =>
             val toSat = And(p.pc, Not(CaseClassInstanceOf(ccd, Variable(id))))
 

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

@@ -77,11 +77,7 @@ class AndOrGraph[AT <: AOAndTask[S], OT <: AOOrTask[S], S](val root: OT, val cos
     }
 
     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.updateMin()
-
-      subProblems += l.task -> n
+      subProblems += l.task -> new OrNode(this, succ, l.task)
     }
 
     def notifySolution(sub: OrTree, sol: S) {
@@ -106,11 +102,7 @@ class AndOrGraph[AT <: AOAndTask[S], OT <: AOOrTask[S], S](val root: OT, val cos
   object RootNode extends OrLeaf(null, root) {
 
     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.updateMin()
-
-      tree = n
+      tree = new OrNode(null, succ, root)
     }
   }
 
@@ -122,10 +114,13 @@ class AndOrGraph[AT <: AOAndTask[S], OT <: AOOrTask[S], S](val root: OT, val cos
   }
 
 
-  class OrNode(val parent: AndNode, var alternatives: Map[AT, AndTree], val task: OT) extends OrTree with Node[AndTree] {
-    var triedAlternatives       = Map[AT, AndTree]()
-    var minAlternative: AndTree = _
-    var minCost                 = costModel.taskCost(task)
+  class OrNode(val parent: AndNode, val altTasks: List[AT], val task: OT) extends OrTree with Node[AndTree] {
+    var alternatives: Map[AT, AndTree] = altTasks.map(t => t -> new AndLeaf(this, t)).toMap
+    var triedAlternatives              = Map[AT, AndTree]()
+    var minAlternative: AndTree        = _
+    var minCost                        = costModel.taskCost(task)
+
+    updateMin()
 
     def updateMin() {
       if (!alternatives.isEmpty) {

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

@@ -20,7 +20,7 @@ abstract class AndOrGraphSearch[AT <: AOAndTask[S],
           case l: g.Leaf =>
             collectLeaf(WL(l, newCosts.reverse)) 
           case a: g.AndNode =>
-            for (o <- (a.subProblems -- a.subSolutions.keySet).values) {
+            for (o <- a.subTasks.filterNot(a.subSolutions.keySet).map(a.subProblems)) {
               collectFromOr(o, newCosts)
             }
         }