From dff5eafba6e8e8a0988eb042a91d9b61b2c4f149 Mon Sep 17 00:00:00 2001
From: Manos Koukoutos <emmanouil.koukoutos@epfl.ch>
Date: Fri, 29 Apr 2016 18:25:29 +0200
Subject: [PATCH] Fix bug in EquivalentInputs where pc got simplified under
itself
---
.../leon/synthesis/rules/EquivalentInputs.scala | 13 ++++++-------
1 file changed, 6 insertions(+), 7 deletions(-)
diff --git a/src/main/scala/leon/synthesis/rules/EquivalentInputs.scala b/src/main/scala/leon/synthesis/rules/EquivalentInputs.scala
index 74abe6721..e4562426c 100644
--- a/src/main/scala/leon/synthesis/rules/EquivalentInputs.scala
+++ b/src/main/scala/leon/synthesis/rules/EquivalentInputs.scala
@@ -9,15 +9,12 @@ import purescala.Path
import purescala.Common._
import purescala.Expressions._
import purescala.ExprOps._
-import purescala.Extractors._
import purescala.Constructors._
import purescala.Types.CaseClassType
case object EquivalentInputs extends NormalizingRule("EquivalentInputs") {
def instantiateOn(implicit hctx: SearchContext, p: Problem): Traversable[RuleInstantiation] = {
- val simplifier = Simplifiers.bestEffort(hctx, hctx.program)(_:Expr, p.pc)
-
var subst = Map.empty[Identifier, Expr]
var reverseSubst = Map.empty[Identifier, Expr]
@@ -57,12 +54,12 @@ case object EquivalentInputs extends NormalizingRule("EquivalentInputs") {
obsolete ++= equivalences.map(_._1)
free ++= unbound
- def replace(e: Expr) = simplifier(replaceFromIDs(equivalences.toMap, e))
+ def replace(e: Expr) = replaceFromIDs(equivalences.toMap, e)
subst = subst.mapValues(replace) ++ equivalences
val reverse = equivalences.toMap.flatMap { case (id, CaseClass(cct, fields)) =>
(cct.classDef.fields zip fields).map { case (vid, Variable(fieldId)) =>
- fieldId -> CaseClassSelector(cct, AsInstanceOf(Variable(id), cct), vid.id)
+ fieldId -> caseClassSelector(cct, asInstOf(Variable(id), cct), vid.id)
}
}
@@ -73,7 +70,7 @@ case object EquivalentInputs extends NormalizingRule("EquivalentInputs") {
// We could discover one equivalence, which could allow us to discover
// other equivalences: We do a fixpoint with limit 5.
- val simplifiedPath = fixpoint({ (path: Path) => discoverEquivalences(path) }, 5)(p.pc)
+ val newPC = fixpoint({ (path: Path) => discoverEquivalences(path) }, 5)(p.pc)
if (subst.nonEmpty) {
// XXX: must take place in this order!! obsolete & free is typically non-empty
@@ -88,10 +85,12 @@ case object EquivalentInputs extends NormalizingRule("EquivalentInputs") {
})
}
+ val simplifier = Simplifiers.bestEffort(hctx, hctx.program)(_:Expr, newPC)
+
val sub = p.copy(
as = newAs,
ws = replaceFromIDs(subst, p.ws),
- pc = simplifiedPath,
+ pc = newPC,
phi = simplifier(replaceFromIDs(subst, p.phi)),
eb = newBank
)
--
GitLab