From 191fa1d05a5c3295fa3a5cdb935250866b312458 Mon Sep 17 00:00:00 2001
From: Philippe Suter <philippe.suter@gmail.com>
Date: Thu, 15 Nov 2012 12:28:28 +0100
Subject: [PATCH] Fixed horrible bug that made a && false == a...
---
src/main/scala/leon/purescala/Trees.scala | 45 ++++++++++++++-----
.../{TreeOpsTest.scala => TreeOpsTests.scala} | 2 +-
.../scala/leon/test/purescala/TreeTests.scala | 36 +++++++++++++++
3 files changed, 70 insertions(+), 13 deletions(-)
rename src/test/scala/leon/test/purescala/{TreeOpsTest.scala => TreeOpsTests.scala} (94%)
create mode 100644 src/test/scala/leon/test/purescala/TreeTests.scala
diff --git a/src/main/scala/leon/purescala/Trees.scala b/src/main/scala/leon/purescala/Trees.scala
index 74925bce8..250dd8ad2 100644
--- a/src/main/scala/leon/purescala/Trees.scala
+++ b/src/main/scala/leon/purescala/Trees.scala
@@ -174,18 +174,25 @@ object Trees {
/* Propositional logic */
object And {
- def apply(l: Expr, r: Expr) : Expr = (l,r) match {
- case (BooleanLiteral(false),_) => BooleanLiteral(false)
- case (BooleanLiteral(true),_) => r
- case (_,BooleanLiteral(true)) => l
- case _ => new And(Seq(l,r))
- }
+ def apply(l: Expr, r: Expr) : Expr = And(Seq(l, r))
+
def apply(exprs: Seq[Expr]) : Expr = {
- val simpler = exprs.flatMap(_ match {
+ val flat = exprs.flatMap(_ match {
case And(es) => es
case o => Seq(o)
- }).takeWhile(_ != BooleanLiteral(false)).filter(_ != BooleanLiteral(true))
- if(simpler.isEmpty) BooleanLiteral(true) else new And(simpler)
+ })
+
+ var stop = false
+ val simpler = for(e <- flat if !stop && e != BooleanLiteral(true)) yield {
+ if(e == BooleanLiteral(false)) stop = true
+ e
+ }
+
+ simpler match {
+ case Seq() => BooleanLiteral(true)
+ case Seq(x) => x
+ case _ => new And(simpler)
+ }
}
def unapply(and: And) : Option[Seq[Expr]] =
@@ -195,6 +202,8 @@ object Trees {
class And private (val exprs: Seq[Expr]) extends Expr with FixedType {
val fixedType = BooleanType
+ assert(exprs.size >= 2)
+
override def equals(that: Any): Boolean = (that != null) && (that match {
case t: And => t.exprs == exprs
case _ => false
@@ -211,12 +220,22 @@ object Trees {
case _ => new Or(Seq(l,r))
}
def apply(exprs: Seq[Expr]) : Expr = {
- val simpler = exprs.flatMap(_ match {
+ val flat = exprs.flatMap(_ match {
case Or(es) => es
case o => Seq(o)
- }).takeWhile(_ != BooleanLiteral(true)).filter(_ != BooleanLiteral(false))
+ })
+
+ var stop = false
+ val simpler = for(e <- flat if !stop && e != BooleanLiteral(false)) yield {
+ if(e == BooleanLiteral(true)) stop = true
+ e
+ }
- if(simpler.isEmpty) BooleanLiteral(false) else new Or(simpler)
+ simpler match {
+ case Seq() => BooleanLiteral(false)
+ case Seq(x) => x
+ case _ => new Or(simpler)
+ }
}
def unapply(or: Or) : Option[Seq[Expr]] =
@@ -226,6 +245,8 @@ object Trees {
class Or(val exprs: Seq[Expr]) extends Expr with FixedType {
val fixedType = BooleanType
+ assert(exprs.size >= 2)
+
override def equals(that: Any): Boolean = (that != null) && (that match {
case t: Or => t.exprs == exprs
case _ => false
diff --git a/src/test/scala/leon/test/purescala/TreeOpsTest.scala b/src/test/scala/leon/test/purescala/TreeOpsTests.scala
similarity index 94%
rename from src/test/scala/leon/test/purescala/TreeOpsTest.scala
rename to src/test/scala/leon/test/purescala/TreeOpsTests.scala
index a0ee0fdf3..a729f00d0 100644
--- a/src/test/scala/leon/test/purescala/TreeOpsTest.scala
+++ b/src/test/scala/leon/test/purescala/TreeOpsTests.scala
@@ -8,7 +8,7 @@ import leon.SilentReporter
import org.scalatest.FunSuite
-class TreeOpsTest extends FunSuite {
+class TreeOpsTests extends FunSuite {
private val silentReporter = new SilentReporter
private val emptyProgram = Program(
diff --git a/src/test/scala/leon/test/purescala/TreeTests.scala b/src/test/scala/leon/test/purescala/TreeTests.scala
new file mode 100644
index 000000000..3ca418ec5
--- /dev/null
+++ b/src/test/scala/leon/test/purescala/TreeTests.scala
@@ -0,0 +1,36 @@
+package leon.test.purescala
+
+import leon.purescala.Common._
+import leon.purescala.Definitions._
+import leon.purescala.Trees._
+import leon.purescala.TypeTrees._
+
+import org.scalatest.FunSuite
+
+class TreeTests extends FunSuite {
+
+ test("And- and Or- simplifications") {
+ val x = Variable(FreshIdentifier("x").setType(BooleanType))
+ val t = BooleanLiteral(true)
+ val f = BooleanLiteral(false)
+
+ def and(es : Expr*) : Expr = And(Seq(es : _*))
+ def or(es : Expr*) : Expr = Or(Seq(es : _*))
+
+ assert(and(x, and(x, x), x) === and(x, x, x, x))
+ assert(and(x, t, x, t) === and(x, x))
+ assert(and(x, t, f, x) === and(x, f))
+ assert(and(x) === x)
+ assert(and() === t)
+ assert(and(t, t) === t)
+ assert(and(f) === f)
+
+ assert(or(x, or(x, x), x) === or(x, x, x, x))
+ assert(or(x, f, x, f) === or(x, x))
+ assert(or(x, f, t, x) === or(x, t))
+ assert(or(x) === x)
+ assert(or() === f)
+ assert(or(f, f) === f)
+ assert(or(t) === t)
+ }
+}
--
GitLab