From 611f687b45c151639847ec369d324119b67a3576 Mon Sep 17 00:00:00 2001
From: Manos Koukoutos <emmanouil.koukoutos@epfl.ch>
Date: Tue, 3 May 2016 15:36:38 +0200
Subject: [PATCH] Fix Focus
1) testCondition should refer to current problem, not top-level function
2) In match, we should not add values to the eb of the problem if we
don't add variables
3) When only input variables are involved, substitute them in the
problem
---
src/main/scala/leon/repair/rules/Focus.scala | 75 +++++++++++---------
1 file changed, 43 insertions(+), 32 deletions(-)
diff --git a/src/main/scala/leon/repair/rules/Focus.scala b/src/main/scala/leon/repair/rules/Focus.scala
index 562e1845f..a77ed826a 100644
--- a/src/main/scala/leon/repair/rules/Focus.scala
+++ b/src/main/scala/leon/repair/rules/Focus.scala
@@ -4,9 +4,6 @@ package leon
package repair
package rules
-import synthesis._
-import leon.evaluators._
-
import purescala.Path
import purescala.Expressions._
import purescala.Common._
@@ -15,8 +12,11 @@ import purescala.ExprOps._
import purescala.Constructors._
import purescala.Extractors._
-import Witnesses._
+import utils.fixpoint
+import evaluators._
+import synthesis._
+import Witnesses._
import graph.AndNode
case object Focus extends PreprocessingRule("Focus") {
@@ -75,10 +75,7 @@ case object Focus extends PreprocessingRule("Focus") {
}
}
- val fdSpec = {
- val id = FreshIdentifier("res", fd.returnType)
- Let(id, fd.body.get, application(fd.postOrTrue, Seq(id.toVariable)))
- }
+
val TopLevelAnds(clauses) = p.ws
@@ -93,17 +90,15 @@ case object Focus extends PreprocessingRule("Focus") {
def ws(g: Expr) = andJoin(Guide(g) +: wss)
- def testCondition(cond: Expr) = {
- val ndSpec = postMap {
- case c if c eq cond => Some(not(cond))
- case _ => None
- }(fdSpec)
- forAllTests(ndSpec, Map(), new AngelicEvaluator(new RepairNDEvaluator(hctx, program, cond)))
+ def testCondition(guide: IfExpr) = {
+ val IfExpr(cond, thenn, elze) = guide
+ val spec = letTuple(p.xs, IfExpr(Not(cond), thenn, elze), p.phi)
+ forAllTests(spec, Map(), new AngelicEvaluator(new RepairNDEvaluator(hctx, program, cond)))
}
guides.flatMap {
case g @ IfExpr(c, thn, els) =>
- testCondition(c) match {
+ testCondition(g) match {
case Some(true) =>
val cx = FreshIdentifier("cond", BooleanType)
// Focus on condition
@@ -146,33 +141,49 @@ case object Focus extends PreprocessingRule("Focus") {
val map = mapForPattern(scrut, c.pattern)
val thisCond = matchCaseCondition(scrut, c)
+ val prevPCSoFar = pcSoFar
val cond = pcSoFar merge thisCond
pcSoFar = pcSoFar merge thisCond.negate
val subP = if (existsFailing(cond.toClause, map, evaluator)) {
- val vars = map.toSeq.map(_._1)
- // Filter tests by the path-condition
- val eb2 = qeb.filterIns(cond.toClause)
+ val vars = map.keys.toSeq
- // Augment test with the additional variables and their valuations
- val ebF: (Seq[Expr] => List[Seq[Expr]]) = { (e: Seq[Expr]) =>
- val emap = (p.as zip e).toMap
+ val (p2e, _) = patternToExpression(c.pattern, scrut.getType)
- evaluator.eval(tupleWrap(vars.map(map)), emap).result.map { r =>
- e ++ unwrapTuple(r, vars.size)
- }.toList
- }
-
- val eb3 = if (vars.nonEmpty) {
- eb2.flatMapIns(ebF)
+ val substAs = ((scrut, p2e) match {
+ case (Variable(i), _) if p.as.contains(i) => Seq(i -> p2e)
+ case (Tuple(as), Tuple(tos)) =>
+ val res = as.zip(tos) collect {
+ case (Variable(i), to) if p.as.contains(i) => i -> to
+ }
+ if (res.size == as.size) res else Nil
+ case _ => Nil
+ }).toMap
+
+ if (substAs.nonEmpty) {
+ val subst = replaceFromIDs(substAs, (_:Expr))
+ // FIXME intermediate binders??
+ val newAs = (p.as diff substAs.keys.toSeq) ++ vars
+ val newPc = (p.pc merge prevPCSoFar) map subst
+ val newWs = subst(ws(c.rhs))
+ val newPhi = subst(p.phi)
+ val eb2 = qeb.filterIns(cond.toClause)
+ val ebF: Seq[(Identifier, Expr)] => List[Seq[Expr]] = { (ins: Seq[(Identifier, Expr)]) =>
+ val eval = evaluator.eval(tupleWrap(vars map Variable), map ++ ins)
+ val insWithout = ins.collect{ case (id, v) if !substAs.contains(id) => v }
+ eval.result.map(r => insWithout ++ unwrapTuple(r, vars.size)).toList
+ }
+ val newEb = eb2.flatMapIns(ebF)
+ Some(Problem(newAs, newWs, newPc, newPhi, p.xs, newEb))
} else {
- eb2.eb
- }
+ // Filter tests by the path-condition
+ val eb2 = qeb.filterIns(cond.toClause)
- val newPc = cond withBindings vars.map(id => id -> map(id))
+ val newPc = cond withBindings vars.map(id => id -> map(id))
- Some(Problem(p.as, ws(c.rhs), p.pc merge newPc, p.phi, p.xs, eb3))
+ Some(Problem(p.as, ws(c.rhs), p.pc merge newPc, p.phi, p.xs, eb2))
+ }
} else {
None
}
--
GitLab