Implement the concept of Normalizing rules

Normalizing rules are rules that:
1) always help synthesis
2) are commutative
3) should be applied as early as possible

Here we apply normalizing rules explicitly before all other rules, and
in a deterministic order. This should dramatically reduce the search
space in cases where such rules apply.

Note that rules that are said to be normalizing should never fail once
instantiated.

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

@@ -7,7 +7,7 @@ import purescala.TypeTrees.TupleType
 import heuristics._
 
 object Heuristics {
-  def all = Set[Rule](
+  def all = List[Rule](
     IntInduction,
     InnerCaseSplit,
     //new OptimisticInjection(_),

src/main/scala/leon/synthesis/ParallelSearch.scala

@@ -8,7 +8,7 @@ import solvers.TrivialSolver
 
 class ParallelSearch(synth: Synthesizer,
                      problem: Problem,
-                     rules: Set[Rule],
+                     rules: Seq[Rule],
                      costModel: CostModel,
                      nWorkers: Int) extends AndOrGraphParallelSearch[SynthesisContext, TaskRunRule, TaskTryRules, Solution](new AndOrGraph(TaskTryRules(problem), SearchCostModel(costModel)), nWorkers) {
 
@@ -69,14 +69,22 @@ class ParallelSearch(synth: Synthesizer,
   }
 
   def expandOrTask(ref: ActorRef, sctx: SynthesisContext)(t: TaskTryRules) = {
-    val sub = rules.flatMap { r => 
-      r.instantiateOn(sctx, t.p).map(TaskRunRule(_))
-    }
+    val (normRules, otherRules) = rules.partition(_.isInstanceOf[NormalizingRule])
+
+    val normApplications = normRules.flatMap(_.instantiateOn(sctx, t.p))
 
-    if (!sub.isEmpty) {
-      Expanded(sub.toList)
+    if (!normApplications.isEmpty) {
+      Expanded(List(TaskRunRule(normApplications.head)))
     } else {
-      ExpandFailure()
+      val sub = otherRules.flatMap { r =>
+        r.instantiateOn(sctx, t.p).map(TaskRunRule(_))
+      }
+
+      if (!sub.isEmpty) {
+        Expanded(sub.toList)
+      } else {
+        ExpandFailure()
+      }
     }
   }
 }

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

@@ -8,7 +8,7 @@ import purescala.TreeOps._
 import rules._
 
 object Rules {
-  def all = Set[Rule](
+  def all = List[Rule](
     Unification.DecompTrivialClash,
     Unification.OccursCheck, // probably useless
     Disunification.Decomp,
@@ -89,3 +89,10 @@ abstract class Rule(val name: String) {
 
   override def toString = "R: "+name
 }
+
+// Note: Rules that extend NormalizingRule should all be commutative, The will
+// be applied before others in a deterministic order and their application
+// should never fail!
+abstract class NormalizingRule(name: String) extends Rule(name) {
+  override def toString = "N: "+name
+}

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

@@ -32,7 +32,7 @@ case class SearchCostModel(cm: CostModel) extends AOCostModel[TaskRunRule, TaskT
 
 class SimpleSearch(synth: Synthesizer,
                    problem: Problem,
-                   rules: Set[Rule],
+                   rules: Seq[Rule],
                    costModel: CostModel) extends AndOrGraphSearch[TaskRunRule, TaskTryRules, Solution](new AndOrGraph(TaskTryRules(problem), SearchCostModel(costModel))) {
 
   import synth.reporter._
@@ -64,12 +64,22 @@ class SimpleSearch(synth: Synthesizer,
   }
 
   def expandOrTask(t: TaskTryRules): ExpandResult[TaskRunRule] = {
-    val sub = rules.flatMap ( r => r.instantiateOn(sctx, t.p).map(TaskRunRule(_)) )
+    val (normRules, otherRules) = rules.partition(_.isInstanceOf[NormalizingRule])
 
-    if (!sub.isEmpty) {
-      Expanded(sub.toList)
+    val normApplications = normRules.flatMap(_.instantiateOn(sctx, t.p))
+
+    if (!normApplications.isEmpty) {
+      Expanded(List(TaskRunRule(normApplications.head)))
     } else {
-      ExpandFailure()
+      val sub = otherRules.flatMap { r =>
+        r.instantiateOn(sctx, t.p).map(TaskRunRule(_))
+      }
+
+      if (!sub.isEmpty) {
+        Expanded(sub.toList)
+      } else {
+        ExpandFailure()
+      }
     }
   }
 

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

@@ -22,7 +22,7 @@ class Synthesizer(val context : LeonContext,
                   val solver: Solver,
                   val program: Program,
                   val problem: Problem,
-                  val rules: Set[Rule],
+                  val rules: Seq[Rule],
                   val options: SynthesizerOptions) {
 
   protected[synthesis] val reporter = context.reporter

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

@@ -6,7 +6,7 @@ import purescala.Trees._
 import purescala.TreeOps._
 import purescala.Extractors._
 
-case object Assert extends Rule("Assert") {
+case object Assert extends NormalizingRule("Assert") {
   def instantiateOn(sctx: SynthesisContext, p: Problem): Traversable[RuleInstantiation] = {
     p.phi match {
       case TopLevelAnds(exprs) =>

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

@@ -6,7 +6,7 @@ import purescala.Trees._
 import purescala.TreeOps._
 import purescala.Extractors._
 
-case object OnePoint extends Rule("One-point") {
+case object OnePoint extends NormalizingRule("One-point") {
   def instantiateOn(sctx: SynthesisContext, p: Problem): Traversable[RuleInstantiation] = {
     val TopLevelAnds(exprs) = p.phi
 

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

@@ -6,7 +6,7 @@ import purescala.Trees._
 import purescala.TreeOps._
 import purescala.Extractors._
 
-case object UnconstrainedOutput extends Rule("Unconstr.Output") {
+case object UnconstrainedOutput extends NormalizingRule("Unconstr.Output") {
   def instantiateOn(sctx: SynthesisContext, p: Problem): Traversable[RuleInstantiation] = {
     val unconstr = p.xs.toSet -- variablesOf(p.phi)
 

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

@@ -6,7 +6,7 @@ import purescala.Trees._
 import purescala.TreeOps._
 import purescala.Extractors._
 
-case object UnusedInput extends Rule("UnusedInput") {
+case object UnusedInput extends NormalizingRule("UnusedInput") {
   def instantiateOn(sctx: SynthesisContext, p: Problem): Traversable[RuleInstantiation] = {
     val unused = p.as.toSet -- variablesOf(p.phi) -- variablesOf(p.pc)