From b97c7e5eb547d8e02a302227636b47c808a7ddca Mon Sep 17 00:00:00 2001
From: Manos Koukoutos <emmanouil.koukoutos@epfl.ch>
Date: Tue, 3 May 2016 17:46:33 +0200
Subject: [PATCH] Revert "Focus removes input variables to not depend on
EquivalentInputs"
This reverts commit 4da35a7a3a5d0d0f085d5d0448520149cf323cdc.
---
src/main/scala/leon/repair/rules/Focus.scala | 71 ++++++--------------
1 file changed, 20 insertions(+), 51 deletions(-)
diff --git a/src/main/scala/leon/repair/rules/Focus.scala b/src/main/scala/leon/repair/rules/Focus.scala
index a4bf840de..562e1845f 100644
--- a/src/main/scala/leon/repair/rules/Focus.scala
+++ b/src/main/scala/leon/repair/rules/Focus.scala
@@ -4,6 +4,9 @@ package leon
package repair
package rules
+import synthesis._
+import leon.evaluators._
+
import purescala.Path
import purescala.Expressions._
import purescala.Common._
@@ -12,11 +15,8 @@ import purescala.ExprOps._
import purescala.Constructors._
import purescala.Extractors._
-import utils.fixpoint
-import evaluators._
-
-import synthesis._
import Witnesses._
+
import graph.AndNode
case object Focus extends PreprocessingRule("Focus") {
@@ -146,64 +146,33 @@ 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)
- val (p2e, _) = patternToExpression(c.pattern, scrut.getType)
-
- 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
- }).toMap
-
- if (substAs.nonEmpty) {
- val subst: Expr => Expr = { e =>
- replaceFromIDs(substAs, e)
- }
- // 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).removeIns(substAs.keySet)
- val ebF: Seq[Expr] => List[Seq[Expr]] = { (ins: Seq[Expr]) =>
- val eval = evaluator.eval(tupleWrap(vars map Variable), p.as.zip(ins).toMap ++ map)
- eval.result.map( r => ins ++ unwrapTuple(r, vars.size)).toList
- }
- val newEb = eb2 flatMapIns ebF
- Some(Problem(newAs, newWs, newPc, newPhi, p.xs, newEb))
- } else {
- // Filter tests by the path-condition
- val eb2 = qeb.filterIns(cond.toClause)
+ // Filter tests by the path-condition
+ 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]) =>
- val emap = (p.as zip e).toMap
+ // 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
- evaluator.eval(tupleWrap(vars.map(map)), emap).result.map { r =>
- e ++ unwrapTuple(r, vars.size)
- }.toList
- }
+ evaluator.eval(tupleWrap(vars.map(map)), emap).result.map { r =>
+ e ++ unwrapTuple(r, vars.size)
+ }.toList
+ }
- val eb3 = if (vars.nonEmpty) {
- eb2.flatMapIns(ebF)
- } else {
- eb2.eb
- }
+ val eb3 = if (vars.nonEmpty) {
+ eb2.flatMapIns(ebF)
+ } else {
+ eb2.eb
+ }
- 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, eb3))
} else {
None
}
--
GitLab