diff --git a/src/main/scala/leon/repair/rules/Focus.scala b/src/main/scala/leon/repair/rules/Focus.scala
index 102ab004c34fe13df3c1590cb23f728137b94ec4..50516c6dbd5c200b20eac59c6fb66edcb73fcb7d 100644
--- a/src/main/scala/leon/repair/rules/Focus.scala
+++ b/src/main/scala/leon/repair/rules/Focus.scala
@@ -24,12 +24,18 @@ import purescala.Extractors._
import Witnesses._
import solvers._
+import graph.AndNode
-case object Focus extends Rule("Focus") {
+case object Focus extends PreprocessingRule("Focus") {
def instantiateOn(implicit hctx: SearchContext, p: Problem): Traversable[RuleInstantiation] = {
- if (hctx.searchDepth > 0) {
- return Nil
+ hctx.parentNode match {
+ case Some(an: AndNode) if an.ri.rule == Focus =>
+ // We proceed as usual
+ case Some(_) =>
+ return None;
+ case _ =>
+
}
val fd = hctx.ci.fd
@@ -42,7 +48,7 @@ case object Focus extends Rule("Focus") {
// - returns Some(true) if for all tests e evaluates to true
// - returns Some(false) if for all tests e evaluates to false
// - returns None otherwise
- def forAllTestsOf(p: Problem)(e: Expr, env: Map[Identifier, Expr], evaluator: Evaluator): Option[Boolean] = {
+ def forAllTests(e: Expr, env: Map[Identifier, Expr], evaluator: Evaluator): Option[Boolean] = {
var soFar: Option[Boolean] = None
p.tb.invalids.foreach { ex =>
@@ -73,151 +79,128 @@ case object Focus extends Rule("Focus") {
)
}
- def focus(p: Problem): Traversable[RuleInstantiation] = {
- val faTests = forAllTestsOf(p) _
+ val TopLevelAnds(clauses) = p.ws
- val TopLevelAnds(clauses) = p.ws
+ val guides = clauses.collect {
+ case Guide(expr) => expr
+ }
- val guides = clauses.collect {
- case Guide(expr) => expr
- }
+ val wss = clauses.filter {
+ case _: Guide => false
+ case _ => true
+ }
- val wss = clauses.filter {
- case _: Guide => false
- case _ => true
- }
+ def ws(g: Expr) = andJoin(Guide(g) +: wss)
- def ws(g: Expr) = andJoin(Guide(g) +: wss)
+ def testCondition(cond: Expr) = {
+ val ndSpec = postMap {
+ case c if c eq cond => Some(not(cond)) // Use reference equality
+ case _ => None
+ }(fdSpec)
- def testCondition(cond: Expr) = {
- val ndSpec = postMap {
- case c if c eq cond => Some(not(cond)) // Use reference equality
- case _ => None
- }(fdSpec)
+ forAllTests(ndSpec, Map(), new RepairNDEvaluator(ctx, program, fd, cond))
+ }
- faTests(ndSpec, Map(), new RepairNDEvaluator(ctx, program, fd, cond))
- }
+ guides.flatMap {
+ case IfExpr(c, thn, els) =>
+ testCondition(c) match {
+ 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.tb.stripOuts)
- guides.flatMap {
- case IfExpr(c, thn, els) =>
- testCondition(c) match {
- 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.tb.stripOuts)
-
- Some(decomp(List(np), termWrap(IfExpr(_, thn, els)), s"Focus on if-cond '$c'")(p))
-
- case _ =>
- // Try to focus on branches
- faTests(c, Map(), evaluator) match {
- case Some(true) =>
- val np = Problem(p.as, ws(thn), and(p.pc, c), p.phi, p.xs, p.tbOps.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), and(p.pc, not(c)), p.phi, p.xs, p.tbOps.filterIns(not(c)))
-
- Some(decomp(List(np), termWrap(IfExpr(c, thn, _), not(c)), s"Focus on if-else")(p))
- case None =>
- // We cannot focus any further
- None
- }
- }
+ Some(decomp(List(np), termWrap(IfExpr(_, thn, els)), s"Focus on if-cond '$c'")(p))
- case MatchExpr(scrut, cases) =>
- var res: Option[Traversable[RuleInstantiation]] = None
-
- var pcSoFar: Seq[Expr] = Nil
+ case _ =>
+ // Try to focus on branches
+ forAllTests(c, Map(), evaluator) match {
+ case Some(true) =>
+ val np = Problem(p.as, ws(thn), and(p.pc, c), p.phi, p.xs, p.tbOps.filterIns(c))
- for (c <- cases if res.isEmpty) {
- val map = mapForPattern(scrut, c.pattern)
+ 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), and(p.pc, not(c)), p.phi, p.xs, p.tbOps.filterIns(not(c)))
- val thisCond = matchCaseCondition(scrut, c)
- val cond = andJoin(pcSoFar :+ thisCond)
- pcSoFar = pcSoFar :+ not(thisCond)
+ Some(decomp(List(np), termWrap(IfExpr(c, thn, _), not(c)), s"Focus on if-else")(p))
+ case None =>
+ // We cannot focus any further
+ None
+ }
+ }
- // thisCond here is safe, because we focus we now that all tests have been false so far
- faTests(thisCond, map, evaluator) match {
- case Some(true) =>
+ case MatchExpr(scrut, cases) =>
+ var res: Option[Traversable[RuleInstantiation]] = None
- val vars = map.toSeq.map(_._1)
+ var pcSoFar: Seq[Expr] = Nil
- // Filter tests by the path-condition
- val tb2 = p.tbOps.filterIns(cond)
+ for (c <- cases if res.isEmpty) {
+ val map = mapForPattern(scrut, c.pattern)
- // Augment test with the additional variables and their valuations
- val tbF: (Seq[Expr] => List[Seq[Expr]]) = { (e: Seq[Expr]) =>
- val emap = (p.as zip e).toMap
+ val thisCond = matchCaseCondition(scrut, c)
+ val cond = andJoin(pcSoFar :+ thisCond)
+ pcSoFar = pcSoFar :+ not(thisCond)
- evaluator.eval(tupleWrap(vars.map(map)), emap).result.map { r =>
- e ++ unwrapTuple(r, vars.size)
- }.toList
- }
+ // thisCond here is safe, because we focus we now that all tests have been false so far
+ forAllTests(thisCond, map, evaluator) match {
+ case Some(true) =>
- val tb3 = if (vars.nonEmpty) {
- tb2.mapIns(tbF)
- } else {
- tb2
- }
+ val vars = map.toSeq.map(_._1)
- val newPc = andJoin(cond +: vars.map { id => equality(id.toVariable, map(id)) })
+ // Filter tests by the path-condition
+ val tb2 = p.tbOps.filterIns(cond)
- val np = Problem(p.as ++ vars, ws(c.rhs), and(p.pc, newPc), p.phi, p.xs, tb3)
+ // Augment test with the additional variables and their valuations
+ val tbF: (Seq[Expr] => List[Seq[Expr]]) = { (e: Seq[Expr]) =>
+ val emap = (p.as zip e).toMap
- res = Some(
- Some(
- decomp(List(np), termWrap(x => MatchExpr(scrut, cases.map {
- case `c` => c.copy(rhs = x)
- case c2 => c2
- }), cond), s"Focus on match-case '${c.pattern}'")(p)
- )
- )
+ evaluator.eval(tupleWrap(vars.map(map)), emap).result.map { r =>
+ e ++ unwrapTuple(r, vars.size)
+ }.toList
+ }
- case Some(false) =>
- // continue until next case
- case None =>
- res = Some(Nil)
- }
- }
+ val tb3 = if (vars.nonEmpty) {
+ tb2.mapIns(tbF)
+ } else {
+ tb2
+ }
- res.getOrElse(Nil)
+ val newPc = andJoin(cond +: vars.map { id => equality(id.toVariable, map(id)) })
+ val np = Problem(p.as ++ vars, ws(c.rhs), and(p.pc, newPc), p.phi, p.xs, tb3)
- case Let(id, value, body) =>
- val tbF: (Seq[Expr] => List[Seq[Expr]]) = { (e: Seq[Expr]) =>
- val map = (p.as zip e).toMap
+ res = Some(
+ Some(
+ decomp(List(np), termWrap(x => MatchExpr(scrut, cases.map {
+ case `c` => c.copy(rhs = x)
+ case c2 => c2
+ }), cond), s"Focus on match-case '${c.pattern}'")(p)
+ )
+ )
- evaluator.eval(value, map).result.map { r =>
- e :+ r
- }.toList
+ case Some(false) =>
+ // continue until next case
+ case None =>
+ res = Some(Nil)
}
+ }
- val np = Problem(p.as :+ id, ws(body), and(p.pc, equality(id.toVariable, value)), p.phi, p.xs, p.tb.mapIns(tbF))
+ res.getOrElse(Nil)
- Some(decomp(List(np), termWrap(Let(id, value, _)), s"Focus on let-body")(p))
- case _ => None
- }
- }
+ case Let(id, value, body) =>
+ val tbF: (Seq[Expr] => List[Seq[Expr]]) = { (e: Seq[Expr]) =>
+ val map = (p.as zip e).toMap
- def focusRec(is: Traversable[RuleInstantiation]): Traversable[RuleInstantiation] = {
- val res = is.flatMap { ri =>
- ri.apply(hctx) match {
- case RuleExpanded(subs) =>
- subs.flatMap(focus)
- case _ =>
- Nil
+ evaluator.eval(value, map).result.map { r =>
+ e :+ r
+ }.toList
}
- }
- if (res.isEmpty) {
- is
- } else {
- res
- }
- }
+ val np = Problem(p.as :+ id, ws(body), and(p.pc, equality(id.toVariable, value)), p.phi, p.xs, p.tb.mapIns(tbF))
- focusRec(focus(p))
+ Some(decomp(List(np), termWrap(Let(id, value, _)), s"Focus on let-body")(p))
+
+ case _ => None
+ }
}
}