From 9bac5b9c35d775db7d33834d9ba792a9be7b97ba Mon Sep 17 00:00:00 2001
From: Manos Koukoutos <emmanouil.koukoutos@epfl.ch>
Date: Fri, 29 Apr 2016 19:28:48 +0200
Subject: [PATCH] More simplification here
---
.../scala/leon/synthesis/rules/EquivalentInputs.scala | 8 +++++---
1 file changed, 5 insertions(+), 3 deletions(-)
diff --git a/src/main/scala/leon/synthesis/rules/EquivalentInputs.scala b/src/main/scala/leon/synthesis/rules/EquivalentInputs.scala
index e4562426c..609b98f50 100644
--- a/src/main/scala/leon/synthesis/rules/EquivalentInputs.scala
+++ b/src/main/scala/leon/synthesis/rules/EquivalentInputs.scala
@@ -15,6 +15,8 @@ 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)
+
var subst = Map.empty[Identifier, Expr]
var reverseSubst = Map.empty[Identifier, Expr]
@@ -54,7 +56,7 @@ case object EquivalentInputs extends NormalizingRule("EquivalentInputs") {
obsolete ++= equivalences.map(_._1)
free ++= unbound
- def replace(e: Expr) = replaceFromIDs(equivalences.toMap, e)
+ def replace(e: Expr) = simplifier(replaceFromIDs(equivalences.toMap, e))
subst = subst.mapValues(replace) ++ equivalences
val reverse = equivalences.toMap.flatMap { case (id, CaseClass(cct, fields)) =>
@@ -85,13 +87,13 @@ case object EquivalentInputs extends NormalizingRule("EquivalentInputs") {
})
}
- val simplifier = Simplifiers.bestEffort(hctx, hctx.program)(_:Expr, newPC)
+ val simplifierWithNewPC = Simplifiers.bestEffort(hctx, hctx.program)(_:Expr, newPC)
val sub = p.copy(
as = newAs,
ws = replaceFromIDs(subst, p.ws),
pc = newPC,
- phi = simplifier(replaceFromIDs(subst, p.phi)),
+ phi = simplifierWithNewPC(replaceFromIDs(subst, p.phi)),
eb = newBank
)
--
GitLab