From aa0700467045b374950c167923c7938218b399f9 Mon Sep 17 00:00:00 2001
From: Manos Koukoutos <emmanouil.koukoutos@epfl.ch>
Date: Thu, 7 Apr 2016 16:56:33 +0200
Subject: [PATCH] Fixes
---
src/main/scala/leon/purescala/Constructors.scala | 2 +-
src/main/scala/leon/purescala/ExprOps.scala | 12 ++++++------
.../integration/purescala/SimplifyPathsSuite.scala | 12 ++++++++++++
3 files changed, 19 insertions(+), 7 deletions(-)
diff --git a/src/main/scala/leon/purescala/Constructors.scala b/src/main/scala/leon/purescala/Constructors.scala
index fb818f1a4..b1b34a548 100644
--- a/src/main/scala/leon/purescala/Constructors.scala
+++ b/src/main/scala/leon/purescala/Constructors.scala
@@ -290,7 +290,7 @@ object Constructors {
*/
// @mk I simplified that because it seemed dangerous and unnessecary
def equality(a: Expr, b: Expr) = {
- if (a.isInstanceOf[Terminal] && !isPurelyFunctional(a) && a == b ) {
+ if (a.isInstanceOf[Terminal] && isPurelyFunctional(a) && a == b ) {
BooleanLiteral(true)
} else {
Equals(a, b)
diff --git a/src/main/scala/leon/purescala/ExprOps.scala b/src/main/scala/leon/purescala/ExprOps.scala
index 357c72861..bc926449c 100644
--- a/src/main/scala/leon/purescala/ExprOps.scala
+++ b/src/main/scala/leon/purescala/ExprOps.scala
@@ -219,7 +219,7 @@ object ExprOps extends GenTreeOps[Expr] {
case CaseClassSelector(cct, cc: CaseClass, id) =>
Some(caseClassSelector(cct, cc, id))
- case IfExpr(c, thenn, elze) if (thenn == elze) && !isPurelyFunctional(c) =>
+ case IfExpr(c, thenn, elze) if (thenn == elze) && isPurelyFunctional(c) =>
Some(thenn)
case IfExpr(c, BooleanLiteral(true), BooleanLiteral(false)) =>
@@ -333,10 +333,10 @@ object ExprOps extends GenTreeOps[Expr] {
def simplifyLets(expr: Expr) : Expr = {
def simplerLet(t: Expr) : Option[Expr] = t match {
- case letExpr @ Let(i, t: Terminal, b) if !isPurelyFunctional(t) =>
+ case letExpr @ Let(i, t: Terminal, b) if isPurelyFunctional(t) =>
Some(replaceFromIDs(Map(i -> t), b))
- case letExpr @ Let(i,e,b) if !isPurelyFunctional(e) =>
+ case letExpr @ Let(i,e,b) if isPurelyFunctional(e) =>
val occurrences = count {
case Variable(`i`) => 1
case _ => 0
@@ -350,7 +350,7 @@ object ExprOps extends GenTreeOps[Expr] {
None
}
- case LetPattern(patt, e0, body) if !isPurelyFunctional(e0) =>
+ case LetPattern(patt, e0, body) if isPurelyFunctional(e0) =>
// Will turn the match-expression with a single case into a list of lets.
// Just extra safety...
@@ -991,8 +991,8 @@ object ExprOps extends GenTreeOps[Expr] {
*/
def isPurelyFunctional(e: Expr): Boolean = {
exists {
- case _ : Error | _ : Choose | _: Hole | _: WithOracle => true
- case _ => false
+ case _ : Error | _ : Choose | _: Hole | _: WithOracle => false
+ case _ => true
}(e)
}
diff --git a/src/test/scala/leon/integration/purescala/SimplifyPathsSuite.scala b/src/test/scala/leon/integration/purescala/SimplifyPathsSuite.scala
index a560f9ca4..bd477c54a 100644
--- a/src/test/scala/leon/integration/purescala/SimplifyPathsSuite.scala
+++ b/src/test/scala/leon/integration/purescala/SimplifyPathsSuite.scala
@@ -86,4 +86,16 @@ class SimplifyPathsSuite extends LeonTestSuite {
val out = simplifyPaths(ctx, in)
assert(out === exp)
}
+
+ test("Simplify Paths 04 - error - 1") { ctx =>
+ val in = And(Error(BooleanType, ""), aV)
+ val out = simplifyPaths(ctx, in)
+ assert(out === in)
+ }
+
+ test("Simplify Paths 05 - error - 2") { ctx =>
+ val in = And(BooleanLiteral(false), Error(BooleanType, ""))
+ val out = simplifyPaths(ctx, in)
+ assert(out === BooleanLiteral(false))
+ }
}
--
GitLab