not implemented with negate

note that I had to remove the precondition of negate
checking that the type is Boolean. Some nested sub-expressions
are untyped.

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]]

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)
   }
 

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)
+  }
   
 }

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)
+
 }