diff --git a/src/main/scala/leon/repair/rules/Focus.scala b/src/main/scala/leon/repair/rules/Focus.scala
index a881953bb9354472703660cae8bacbb542e67596..e1f2f0cbd3b994a127425bfe1b3e9da17ee9ec3d 100644
--- a/src/main/scala/leon/repair/rules/Focus.scala
+++ b/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))
diff --git a/src/main/scala/leon/synthesis/ExamplesBank.scala b/src/main/scala/leon/synthesis/ExamplesBank.scala
index 6cababe398c6159ec4e5cce721b795a751825bda..e8d831a5c60f86c02e6faa3c7f7def2d766e8220 100644
--- a/src/main/scala/leon/synthesis/ExamplesBank.scala
+++ b/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 {
diff --git a/src/main/scala/leon/synthesis/Problem.scala b/src/main/scala/leon/synthesis/Problem.scala
index 4127a28f5ebda80ecbfec4c3960b9d8fa18680b3..2a9b113e761d3aa820cd76f3cfb15c0c1ca23791 100644
--- a/src/main/scala/leon/synthesis/Problem.scala
+++ b/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,
diff --git a/src/main/scala/leon/synthesis/rules/ADTSplit.scala b/src/main/scala/leon/synthesis/rules/ADTSplit.scala
index 317f63807bf990624160e2f0cca40a332c3be879..56d28d01e82b17640a27738df7d6c9e65e6c2b73 100644
--- a/src/main/scala/leon/synthesis/rules/ADTSplit.scala
+++ b/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]()
diff --git a/src/main/scala/leon/synthesis/rules/Assert.scala b/src/main/scala/leon/synthesis/rules/Assert.scala
index 61b356415f833f493bfc9d7ebf2bbf9c17676a9a..4b29537db8118ddf70d68b0c1024a1b950650e95 100644
--- a/src/main/scala/leon/synthesis/rules/Assert.scala
+++ b/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)) =>
diff --git a/src/main/scala/leon/synthesis/rules/CEGISLike.scala b/src/main/scala/leon/synthesis/rules/CEGISLike.scala
index 3f2b23292619f6aa5b56eecf74f307b2c180289d..4a9a277b6851b25d6999436a61e0237e1be56129 100644
--- a/src/main/scala/leon/synthesis/rules/CEGISLike.scala
+++ b/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 =>
diff --git a/src/main/scala/leon/synthesis/rules/GenericTypeEqualitySplit.scala b/src/main/scala/leon/synthesis/rules/GenericTypeEqualitySplit.scala
index 6df6624bc2c54c9ef9637b9ca65ade8fe9fae977..8f1324828fc613a0bf277189b43bb583cd5a6bf5 100644
--- a/src/main/scala/leon/synthesis/rules/GenericTypeEqualitySplit.scala
+++ b/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)
diff --git a/src/main/scala/leon/synthesis/rules/IfSplit.scala b/src/main/scala/leon/synthesis/rules/IfSplit.scala
index 3d0c0d0ba406c7ba34ff83b80e4e62faabb51959..16e0f3066998b7e0fca0a63647e554b01d37ccf0 100644
--- a/src/main/scala/leon/synthesis/rules/IfSplit.scala
+++ b/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] = {
diff --git a/src/main/scala/leon/synthesis/rules/InequalitySplit.scala b/src/main/scala/leon/synthesis/rules/InequalitySplit.scala
index cacb44a4657ac15f1d1228026a521182501bb0e3..17a4c0d072c1d9a86156371565e812f11ec89314 100644
--- a/src/main/scala/leon/synthesis/rules/InequalitySplit.scala
+++ b/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
diff --git a/src/main/scala/leon/synthesis/rules/InputSplit.scala b/src/main/scala/leon/synthesis/rules/InputSplit.scala
index a14078ec808d6effd0e9fe64b689ccf14f3d251e..fbdca3ad269868dde0c8865b348066e4905b877c 100644
--- a/src/main/scala/leon/synthesis/rules/InputSplit.scala
+++ b/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
}
diff --git a/src/main/scala/leon/synthesis/rules/IntroduceRecCalls.scala b/src/main/scala/leon/synthesis/rules/IntroduceRecCalls.scala
index 22af64c189a33afe9890fa3a62d8b7c74bb1da62..8c2f14cc2e209378b03d3a3d813792f7c9b0831a 100644
--- a/src/main/scala/leon/synthesis/rules/IntroduceRecCalls.scala
+++ b/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))
diff --git a/src/main/scala/leon/synthesis/rules/unused/IntegerInequalities.scala b/src/main/scala/leon/synthesis/rules/unused/IntegerInequalities.scala
index 8ef51a44db038af0990f0a35e8bac5f154713a15..e809fe8e04bf11fa456c605030dbb458b814c9c8 100644
--- a/src/main/scala/leon/synthesis/rules/unused/IntegerInequalities.scala
+++ b/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) {