From 8b20aa8ee0c5ac24094d25e0710f4b0705014c03 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Mika=C3=ABl=20Mayer?= <mikael.mayer@epfl.ch>
Date: Tue, 26 Jan 2016 17:29:22 +0100
Subject: [PATCH] New tests for function canBeHomomorphic + corrected
implementation.
---
src/main/scala/leon/purescala/ExprOps.scala | 5 ++++-
.../leon/integration/purescala/ExprOpsSuite.scala | 12 ++++++++++++
2 files changed, 16 insertions(+), 1 deletion(-)
diff --git a/src/main/scala/leon/purescala/ExprOps.scala b/src/main/scala/leon/purescala/ExprOps.scala
index 6899a422e..113aec1e1 100644
--- a/src/main/scala/leon/purescala/ExprOps.scala
+++ b/src/main/scala/leon/purescala/ExprOps.scala
@@ -1537,6 +1537,9 @@ object ExprOps {
/** Checks whether two expressions can be homomorphic and returns the corresponding mapping */
def canBeHomomorphic(t1: Expr, t2: Expr): Option[Map[Identifier, Identifier]] = {
+ val freeT1Variables = ExprOps.variablesOf(t1)
+ val freeT2Variables = ExprOps.variablesOf(t2)
+
def mergeContexts(a: Option[Map[Identifier, Identifier]], b: =>Option[Map[Identifier, Identifier]]) = a match {
case Some(m) =>
b match {
@@ -1570,7 +1573,7 @@ object ExprOps {
def idHomo(i1: Identifier, i2: Identifier): Option[Map[Identifier, Identifier]] = {
- Some(Map(i1 -> i2))
+ if(!(freeT1Variables(i1) || freeT2Variables(i2)) || i1 == i2) Some(Map(i1 -> i2)) else None
}
def fdHomo(fd1: FunDef, fd2: FunDef): Option[Map[Identifier, Identifier]] = {
diff --git a/src/test/scala/leon/integration/purescala/ExprOpsSuite.scala b/src/test/scala/leon/integration/purescala/ExprOpsSuite.scala
index 17260f7e5..2512f87ce 100644
--- a/src/test/scala/leon/integration/purescala/ExprOpsSuite.scala
+++ b/src/test/scala/leon/integration/purescala/ExprOpsSuite.scala
@@ -101,5 +101,17 @@ class ExprOpsSuite extends LeonTestSuiteWithProgram with helpers.ExpressionsDSL
assert(isSubtypeOf(simplestValue(act).getType, act))
assert(simplestValue(cct).getType == cct)
}
+
+ test("canBeHomomorphic") { implicit fix =>
+ import leon.purescala.ExprOps.canBeHomomorphic
+ import leon.purescala.Types._
+ import leon.purescala.Definitions._
+ val d = FreshIdentifier("x", IntegerType)
+ val e = FreshIdentifier("y", IntegerType)
+ assert(canBeHomomorphic(Variable(d), Variable(e)).isEmpty)
+ val l1 = Lambda(Seq(ValDef(d)), Variable(d))
+ val l2 = Lambda(Seq(ValDef(e)), Variable(e))
+ assert(canBeHomomorphic(l1, l2).nonEmpty)
+ }
}
--
GitLab