By convention, we reserve priorities 1-99 to heuristics

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

@@ -22,7 +22,7 @@ trait Heuristic {
   override def toString = "H: "+name
 }
 
-class OptimisticGround(synth: Synthesizer) extends Rule("Optimistic Ground", synth, 9) with Heuristic {
+class OptimisticGround(synth: Synthesizer) extends Rule("Optimistic Ground", synth, 90) with Heuristic {
   def applyOn(task: Task): RuleResult = {
     val p = task.problem
 
@@ -79,7 +79,7 @@ class OptimisticGround(synth: Synthesizer) extends Rule("Optimistic Ground", syn
 }
 
 
-class IntInduction(synth: Synthesizer) extends Rule("Int Induction", synth, 8) with Heuristic {
+class IntInduction(synth: Synthesizer) extends Rule("Int Induction", synth, 80) with Heuristic {
   def applyOn(task: Task): RuleResult = {
     val p = task.problem
 
@@ -124,7 +124,7 @@ class IntInduction(synth: Synthesizer) extends Rule("Int Induction", synth, 8) w
   }
 }
 
-class OptimisticInjection(synth: Synthesizer) extends Rule("Opt. Injection", synth, 5) with Heuristic {
+class OptimisticInjection(synth: Synthesizer) extends Rule("Opt. Injection", synth, 50) with Heuristic {
   def applyOn(task: Task): RuleResult = {
     val p = task.problem
 
@@ -148,9 +148,42 @@ class OptimisticInjection(synth: Synthesizer) extends Rule("Opt. Injection", syn
         val args     = argss(0) zip argss(1)
 
         newExprs ++= args.map{ case (l, r) => Equals(l, r) }
+        newExprs = newExprs.filterNot(toRemove)
+      }
+
+      val sub = p.copy(phi = And(newExprs))
+
+      RuleDecomposed(List(sub), forward)
+    } else {
+      RuleInapplicable
+    }
+  }
+}
+
+class SelectiveInlining(synth: Synthesizer) extends Rule("Sel. Inlining", synth, 20) with Heuristic {
+  def applyOn(task: Task): RuleResult = {
+    val p = task.problem
+
+    val TopLevelAnds(exprs) = p.phi
 
+    val eqfuncalls = exprs.collect{
+      case eq @ Equals(FunctionInvocation(fd, args), e) =>
+        ((fd, e), args, eq : Expr)
+      case eq @ Equals(e, FunctionInvocation(fd, args)) =>
+        ((fd, e), args, eq : Expr)
+    }
+
+    val candidates = eqfuncalls.groupBy(_._1).filter(_._2.size > 1)
+    if (!candidates.isEmpty) {
 
+      var newExprs = exprs
+      for (cands <- candidates.values) {
+        val cand = cands.take(2)
+        val toRemove = cand.map(_._3).toSet
+        val argss    = cand.map(_._2)
+        val args     = argss(0) zip argss(1)
 
+        newExprs ++= args.map{ case (l, r) => Equals(l, r) }
         newExprs = newExprs.filterNot(toRemove)
       }
 

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

@@ -42,7 +42,7 @@ abstract class Rule(val name: String, val synth: Synthesizer, val priority: Prio
   override def toString = "R: "+name
 }
 
-class OnePoint(synth: Synthesizer) extends Rule("One-point", synth, 30) {
+class OnePoint(synth: Synthesizer) extends Rule("One-point", synth, 300) {
   def applyOn(task: Task): RuleResult = {
 
     val p = task.problem
@@ -81,7 +81,7 @@ class OnePoint(synth: Synthesizer) extends Rule("One-point", synth, 30) {
   }
 }
 
-class Ground(synth: Synthesizer) extends Rule("Ground", synth, 50) {
+class Ground(synth: Synthesizer) extends Rule("Ground", synth, 500) {
   def applyOn(task: Task): RuleResult = {
     val p = task.problem
 
@@ -103,7 +103,7 @@ class Ground(synth: Synthesizer) extends Rule("Ground", synth, 50) {
   }
 }
 
-class CaseSplit(synth: Synthesizer) extends Rule("Case-Split", synth, 20) {
+class CaseSplit(synth: Synthesizer) extends Rule("Case-Split", synth, 200) {
   def applyOn(task: Task): RuleResult = {
     val p = task.problem
     p.phi match {
@@ -123,7 +123,7 @@ class CaseSplit(synth: Synthesizer) extends Rule("Case-Split", synth, 20) {
   }
 }
 
-class Assert(synth: Synthesizer) extends Rule("Assert", synth, 20) {
+class Assert(synth: Synthesizer) extends Rule("Assert", synth, 200) {
   def applyOn(task: Task): RuleResult = {
     val p = task.problem
 
@@ -159,7 +159,7 @@ class Assert(synth: Synthesizer) extends Rule("Assert", synth, 20) {
   }
 }
 
-class UnusedInput(synth: Synthesizer) extends Rule("UnusedInput", synth, 10) {
+class UnusedInput(synth: Synthesizer) extends Rule("UnusedInput", synth, 100) {
   def applyOn(task: Task): RuleResult = {
     val p = task.problem
     val unused = p.as.toSet -- variablesOf(p.phi)
@@ -174,7 +174,7 @@ class UnusedInput(synth: Synthesizer) extends Rule("UnusedInput", synth, 10) {
   }
 }
 
-class UnconstrainedOutput(synth: Synthesizer) extends Rule("Unconstr.Output", synth, 10) {
+class UnconstrainedOutput(synth: Synthesizer) extends Rule("Unconstr.Output", synth, 100) {
   def applyOn(task: Task): RuleResult = {
     val p = task.problem
     val unconstr = p.xs.toSet -- variablesOf(p.phi)
@@ -198,7 +198,7 @@ class UnconstrainedOutput(synth: Synthesizer) extends Rule("Unconstr.Output", sy
 }
 
 object Unification {
-  class DecompTrivialClash(synth: Synthesizer) extends Rule("Unif Dec./Clash/Triv.", synth, 20) {
+  class DecompTrivialClash(synth: Synthesizer) extends Rule("Unif Dec./Clash/Triv.", synth, 200) {
     def applyOn(task: Task): RuleResult = {
       val p = task.problem
 
@@ -226,7 +226,7 @@ object Unification {
     }
   }
 
-  class OccursCheck(synth: Synthesizer) extends Rule("Unif OccursCheck", synth, 20) {
+  class OccursCheck(synth: Synthesizer) extends Rule("Unif OccursCheck", synth, 200) {
     def applyOn(task: Task): RuleResult = {
       val p = task.problem
 
@@ -253,7 +253,7 @@ object Unification {
 }
 
 
-class ADTDual(synth: Synthesizer) extends Rule("ADTDual", synth, 20) {
+class ADTDual(synth: Synthesizer) extends Rule("ADTDual", synth, 200) {
   def applyOn(task: Task): RuleResult = {
     val p = task.problem