diff --git a/src/main/scala/leon/purescala/Constructors.scala b/src/main/scala/leon/purescala/Constructors.scala
index 5b6147c055672096f1e68a8718b6ba07013bf6d9..98379c079f8bc36e6aa8b6f89c1e774995c9cfc2 100644
--- a/src/main/scala/leon/purescala/Constructors.scala
+++ b/src/main/scala/leon/purescala/Constructors.scala
@@ -235,11 +235,7 @@ object Constructors {
/** $encodingof simplified `!`-expressions .
* @see [[purescala.Expressions.Not Not]]
*/
- def not(e: Expr): Expr = e match {
- case Not(e) => e
- case BooleanLiteral(v) => BooleanLiteral(!v)
- case _ => Not(e)
- }
+ def not(e: Expr): Expr = negate(e)
/** $encodingof simplified `... ==> ...` (implication)
* @see [[purescala.Expressions.Implies Implies]]
diff --git a/src/main/scala/leon/purescala/ExprOps.scala b/src/main/scala/leon/purescala/ExprOps.scala
index 918fa363c0e64c32916922ae012e09940441bb15..eda6e8d9de4d710a1ccb9742d9296229955e5447 100644
--- a/src/main/scala/leon/purescala/ExprOps.scala
+++ b/src/main/scala/leon/purescala/ExprOps.scala
@@ -349,9 +349,9 @@ object ExprOps {
}(e)
}
- /** Computes the negation of a boolean formula in Negation Normal Form. */
+ /** Computes the negation of a boolean formula, with some simplifications. */
def negate(expr: Expr) : Expr = {
- require(expr.getType == BooleanType)
+ //require(expr.getType == BooleanType)
(expr match {
case Let(i,b,e) => Let(i,b,negate(e))
case Not(e) => e
@@ -362,9 +362,9 @@ object ExprOps {
case LessEquals(e1,e2) => GreaterThan(e1,e2)
case GreaterThan(e1,e2) => LessEquals(e1,e2)
case GreaterEquals(e1,e2) => LessThan(e1,e2)
- case i @ IfExpr(c,e1,e2) => IfExpr(c, negate(e1), negate(e2))
+ case IfExpr(c,e1,e2) => IfExpr(c, negate(e1), negate(e2))
case BooleanLiteral(b) => BooleanLiteral(!b)
- case _ => Not(expr)
+ case e => Not(e)
}).setPos(expr)
}
diff --git a/src/unit-test/scala/leon/purescala/ExprOpsSuite.scala b/src/unit-test/scala/leon/purescala/ExprOpsSuite.scala
index 91e14f1d58fd4dd48623ef66e7b286522f79f793..d929ce295daf6ff12c257bea272c6ea0726cc19a 100644
--- a/src/unit-test/scala/leon/purescala/ExprOpsSuite.scala
+++ b/src/unit-test/scala/leon/purescala/ExprOpsSuite.scala
@@ -169,9 +169,6 @@ class ExprOpsSuite extends LeonTestSuite with WithLikelyEq with ExpressionsBuild
}
- val xs = Set(xId, yId)
- val as = Set(aId, bId)
-
def checkSameExpr(e1: Expr, e2: Expr, vs: Set[Identifier]) {
assert( //this outer assert should not be needed because of the nested one
LikelyEq(e1, e2, vs, BooleanLiteral(true), (e1, e2) => {assert(e1 === e2); true})
@@ -179,37 +176,37 @@ class ExprOpsSuite extends LeonTestSuite with WithLikelyEq with ExpressionsBuild
}
test("simplifyArithmetic") {
- val e1 = Plus(InfiniteIntegerLiteral(3), InfiniteIntegerLiteral(2))
+ val e1 = Plus(i(3), i(2))
checkSameExpr(e1, simplifyArithmetic(e1), Set())
- val e2 = Plus(x, Plus(InfiniteIntegerLiteral(3), InfiniteIntegerLiteral(2)))
- checkSameExpr(e2, simplifyArithmetic(e2), Set(xId))
+ val e2 = Plus(a, Plus(i(3), i(2)))
+ checkSameExpr(e2, simplifyArithmetic(e2), Set(aId))
- val e3 = Minus(InfiniteIntegerLiteral(3), InfiniteIntegerLiteral(2))
+ val e3 = Minus(i(3), i(2))
checkSameExpr(e3, simplifyArithmetic(e3), Set())
- val e4 = Plus(x, Minus(InfiniteIntegerLiteral(3), InfiniteIntegerLiteral(2)))
- checkSameExpr(e4, simplifyArithmetic(e4), Set(xId))
- val e5 = Plus(x, Minus(x, InfiniteIntegerLiteral(2)))
- checkSameExpr(e5, simplifyArithmetic(e5), Set(xId))
+ val e4 = Plus(a, Minus(i(3), i(2)))
+ checkSameExpr(e4, simplifyArithmetic(e4), Set(aId))
+ val e5 = Plus(a, Minus(a, i(2)))
+ checkSameExpr(e5, simplifyArithmetic(e5), Set(aId))
- val e6 = Times(InfiniteIntegerLiteral(9), Plus(Division(x, InfiniteIntegerLiteral(3)), Division(x, InfiniteIntegerLiteral(6))))
- checkSameExpr(e6, simplifyArithmetic(e6), Set(xId))
+ val e6 = Times(i(9), Plus(Division(a, i(3)), Division(a, i(6))))
+ checkSameExpr(e6, simplifyArithmetic(e6), Set(aId))
}
test("expandAndSimplifyArithmetic") {
- val e1 = Plus(InfiniteIntegerLiteral(3), InfiniteIntegerLiteral(2))
+ val e1 = Plus(i(3), i(2))
checkSameExpr(e1, expandAndSimplifyArithmetic(e1), Set())
- val e2 = Plus(x, Plus(InfiniteIntegerLiteral(3), InfiniteIntegerLiteral(2)))
- checkSameExpr(e2, expandAndSimplifyArithmetic(e2), Set(xId))
+ val e2 = Plus(a, Plus(i(3), i(2)))
+ checkSameExpr(e2, expandAndSimplifyArithmetic(e2), Set(aId))
- val e3 = Minus(InfiniteIntegerLiteral(3), InfiniteIntegerLiteral(2))
+ val e3 = Minus(i(3), i(2))
checkSameExpr(e3, expandAndSimplifyArithmetic(e3), Set())
- val e4 = Plus(x, Minus(InfiniteIntegerLiteral(3), InfiniteIntegerLiteral(2)))
- checkSameExpr(e4, expandAndSimplifyArithmetic(e4), Set(xId))
- val e5 = Plus(x, Minus(x, InfiniteIntegerLiteral(2)))
- checkSameExpr(e5, expandAndSimplifyArithmetic(e5), Set(xId))
+ val e4 = Plus(a, Minus(i(3), i(2)))
+ checkSameExpr(e4, expandAndSimplifyArithmetic(e4), Set(aId))
+ val e5 = Plus(a, Minus(a, i(2)))
+ checkSameExpr(e5, expandAndSimplifyArithmetic(e5), Set(aId))
- val e6 = Times(InfiniteIntegerLiteral(9), Plus(Division(x, InfiniteIntegerLiteral(3)), Division(x, InfiniteIntegerLiteral(6))))
- checkSameExpr(e6, expandAndSimplifyArithmetic(e6), Set(xId))
+ val e6 = Times(i(9), Plus(Division(a, i(3)), Division(a, i(6))))
+ checkSameExpr(e6, expandAndSimplifyArithmetic(e6), Set(aId))
}
test("extractEquals") {
@@ -241,7 +238,7 @@ class ExprOpsSuite extends LeonTestSuite with WithLikelyEq with ExpressionsBuild
}
test("pre and post traversal") {
- val expr = Plus(InfiniteIntegerLiteral(1), Minus(InfiniteIntegerLiteral(2), InfiniteIntegerLiteral(3)))
+ val expr = Plus(i(1), Minus(i(2), i(3)))
var res = ""
def f(e: Expr): Unit = e match {
case InfiniteIntegerLiteral(i) => res += i
@@ -258,19 +255,35 @@ class ExprOpsSuite extends LeonTestSuite with WithLikelyEq with ExpressionsBuild
}
test("pre- and postMap") {
- val expr = Plus(InfiniteIntegerLiteral(1), Minus(InfiniteIntegerLiteral(2), InfiniteIntegerLiteral(3)))
+ val expr = Plus(i(1), Minus(i(2), i(3)))
def op(e : Expr ) = e match {
- case Minus(InfiniteIntegerLiteral(two), e2) if two == BigInt(2) => Some(InfiniteIntegerLiteral(2))
- case InfiniteIntegerLiteral(one) if one == BigInt(1) => Some(InfiniteIntegerLiteral(2))
- case InfiniteIntegerLiteral(two) if two == BigInt(2) => Some(InfiniteIntegerLiteral(42))
+ case Minus(InfiniteIntegerLiteral(two), e2) if two == BigInt(2) => Some(i(2))
+ case InfiniteIntegerLiteral(one) if one == BigInt(1) => Some(i(2))
+ case InfiniteIntegerLiteral(two) if two == BigInt(2) => Some(i(42))
case _ => None
}
- assert( preMap(op, false)(expr) == Plus(InfiniteIntegerLiteral(2), InfiniteIntegerLiteral(2)) )
- assert( preMap(op, true )(expr) == Plus(InfiniteIntegerLiteral(42), InfiniteIntegerLiteral(42)) )
- assert( postMap(op, false)(expr) == Plus(InfiniteIntegerLiteral(2), Minus(InfiniteIntegerLiteral(42), InfiniteIntegerLiteral(3))) )
- assert( postMap(op, true)(expr) == Plus(InfiniteIntegerLiteral(42), Minus(InfiniteIntegerLiteral(42), InfiniteIntegerLiteral(3))) )
+ assert( preMap(op, false)(expr) == Plus(i(2), i(2)) )
+ assert( preMap(op, true )(expr) == Plus(i(42), i(42)) )
+ assert( postMap(op, false)(expr) == Plus(i(2), Minus(i(42), i(3))) )
+ assert( postMap(op, true)(expr) == Plus(i(42), Minus(i(42), i(3))) )
}
+
+
+ test("negate of literal returns the correct literal") {
+ assert(negate(BooleanLiteral(true)) === BooleanLiteral(false))
+ assert(negate(BooleanLiteral(false)) === BooleanLiteral(true))
+ }
+
+ test("negate of a variable simply wraps it with a Not node") {
+ assert(negate(p) === Not(p))
+ assert(negate(q) === Not(q))
+ }
+
+ test("negate of a negated variable simply returns the variable") {
+ assert(negate(Not(p)) === p)
+ assert(negate(Not(q)) === q)
+ }
}
diff --git a/src/unit-test/scala/leon/purescala/ExpressionsBuilder.scala b/src/unit-test/scala/leon/purescala/ExpressionsBuilder.scala
index b634dd686d3119d3bf1b47af9f3bc7a3da9b8d39..c49636697589aff9ecaee6f9af8f779ccac1522b 100644
--- a/src/unit-test/scala/leon/purescala/ExpressionsBuilder.scala
+++ b/src/unit-test/scala/leon/purescala/ExpressionsBuilder.scala
@@ -8,16 +8,18 @@ import Common._
trait ExpressionsBuilder {
- protected def i(x: Int) = InfiniteIntegerLiteral(x)
+ protected def i(i: Int) = InfiniteIntegerLiteral(i)
+ protected def r(x: Double) = RealLiteral(BigDecimal(x))
protected def v(name: String, tpe: TypeTree = IntegerType) = Variable(FreshIdentifier(name, tpe))
- protected val xId = FreshIdentifier("x", IntegerType)
+ protected val xId = FreshIdentifier("x", RealType)
protected val x = Variable(xId)
- protected val yId = FreshIdentifier("y", IntegerType)
+ protected val yId = FreshIdentifier("y", RealType)
protected val y = Variable(yId)
- protected val zId = FreshIdentifier("z", IntegerType)
+ protected val zId = FreshIdentifier("z", RealType)
protected val z = Variable(zId)
+
protected val aId = FreshIdentifier("a", IntegerType)
protected val a = Variable(aId)
protected val bId = FreshIdentifier("b", IntegerType)
@@ -25,10 +27,19 @@ trait ExpressionsBuilder {
protected val cId = FreshIdentifier("c", IntegerType)
protected val c = Variable(cId)
+ protected val mId = FreshIdentifier("m", IntegerType)
+ protected val m = Variable(mId)
+ protected val nId = FreshIdentifier("n", IntegerType)
+ protected val n = Variable(nId)
+ protected val kId = FreshIdentifier("k", IntegerType)
+ protected val k = Variable(kId)
+
+
protected val pId = FreshIdentifier("p", BooleanType)
protected val p = Variable(pId)
protected val qId = FreshIdentifier("q", BooleanType)
protected val q = Variable(qId)
protected val rId = FreshIdentifier("r", BooleanType)
protected val r = Variable(rId)
+
}