Some organization

src/main/scala/leon/synthesis/Heuristics.scala

+package leon
+package synthesis
+
+import purescala.Common._
+import purescala.Trees._
+import purescala.Extractors._
+import purescala.TreeOps._
+import purescala.TypeTrees._
+
+object Heuristics {
+  def all(synth: Synthesizer) = Set(
+    new IntInduction(synth)
+  )
+}
+
+class OptimisticGround(synth: Synthesizer) extends Rule("Optimistic Ground", synth, 90) {
+  def applyOn(task: Task): RuleResult = {
+    val p = task.problem
+
+    if (!p.as.isEmpty && !p.xs.isEmpty) {
+      val xss = p.xs.toSet
+      val ass = p.as.toSet
+
+      val tpe = TupleType(p.xs.map(_.getType))
+
+      var i = 0;
+      var maxTries = 3;
+
+      var result: Option[RuleResult]   = None
+      var predicates: Seq[Expr]        = Seq()
+
+      while (result.isEmpty && i < maxTries) {
+        val phi = And(p.phi +: predicates)
+        synth.solveSAT(phi) match {
+          case (Some(true), satModel) =>
+            val satXsModel = satModel.filterKeys(xss) 
+
+            val newPhi = valuateWithModelIn(phi, xss, satModel)
+
+            synth.solveSAT(Not(newPhi)) match {
+              case (Some(true), invalidModel) =>
+                // Found as such as the xs break, refine predicates
+                predicates = valuateWithModelIn(phi, ass, invalidModel) +: predicates
+
+              case (Some(false), _) =>
+                result = Some(RuleSuccess(Solution(BooleanLiteral(true), Tuple(p.xs.map(valuateWithModel(satModel))).setType(tpe))))
+
+              case _ =>
+                result = Some(RuleInapplicable)
+            }
+
+          case (Some(false), _) =>
+            if (predicates.isEmpty) {
+              result = Some(RuleSuccess(Solution(BooleanLiteral(false), Error(p.phi+" is UNSAT!").setType(tpe))))
+            } else {
+              result = Some(RuleInapplicable)
+            }
+          case _ =>
+            result = Some(RuleInapplicable)
+        }
+
+        i += 1 
+      }
+
+      result.getOrElse(RuleInapplicable)
+    } else {
+      RuleInapplicable
+    }
+  }
+}
+
+
+class IntInduction(synth: Synthesizer) extends Rule("Int Induction", synth, 80) {
+  def applyOn(task: Task): RuleResult = {
+    val p = task.problem
+
+    p.as.find(_.getType == Int32Type) match {
+      case Some(inductOn) =>
+              
+        val subBase = Problem(p.as.filterNot(_ == inductOn), subst(inductOn -> IntLiteral(0), p.phi), p.xs)
+      //  val subGT   = Problem(p.as + tmpGT, And(Seq(p.phi, GreaterThan(Variable(inductOn), IntLiteral(0)), subst(inductOn -> IntLiteral(0), p.phi), p.xs)
+
+        RuleDecomposed(List(subBase), forward)
+      case None =>
+        RuleInapplicable
+    }
+  }
+}

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

@@ -8,13 +8,12 @@ import purescala.TreeOps._
 import purescala.TypeTrees._
 
 object Rules {
-  def all(synth: Synthesizer) = List(
+  def all(synth: Synthesizer) = Set(
     new Unification.DecompTrivialClash(synth),
     new Unification.OccursCheck(synth),
     new ADTDual(synth),
     new OnePoint(synth),
     new Ground(synth),
-    new OptimisticGround(synth),
     new CaseSplit(synth),
     new UnusedInput(synth),
     new UnconstrainedOutput(synth),
@@ -103,62 +102,6 @@ class Ground(synth: Synthesizer) extends Rule("Ground", synth, 500) {
   }
 }
 
-class OptimisticGround(synth: Synthesizer) extends Rule("Optimistic Ground", synth, 90) {
-  def applyOn(task: Task): RuleResult = {
-    val p = task.problem
-
-    if (!p.as.isEmpty && !p.xs.isEmpty) {
-      val xss = p.xs.toSet
-      val ass = p.as.toSet
-
-      val tpe = TupleType(p.xs.map(_.getType))
-
-      var i = 0;
-      var maxTries = 3;
-
-      var result: Option[RuleResult]   = None
-      var predicates: Seq[Expr]        = Seq()
-
-      while (result.isEmpty && i < maxTries) {
-        val phi = And(p.phi +: predicates)
-        synth.solveSAT(phi) match {
-          case (Some(true), satModel) =>
-            val satXsModel = satModel.filterKeys(xss) 
-
-            val newPhi = valuateWithModelIn(phi, xss, satModel)
-
-            synth.solveSAT(Not(newPhi)) match {
-              case (Some(true), invalidModel) =>
-                // Found as such as the xs break, refine predicates
-                predicates = valuateWithModelIn(phi, ass, invalidModel) +: predicates
-
-              case (Some(false), _) =>
-                result = Some(RuleSuccess(Solution(BooleanLiteral(true), Tuple(p.xs.map(valuateWithModel(satModel))).setType(tpe))))
-
-              case _ =>
-                result = Some(RuleInapplicable)
-            }
-
-          case (Some(false), _) =>
-            if (predicates.isEmpty) {
-              result = Some(RuleSuccess(Solution(BooleanLiteral(false), Error(p.phi+" is UNSAT!").setType(tpe))))
-            } else {
-              result = Some(RuleInapplicable)
-            }
-          case _ =>
-            result = Some(RuleInapplicable)
-        }
-
-        i += 1 
-      }
-
-      result.getOrElse(RuleInapplicable)
-    } else {
-      RuleInapplicable
-    }
-  }
-}
-
 class CaseSplit(synth: Synthesizer) extends Rule("Case-Split", synth, 200) {
   def applyOn(task: Task): RuleResult = {
     val p = task.problem
@@ -332,21 +275,3 @@ class ADTDual(synth: Synthesizer) extends Rule("ADTDual", synth, 200) {
   }
 }
 
-object Heuristics {
-  class IntInduction(synth: Synthesizer) extends Rule("Int Induction", synth, 80) {
-    def applyOn(task: Task): RuleResult = {
-      val p = task.problem
-
-      p.as.find(_.getType == Int32Type) match {
-        case Some(inductOn) =>
-                
-          val subBase = Problem(p.as.filterNot(_ == inductOn), subst(inductOn -> IntLiteral(0), p.phi), p.xs)
-        //  val subGT   = Problem(p.as + tmpGT, And(Seq(p.phi, GreaterThan(Variable(inductOn), IntLiteral(0)), subst(inductOn -> IntLiteral(0), p.phi), p.xs)
-
-          RuleDecomposed(List(subBase), forward)
-        case None =>
-          RuleInapplicable
-      }
-    }
-  }
-}

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

@@ -18,7 +18,7 @@ class Synthesizer(val r: Reporter, val solvers: List[Solver], generateDerivation
 
   var derivationCounter = 1;
 
-  def synthesize(p: Problem, rules: List[Rule]): Solution = {
+  def synthesize(p: Problem, rules: Set[Rule]): Solution = {
 
     val workList = new PriorityQueue[Task]()
     val rootTask = new RootTask(this, p)
@@ -56,7 +56,7 @@ class Synthesizer(val r: Reporter, val solvers: List[Solver], generateDerivation
     (None, Map())
   }
 
-  val rules = Rules.all(this)
+  val rules = Rules.all(this) ++ Heuristics.all(this)
 
   import purescala.Trees._
   def synthesizeAll(program: Program): Map[Choose, Solution] = {

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

@@ -33,7 +33,7 @@ class SimpleTask(synth: Synthesizer,
   }
 
   def run: List[Task] = {
-    synth.rules.map(r => new ApplyRuleTask(synth, this, problem, r))
+    synth.rules.map(r => new ApplyRuleTask(synth, this, problem, r)).toList
   }
 
   var failed = Set[Rule]()

testcases/synthesis/SortedList.scala

@@ -24,6 +24,9 @@ object SortedList {
 
   def insertSynth(in: List, v: Int) = choose{ (out: List) => content(out) == content(in) ++ Set(v) }
 
+  def tailSynth(in: List) = choose{out: List => size(out)+1 == size(in)}
+  def consSynth(in: List) = choose{out: List => size(out) == size(in)+1}
+
   def insert1(l: List, v: Int) = (
     Cons(v, l)
   ) ensuring(res => content(res) == content(l) ++ Set(v) && size(res) >= size(l))