Conflate inputs when possible

src/main/scala/leon/purescala/TreeOps.scala

@@ -336,6 +336,14 @@ object TreeOps {
     postMap(substs.lift)(expr)
   }
 
+  def replaceSeq(substs: Seq[(Expr, Expr)], expr: Expr): Expr = {
+    var res = expr
+    for (s <- substs) {
+      res = replace(Map(s), res)
+    }
+    res
+  }
+
 
   def replaceFromIDs(substs: Map[Identifier, Expr], expr: Expr) : Expr = {
     postMap( {

src/main/scala/leon/repair/Repairman.scala

@@ -58,9 +58,10 @@ class Repairman(ctx: LeonContext, initProgram: Program, fd: FunDef, verifTimeout
     val soptions = soptions0.copy(
       costModel = RepairCostModel(soptions0.costModel),
       rules = (soptions0.rules ++ Seq(
-        GuidedDecomp,
-        GuidedCloser,
-        CEGLESS
+        //GuidedDecomp,
+        //GuidedCloser,
+        CEGLESS,
+        TEGLESS
       )) diff Seq(ADTInduction)
     );
 
@@ -149,23 +150,15 @@ class Repairman(ctx: LeonContext, initProgram: Program, fd: FunDef, verifTimeout
         var res: Option[(Expr, Expr)] = None
 
         // in case scrut is an non-variable expr, we simplify to a variable + inject in env
-        val (sid, nenv) = scrut match {
-          case Variable(id) =>
-            (id, env)
-          case expr =>
-            val id = FreshIdentifier("scrut", true).copiedFrom(scrut)
-            (id, env + (id -> scrut))
-        }
-
         for (c <- cases if res.isEmpty) {
-          val cond = and(conditionForPattern(sid.toVariable, c.pattern, includeBinders = false),
+          val cond = and(conditionForPattern(scrut, c.pattern, includeBinders = false),
                          c.optGuard.getOrElse(BooleanLiteral(true)))
-          val map  = mapForPattern(sid.toVariable, c.pattern)
+          val map  = mapForPattern(scrut, c.pattern)
 
 
-          forAllTests(cond, nenv ++ map) match {
+          forAllTests(cond, env ++ map) match {
             case Some(true) =>
-              val (b, r) = focus(c.rhs, nenv ++ map)
+              val (b, r) = focus(c.rhs, env ++ map)
               res = Some((MatchExpr(scrut, cases.map { c2 =>
                 if (c2 eq c) {
                   c2.copy(rhs = b)

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

@@ -20,6 +20,7 @@ object Rules {
     CaseSplit,
     IfSplit,
     UnusedInput,
+    EquivalentInputs,
     UnconstrainedOutput,
     OptimisticGround,
     EqualitySplit,

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

@@ -600,6 +600,7 @@ abstract class CEGISLike[T <% Typed](name: String) extends Rule(name) {
                   val e = examples.next()
                   if (!ndProgram.testForProgram(bs)(e)) {
                     failedTestsStats(e) += 1
+                    //sctx.reporter.debug(" Program: "+ndProgram.determinize(bs)+" failed on "+e)
                     wrongPrograms += bs
                     prunedPrograms -= bs
 

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

@@ -26,6 +26,13 @@ case object CEGLESS extends CEGISLike[Label[String]]("CEGLESS") {
 
     val inputs = p.as.map(_.toVariable)
 
+    sctx.reporter.ifDebug { printer =>
+      printer("Guides available:")
+      for (g <- guides) {
+        printer(" - "+g)
+      }
+    }
+
     val guidedGrammar = guides.map(SimilarTo(_, inputs.toSet, sctx, p)).foldLeft[ExpressionGrammar[Label[String]]](Empty())(_ || _)
 
     CegisParams(

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

+/* Copyright 2009-2014 EPFL, Lausanne */
+
+package leon
+package synthesis
+package rules
+
+import leon.utils._
+import purescala.Trees._
+import purescala.TreeOps._
+import purescala.Extractors._
+
+case object EquivalentInputs extends NormalizingRule("EquivalentInputs") {
+  def instantiateOn(sctx: SynthesisContext, p: Problem): Traversable[RuleInstantiation] = {
+    val TopLevelAnds(clauses) = p.pc
+
+    def discoverEquivalences(allClauses: Seq[Expr]): Seq[(Expr, Expr)] = {
+      val instanceOfs = allClauses.collect {
+        case ccio @ CaseClassInstanceOf(cct, s) => ccio
+      }
+
+      var clauses = allClauses.filterNot(instanceOfs.toSet)
+
+      val ccSubsts = for (CaseClassInstanceOf(cct, s) <- instanceOfs) yield {
+
+        val fieldsVals = (for (f <- cct.fields) yield {
+          val id = f.id
+
+          clauses.find {
+            case Equals(e, CaseClassSelector(`cct`, `s`, `id`)) => true
+            case _ => false
+          } match {
+            case Some(Equals(e, _)) =>
+              Some(e)
+            case _ =>
+              None
+          }
+
+        }).flatten
+
+        
+        if (fieldsVals.size == cct.fields.size) {
+          Some((s, CaseClass(cct, fieldsVals)))
+        } else {
+          None
+        }
+      }
+
+      ccSubsts.flatten
+    }
+
+
+    val substs = discoverEquivalences(clauses)
+
+    if (substs.nonEmpty) {
+      val simplifier = Simplifiers.bestEffort(sctx.context, sctx.program) _
+
+      val sub = p.copy(ws = replaceSeq(substs, p.ws), 
+                       pc = simplifier(replaceSeq(substs, p.pc)),
+                       phi = simplifier(replaceSeq(substs, p.phi)))
+
+      List(RuleInstantiation.immediateDecomp(p, this, List(sub), forward, this.name))
+    } else {
+      Nil
+    }
+  }
+}

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

@@ -28,14 +28,6 @@ case object GuidedDecomp extends Rule("Guided Decomp") {
 
     val simplify = Simplifiers.bestEffort(sctx.context, sctx.program)_
 
-    def doSubstitute(substs: Seq[(Expr, Expr)], e: Expr): Expr = {
-      var res = e
-      for (s <- substs) {
-        res = postMap(Map(s).lift)(res)
-      }
-      res
-    }
-
     val alts = guides.collect {
       case g @ IfExpr(c, thn, els) =>
         val sub1 = p.copy(ws = replace(Map(g -> thn), p.ws), pc = and(c, replace(Map(g -> thn), p.pc)))
@@ -66,11 +58,11 @@ case object GuidedDecomp extends Rule("Guided Decomp") {
           
           val pc  = simplify(and(
             scrutCond,
-            replace(Map(scrut0 -> scrut), doSubstitute(substs,scrutConstraint)),
+            replace(Map(scrut0 -> scrut), replaceSeq(substs,scrutConstraint)),
             replace(Map(scrut0 -> scrut), replace(Map(m -> c.rhs), andJoin(cond)))
           ))
           val ws = replace(Map(m -> c.rhs), p.ws)
-          val phi = doSubstitute(substs, p.phi)
+          val phi = replaceSeq(substs, p.phi)
           val free = variablesOf(and(pc, phi)) -- p.xs
           val asPrefix = p.as.filter(free)
 

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

@@ -16,9 +16,10 @@ import datagen._
 import utils._
 
 case object TEGIS extends TEGISLike[TypeTree]("TEGIS") {
-  def getGrammar(sctx: SynthesisContext, p: Problem) = {
-    ExpressionGrammars.default(sctx, p)
+  def getParams(sctx: SynthesisContext, p: Problem) = {
+    TegisParams(
+      grammar = ExpressionGrammars.default(sctx, p),
+      rootLabel = {(tpe: TypeTree) => tpe }
+    )
   }
-
-  def getRootLabel(tpe: TypeTree): TypeTree = tpe
 }

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

@@ -21,19 +21,22 @@ import bonsai._
 import bonsai.enumerators._
 
 abstract class TEGISLike[T <% Typed](name: String) extends Rule(name) {
-  def getGrammar(sctx: SynthesisContext, p: Problem): ExpressionGrammar[T]
+  case class TegisParams(
+    grammar: ExpressionGrammar[T],
+    rootLabel: TypeTree => T,
+    enumLimit: Int = 10000,
+    reorderInterval: Int = 50
+  );
 
-  def getRootLabel(tpe: TypeTree): T
-
-  val enumLimit = 10000;
-  val testsReorderInterval = 50; // Every X test filterings, we reorder tests with most filtering first.
+  def getParams(sctx: SynthesisContext, p: Problem): TegisParams
 
   def instantiateOn(sctx: SynthesisContext, p: Problem): Traversable[RuleInstantiation] = {
 
     List(new RuleInstantiation(p, this, SolutionBuilder.none, this.name, this.priority) {
       def apply(sctx: SynthesisContext): RuleApplication = {
 
-        val grammar = getGrammar(sctx, p)
+        val params = getParams(sctx, p)
+        val grammar = params.grammar
 
         var tests = p.getTests(sctx).map(_.ins).distinct
         if (tests.nonEmpty) {
@@ -53,7 +56,7 @@ abstract class TEGISLike[T <% Typed](name: String) extends Rule(name) {
 
           val timers = sctx.context.timers.synthesis.rules.tegis;
 
-          val allExprs = enum.iterator(getRootLabel(targetType))
+          val allExprs = enum.iterator(params.rootLabel(targetType))
 
           var failStat = Map[Seq[Expr], Int]().withDefaultValue(0)
 
@@ -63,7 +66,7 @@ abstract class TEGISLike[T <% Typed](name: String) extends Rule(name) {
           def findNext(): Option[Expr] = {
             candidate = None
             timers.generating.start()
-            allExprs.take(enumLimit).takeWhile(e => candidate.isEmpty).foreach { e =>
+            allExprs.take(params.enumLimit).takeWhile(e => candidate.isEmpty).foreach { e =>
               val exprToTest = if (!isWrapped) {
                 Let(p.xs.head, e, p.phi)
               } else {
@@ -93,7 +96,7 @@ abstract class TEGISLike[T <% Typed](name: String) extends Rule(name) {
               }
               timers.testing.stop()
 
-              if (n % testsReorderInterval == 0) {
+              if (n % params.reorderInterval == 0) {
                 tests = tests.sortBy(t => -failStat(t))
               }
               n += 1
@@ -114,6 +117,7 @@ abstract class TEGISLike[T <% Typed](name: String) extends Rule(name) {
 
           RuleClosed(toStream())
         } else {
+          sctx.reporter.debug("No test available")
           RuleFailed()
         }
       }

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

+/* Copyright 2009-2014 EPFL, Lausanne */
+
+package leon
+package synthesis
+package rules
+
+import purescala.Trees._
+import purescala.TreeOps._
+import purescala.TypeTrees._
+import purescala.Common._
+import purescala.Definitions._
+import purescala.Extractors._
+import utils._
+import utils.ExpressionGrammars._
+
+case object TEGLESS extends TEGISLike[Label[String]]("TEGLESS") {
+  def getParams(sctx: SynthesisContext, p: Problem) = {
+
+    val TopLevelAnds(clauses) = p.ws
+
+    val guide = sctx.program.library.guide.get
+
+    val guides = clauses.collect {
+      case FunctionInvocation(TypedFunDef(`guide`, _), Seq(expr)) => expr
+    }
+
+    val inputs = p.as.map(_.toVariable)
+
+    sctx.reporter.ifDebug { printer =>
+      printer("Guides available:")
+      for (g <- guides) {
+        printer(" - "+g)
+      }
+    }
+
+    val guidedGrammar = guides.map(SimilarTo(_, inputs.toSet, sctx, p)).foldLeft[ExpressionGrammar[Label[String]]](Empty())(_ || _)
+
+    TegisParams(
+      grammar = guidedGrammar,
+      rootLabel = { (tpe: TypeTree) => Label(tpe, "G0") }
+    )
+  }
+}
+
+
+

src/main/scala/leon/synthesis/utils/ExpressionGrammar.scala

@@ -222,7 +222,7 @@ object ExpressionGrammars {
             gl -> Generator(subEls.updated(i, sgl), builder)
           }
 
-          val swaps = if (subs.size > 1 || isCommutative(e)) {
+          val swaps = if (subs.size > 1 && !isCommutative(e)) {
             (for (i <- 0 until subs.size;
                  j <- i+1 until subs.size) yield {