Add heuristic exploiting an optimistic assumption about injective nature of functions.

foo(x) == expr && foo(y) == expr  --> x == y

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

@@ -11,11 +11,18 @@ import purescala.Definitions._
 object Heuristics {
   def all(synth: Synthesizer) = Set(
     new OptimisticGround(synth),
-    new IntInduction(synth)
+    new IntInduction(synth),
+    new OptimisticInjection(synth)
   )
 }
 
-class OptimisticGround(synth: Synthesizer) extends Rule("Optimistic Ground", synth, 9) {
+trait Heuristic {
+  this: Rule =>
+
+  override def toString = "H: "+name
+}
+
+class OptimisticGround(synth: Synthesizer) extends Rule("Optimistic Ground", synth, 9) with Heuristic {
   def applyOn(task: Task): RuleResult = {
     val p = task.problem
 
@@ -72,7 +79,7 @@ class OptimisticGround(synth: Synthesizer) extends Rule("Optimistic Ground", syn
 }
 
 
-class IntInduction(synth: Synthesizer) extends Rule("Int Induction", synth, 8) {
+class IntInduction(synth: Synthesizer) extends Rule("Int Induction", synth, 8) with Heuristic {
   def applyOn(task: Task): RuleResult = {
     val p = task.problem
 
@@ -116,3 +123,42 @@ class IntInduction(synth: Synthesizer) extends Rule("Int Induction", synth, 8) {
     }
   }
 }
+
+class OptimisticInjection(synth: Synthesizer) extends Rule("Opt. Injection", synth, 5) 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)
+      }
+
+      val sub = p.copy(phi = And(newExprs))
+
+      RuleDecomposed(List(sub), forward)
+    } else {
+      RuleInapplicable
+    }
+  }
+}

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

@@ -39,7 +39,7 @@ abstract class Rule(val name: String, val synth: Synthesizer, val priority: Prio
     case _ => Solution.none
   }
 
-  override def toString = name
+  override def toString = "R: "+name
 }
 
 class OnePoint(synth: Synthesizer) extends Rule("One-point", synth, 30) {

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

@@ -54,15 +54,6 @@ class Synthesizer(val r: Reporter,
       // Check if solving this task has the slightest chance of improving the
       // current solution
       if (task.minComplexity < bestSolutionSoFar().complexity) {
-        if (!subProblems.isEmpty) {
-          val prefix = "[%-20s] ".format(Option(task.rule).map(_.name).getOrElse("root"))
-          println(prefix+"Got: "+task.problem)
-          println(prefix+"Decomposed into:")
-          for(p <- subProblems) {
-            println(prefix+" - "+p)
-          }
-        }
-
         for (p <- subProblems; r <- rules) yield {
           workList += new Task(this, task, p, r)
         }

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

@@ -58,6 +58,11 @@ class Task(synth: Synthesizer,
         // Solved
         this.solution = Some(solution)
         parent.partlySolvedBy(this, solution)
+
+        val prefix = "[%-20s] ".format(Option(rule).map(_.toString).getOrElse("root"))
+        println(prefix+"Got: "+problem)
+        println(prefix+"Solved with: "+solution)
+
         Nil
 
       case RuleDecomposed(subProblems, onSuccess) =>
@@ -67,6 +72,13 @@ class Task(synth: Synthesizer,
         val simplestSolution = onSuccess(subProblems.map(Solution.basic _))
         minComplexity = new FixedSolComplexity(parent.minComplexity.value + simplestSolution.complexity.value)
 
+        val prefix = "[%-20s] ".format(Option(rule).map(_.toString).getOrElse("root"))
+        println(prefix+"Got: "+problem)
+        println(prefix+"Decomposed into:")
+        for(p <- subProblems) {
+          println(prefix+" - "+p)
+        }
+
         subProblems
 
       case RuleInapplicable =>