Synthesis: Don't filter tests during decomposition. Filter as needed in terminal rules.

src/main/scala/leon/repair/rules/Focus.scala

@@ -31,6 +31,8 @@ case object Focus extends PreprocessingRule("Focus") {
         
     }
 
+    val qeb = p.qebFiltered
+
     val fd      = hctx.functionContext
     val program = hctx.program
 
@@ -43,7 +45,7 @@ case object Focus extends PreprocessingRule("Focus") {
     def forAllTests(e: Expr, env: Map[Identifier, Expr], evaluator: Evaluator): Option[Boolean] = {
       var soFar: Option[Boolean] = None
 
-      p.eb.invalids.foreach { ex =>
+      qeb.invalids.foreach { ex =>
         evaluator.eval(e, (p.as zip ex.ins).toMap ++ env) match {
           case EvaluationResults.Successful(BooleanLiteral(b)) => 
             soFar match {
@@ -65,7 +67,7 @@ case object Focus extends PreprocessingRule("Focus") {
     }
 
     def existsFailing(e: Expr, env: Map[Identifier, Expr], evaluator: DeterministicEvaluator): Boolean = {
-      p.eb.invalids.exists { ex =>
+      qeb.invalids.exists { ex =>
         evaluator.eval(e, (p.as zip ex.ins).toMap ++ env).result match {
           case Some(BooleanLiteral(b)) => b
           case _ => true
@@ -105,7 +107,7 @@ case object Focus extends PreprocessingRule("Focus") {
           case Some(true) =>
             val cx = FreshIdentifier("cond", BooleanType)
             // Focus on condition
-            val np = Problem(p.as, ws(c), p.pc, letTuple(p.xs, IfExpr(cx.toVariable, thn, els), p.phi), List(cx), p.eb.stripOuts)
+            val np = Problem(p.as, ws(c), p.pc, letTuple(p.xs, IfExpr(cx.toVariable, thn, els), p.phi), List(cx), qeb.stripOuts)
 
             Some(decomp(List(np), termWrap(IfExpr(_, thn, els)), s"Focus on if-cond '${c.asString}'")(p))
 
@@ -113,17 +115,17 @@ case object Focus extends PreprocessingRule("Focus") {
             // Try to focus on branches
             forAllTests(c, Map(), evaluator) match {
               case Some(true) =>
-                val np = Problem(p.as, ws(thn), p.pc withCond c, p.phi, p.xs, p.qeb.filterIns(c))
+                val np = Problem(p.as, ws(thn), p.pc withCond c, p.phi, p.xs, qeb.filterIns(c))
 
                 Some(decomp(List(np), termWrap(IfExpr(c, _, els), c), s"Focus on if-then")(p))
               case Some(false) =>
-                val np = Problem(p.as, ws(els), p.pc withCond not(c), p.phi, p.xs, p.qeb.filterIns(not(c)))
+                val np = Problem(p.as, ws(els), p.pc withCond not(c), p.phi, p.xs, qeb.filterIns(not(c)))
 
                 Some(decomp(List(np), termWrap(IfExpr(c, thn, _), not(c)), s"Focus on if-else")(p))
               case None =>
                 // We split
-                val sub1 = p.copy(ws = ws(thn), pc = p.pc map (replace(Map(g -> thn), _)) withCond     c , eb = p.qeb.filterIns(c))
-                val sub2 = p.copy(ws = ws(els), pc = p.pc map (replace(Map(g -> thn), _)) withCond Not(c), eb = p.qeb.filterIns(Not(c)))
+                val sub1 = p.copy(ws = ws(thn), pc = p.pc map (replace(Map(g -> thn), _)) withCond     c , eb = qeb.filterIns(c))
+                val sub2 = p.copy(ws = ws(els), pc = p.pc map (replace(Map(g -> thn), _)) withCond Not(c), eb = qeb.filterIns(Not(c)))
 
                 val onSuccess: List[Solution] => Option[Solution] = { 
                   case List(s1, s2) =>
@@ -151,7 +153,7 @@ case object Focus extends PreprocessingRule("Focus") {
             val vars = map.toSeq.map(_._1)
 
             // Filter tests by the path-condition
-            val eb2 = p.qeb.filterIns(cond.toClause)
+            val eb2 = qeb.filterIns(cond.toClause)
 
             // Augment test with the additional variables and their valuations
             val ebF: (Seq[Expr] => List[Seq[Expr]]) = { (e: Seq[Expr]) =>
@@ -185,7 +187,7 @@ case object Focus extends PreprocessingRule("Focus") {
         if (existsFailing(elsePc.toClause, Map(), evaluator)) {
           val newCase    = MatchCase(WildcardPattern(None), None, NoTree(scrut.getType))
 
-          val eb = p.qeb.filterIns(elsePc.toClause)
+          val eb = qeb.filterIns(elsePc.toClause)
 
           val newProblem = Problem(p.as, andJoin(wss), p.pc merge elsePc, p.phi, p.xs, eb)
 
@@ -232,7 +234,6 @@ case object Focus extends PreprocessingRule("Focus") {
           None
         }
 
-
       case Let(id, value, body) =>
         val ebF: (Seq[Expr] => List[Seq[Expr]]) = { (e: Seq[Expr]) =>
           val map = (p.as zip e).toMap
@@ -242,7 +243,7 @@ case object Focus extends PreprocessingRule("Focus") {
           }.toList
         }
 
-        val np = Problem(p.as, ws(body), p.pc withBinding (id -> value), p.phi, p.xs, p.eb.mapIns(ebF))
+        val np = Problem(p.as, ws(body), p.pc withBinding (id -> value), p.phi, p.xs, qeb.mapIns(ebF))
 
         Some(decomp(List(np), termWrap(Let(id, value, _)), s"Focus on let-body")(p))
 

src/main/scala/leon/synthesis/ExamplesBank.scala

@@ -3,6 +3,7 @@
 package leon
 package synthesis
 
+import evaluators.DefaultEvaluator
 import purescala.Definitions._
 import purescala.Expressions._
 import purescala.Constructors._
@@ -167,6 +168,8 @@ object ExamplesBank {
   * allows us to evaluate expressions. */
 case class QualifiedExamplesBank(as: List[Identifier], xs: List[Identifier], eb: ExamplesBank)(implicit hctx: SearchContext) {
 
+  lazy val evaluator = new DefaultEvaluator(hctx, hctx.program).setEvaluationFailOnChoose(true)
+
   def removeOuts(toRemove: Set[Identifier]): QualifiedExamplesBank = {
     val nxs    = xs.filterNot(toRemove)
     val toKeep = xs.zipWithIndex.filterNot(x => toRemove(x._1)).map(_._2)
@@ -183,9 +186,7 @@ case class QualifiedExamplesBank(as: List[Identifier], xs: List[Identifier], eb:
 
   /** Filter inputs through expr which is an expression evaluating to a boolean */
   def filterIns(expr: Expr): QualifiedExamplesBank = {
-    filterIns(m =>
-      hctx.defaultEvaluator.eval(expr, m)
-      .result == Some(BooleanLiteral(true)))
+    filterIns(m => evaluator.eval(expr, m).result.contains(BooleanLiteral(true)))
   }
 
   /** Filters inputs through the predicate pred, with an assignment of input variables to expressions. */
@@ -203,6 +204,7 @@ case class QualifiedExamplesBank(as: List[Identifier], xs: List[Identifier], eb:
   }
 
   /** Maps inputs through the function f
+    *
     * @return A new ExampleBank */
   def mapIns(f: Seq[(Identifier, Expr)] => List[Seq[Expr]]) = {
     eb map {

src/main/scala/leon/synthesis/Problem.scala

@@ -10,7 +10,7 @@ import purescala.Types._
 import purescala.Common._
 import purescala.Constructors._
 import purescala.Extractors._
-import purescala.Definitions.FunDef
+import leon.purescala.Definitions.FunDef
 import Witnesses._
 
 /** Defines a synthesis triple of the form:
@@ -21,6 +21,8 @@ import Witnesses._
   * @param pc The path condition so far
   * @param phi The formula on `as` and `xs` to satisfy
   * @param xs The list of output identifiers for which we want to compute a function
+  * @note Since the examples are not eagerly filtered by [[Rule]]s, some may not
+  *       pass the path condition. Use [[qebFiltered]] to get the legal ones.
   */
 case class Problem(as: List[Identifier], ws: Expr, pc: Path, phi: Expr, xs: List[Identifier], eb: ExamplesBank = ExamplesBank.empty) extends Printable {
 
@@ -50,12 +52,15 @@ case class Problem(as: List[Identifier], ws: Expr, pc: Path, phi: Expr, xs: List
     copy(ws = andJoin(wsList ++ es))
   }
 
+  def qebFiltered(implicit sctx: SearchContext) = qeb.filterIns(pc.fullClause)
+
   // Qualified example bank, allows us to perform operations (e.g. filter) with expressions
   def qeb(implicit sctx: SearchContext) = QualifiedExamplesBank(this.as, this.xs, eb)
 
 }
 
 object Problem {
+
   def fromSpec(
     spec: Expr,
     pc: Path = Path.empty,

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

@@ -19,15 +19,6 @@ import evaluators.DefaultEvaluator
   * it will create a match case statement on all known subtypes. */
 case object ADTSplit extends Rule("ADT Split.") {
 
-  protected class NoChooseEvaluator(ctx: LeonContext, prog: Program) extends DefaultEvaluator(ctx, prog) {
-    override def e(expr: Expr)(implicit rctx: RC, gctx: GC): Expr = expr match {
-      case ch: Choose =>
-        throw new EvalError("Choose!")
-      case _ =>
-        super.e(expr)
-    }
-  }
-
   def instantiateOn(implicit hctx: SearchContext, p: Problem): Traversable[RuleInstantiation] = {
     // We approximate knowledge of types based on facts found at the top-level
     // we don't care if the variables are known to be equal or not, we just
@@ -75,8 +66,6 @@ case object ADTSplit extends Rule("ADT Split.") {
       case Some((id, act, cases)) =>
         val oas = p.as.filter(_ != id)
 
-        val evaluator = new NoChooseEvaluator(hctx, hctx.program)
-
         val subInfo0 = for(ccd <- cases) yield {
           val isInputVar = p.as.contains(id)
           val cct = CaseClassType(ccd, act.tps)
@@ -101,6 +90,7 @@ case object ADTSplit extends Rule("ADT Split.") {
           val eb2 = {
             if (isInputVar) {
               // Filter out examples where id has the wrong type, and fix input variables
+              // Note: It is fine to filter here as no evaluation is required
               p.qeb.mapIns { inInfo =>
                 inInfo.toMap.apply(id) match {
                   case CaseClass(`cct`, vs) =>
@@ -110,10 +100,7 @@ case object ADTSplit extends Rule("ADT Split.") {
                 }
               }
             } else {
-              // Filter out examples where id has the wrong type
-              p.qeb.filterIns { inValues =>
-                evaluator.eval(id.toVariable, inValues ++ p.pc.bindings).result.exists(_.getType == cct)
-              }.eb
+              p.eb
             }
           }
           val newAs = if (isInputVar) args ::: oas else p.as
@@ -128,7 +115,6 @@ case object ADTSplit extends Rule("ADT Split.") {
           cct.fieldsTypes.count { t => t == act }
         }
 
-
         val onSuccess: List[Solution] => Option[Solution] = {
           case sols =>
             var globalPre = List[Expr]()

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

@@ -29,7 +29,7 @@ case object Assert extends NormalizingRule("Assert") {
               Some(solve(Solution(pre = andJoin(exprsA), defs = Set(), term = simplestOut)))
             }
           } else {
-            val sub = p.copy(pc = p.pc withConds exprsA, phi = andJoin(others), eb = p.qeb.filterIns(andJoin(exprsA)))
+            val sub = p.copy(pc = p.pc withConds exprsA, phi = andJoin(others))
 
             Some(decomp(List(sub), {
               case List(s @ Solution(pre, defs, term, isTrusted)) =>

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

@@ -772,7 +772,7 @@ abstract class CEGISLike(name: String) extends Rule(name) {
           }
         }
 
-        val baseExampleInputs = p.qeb.filterIns(p.pc.fullClause).eb.examples ++ solverExample
+        val baseExampleInputs = p.qebFiltered.examples ++ solverExample
 
         ifDebug { debug =>
           baseExampleInputs.foreach { in =>

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

@@ -50,16 +50,13 @@ case object GenericTypeEqualitySplit extends Rule("Eq. Split") {
             pc = p.pc map (subst(f -> t, _)),
             ws = subst(f -> t, p.ws),
             phi = subst(f -> t, p.phi),
-            eb = p.qeb.filterIns(Equals(v1, v2)).removeIns(Set(f))
+            eb = p.qeb.removeIns(Set(f))
           )
         } else {
           p.copy(pc = p.pc withCond Equals(v1,v2)).withWs(Seq(Inactive(f))) // FIXME!
         }
 
-        val neq = p.copy(
-          pc = p.pc withCond not(Equals(v1, v2)),
-          eb = p.qeb.filterIns(not(Equals(v1, v2))) // FIXME!
-        )
+        val neq = p.copy(pc = p.pc withCond not(Equals(v1, v2)))
 
         val subProblems = List(eq, neq)
 

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

@@ -13,8 +13,8 @@ case object IfSplit extends Rule("If-Split") {
 
     def split(i: IfExpr, description: String): RuleInstantiation = {
       val subs = List(
-        Problem(p.as, p.ws, p.pc withCond i.cond, replace(Map(i -> i.thenn), p.phi), p.xs, p.qeb.filterIns(i.cond)),
-        Problem(p.as, p.ws, p.pc withCond not(i.cond), replace(Map(i -> i.elze), p.phi), p.xs, p.qeb.filterIns(not(i.cond)))
+        Problem(p.as, p.ws, p.pc withCond i.cond, replace(Map(i -> i.thenn), p.phi), p.xs),
+        Problem(p.as, p.ws, p.pc withCond not(i.cond), replace(Map(i -> i.elze), p.phi), p.xs)
       )
 
       val onSuccess: List[Solution] => Option[Solution] = {

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

@@ -57,12 +57,12 @@ case object InequalitySplit extends Rule("Ineq. Split.") {
 
         val lt = if (!facts.contains(LT(v1, v2))) {
           val pc = LessThan(v1, v2)
-          Some(pc, p.copy(pc = p.pc withCond pc, eb = p.qeb.filterIns(pc)))
+          Some(pc, p.copy(pc = p.pc withCond pc))
         } else None
 
         val gt = if (!facts.contains(LT(v2, v1))) {
           val pc = GreaterThan(v1, v2)
-          Some(pc, p.copy(pc = p.pc withCond pc, eb = p.qeb.filterIns(pc)))
+          Some(pc, p.copy(pc = p.pc withCond pc))
         } else None
 
         val eq = if (!facts.contains(EQ(v1, v2)) && !facts.contains(EQ(v2,v1))) {
@@ -79,7 +79,7 @@ case object InequalitySplit extends Rule("Ineq. Split.") {
               pc = p.pc map (subst(f -> t, _)),
               ws = subst(f -> t, p.ws),
               phi = subst(f -> t, p.phi),
-              eb = p.qeb.filterIns(Equals(v1, v2)).removeIns(Set(f))
+              eb = p.qeb.removeIns(Set(f))
             )
           } else {
             p.copy(pc = p.pc withCond pc).withWs(Seq(Inactive(f))) // equality in pc is fine for numeric types

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

@@ -15,12 +15,10 @@ case object InputSplit extends Rule("In. Split") {
     p.allAs.filter(_.getType == BooleanType).flatMap { a =>
       def getProblem(v: Boolean): Problem = {
         def replaceA(e: Expr) = replaceFromIDs(Map(a -> BooleanLiteral(v)), e)
-
-        val tests = QualifiedExamplesBank(p.as, p.xs, p.qeb.filterIns(m => m(a) == BooleanLiteral(v)))
         
         val newPc: Path = {
           val withoutA = p.pc -- Set(a) map replaceA
-          withoutA withConds (p.pc.bindings.find(_._1 == a).map { case (id, res) =>
+          withoutA withConds (p.pc.bindings.collectFirst { case (`a`, res) =>
             if (v) res else not(res)
           })
         }
@@ -30,7 +28,7 @@ case object InputSplit extends Rule("In. Split") {
           ws  = replaceA(p.ws),
           pc  = newPc,
           phi = replaceA(p.phi),
-          eb  = tests.removeIns(Set(a))
+          eb  = p.qeb.removeIns(Set(a))
         )
       }
 
@@ -42,7 +40,9 @@ case object InputSplit extends Rule("In. Split") {
           Some(Solution(or(and(    Variable(a) , s1.pre),
                            and(Not(Variable(a)), s2.pre)),
                         s1.defs ++ s2.defs,
-                        IfExpr(Variable(a), s1.term, s2.term), s1.isTrusted && s2.isTrusted))
+                        IfExpr(Variable(a), s1.term, s2.term),
+                        s1.isTrusted && s2.isTrusted
+          ))
         case _ =>
           None
       }

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

@@ -74,7 +74,7 @@ case object IntroduceRecCalls extends NormalizingRule("Introduce rec. calls") {
             as = p.as ++ (if (specifyCalls) Nil else recs.map(_._1)),
             pc = recs.map(_._2).foldLeft(p.pc)(_ merge _),
             ws = andJoin(ws ++ newWs),
-            eb = p.qeb//.filterIns(filter _)
+            eb = p.eb
           )
 
           RuleExpanded(List(newProblem))

src/main/scala/leon/synthesis/rules/unused/IntegerInequalities.scala

@@ -173,7 +173,6 @@ case object IntegerInequalities extends Rule("Integer Inequalities") {
         val subProblemxs: List[Identifier] = quotientIds ++ otherVars
         val subProblem = Problem(problem.as ++ remainderIds, problem.ws, problem.pc, subProblemFormula, subProblemxs)
 
-
         def onSuccess(sols: List[Solution]): Option[Solution] = sols match {
           case List(s @ Solution(pre, defs, term, isTrusted)) =>
             if(remainderIds.isEmpty) {