From 3b9c89c3efe0fb487ab095a7d98aecd4c9d49252 Mon Sep 17 00:00:00 2001
From: Etienne Kneuss <etienne.kneuss@epfl.ch>
Date: Fri, 23 Jan 2015 17:05:36 +0100
Subject: [PATCH] Remove a == b in Equivalent Inputs as well
---
.../scala/leon/synthesis/rules/EquivalentInputs.scala | 11 +++++++++--
1 file changed, 9 insertions(+), 2 deletions(-)
diff --git a/src/main/scala/leon/synthesis/rules/EquivalentInputs.scala b/src/main/scala/leon/synthesis/rules/EquivalentInputs.scala
index 35423e656..f4da2f71a 100644
--- a/src/main/scala/leon/synthesis/rules/EquivalentInputs.scala
+++ b/src/main/scala/leon/synthesis/rules/EquivalentInputs.scala
@@ -46,7 +46,12 @@ case object EquivalentInputs extends NormalizingRule("EquivalentInputs") {
}
}
- ccSubsts.flatten
+ // Direct equivalences:
+ val directEqs = allClauses.collect {
+ case Equals(v1 @ Variable(a1), v2 @ Variable(a2)) if a1 != a2 => (v2, v1)
+ }
+
+ ccSubsts.flatten ++ directEqs
}
@@ -78,7 +83,9 @@ case object EquivalentInputs extends NormalizingRule("EquivalentInputs") {
_:Expr
)
- List(decomp(List(sub), forwardMap(subst), "Equivalent Inputs"))
+ val substString = substs.map { case (f, t) => f+" -> "+t }
+
+ List(decomp(List(sub), forwardMap(subst), "Equivalent Inputs ("+substString.mkString(", ")+")"))
} else {
Nil
}
--
GitLab