From 7aa6c4c425cc44c627d4408633fe5c753aec774e Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?R=C3=A9gis=20Blanc?= <regwblanc@gmail.com>
Date: Thu, 29 Nov 2012 16:29:43 +0100
Subject: [PATCH] tests for new simplify
---
src/main/scala/leon/purescala/TreeOps.scala | 5 +----
.../scala/leon/test/purescala/TreeOpsTests.scala | 16 ++++++++++++++++
2 files changed, 17 insertions(+), 4 deletions(-)
diff --git a/src/main/scala/leon/purescala/TreeOps.scala b/src/main/scala/leon/purescala/TreeOps.scala
index 0d4650149..234c0d608 100644
--- a/src/main/scala/leon/purescala/TreeOps.scala
+++ b/src/main/scala/leon/purescala/TreeOps.scala
@@ -1421,7 +1421,6 @@ object TreeOps {
}
def expandAndSimplifyArithmetic(expr: Expr): Expr = {
- println("got: " + expr)
val expr0 = try {
val freeVars: Array[Identifier] = variablesOf(expr).toArray
val coefs: Array[Expr] = TreeNormalizations.linearArithmeticForm(expr, freeVars)
@@ -1431,9 +1430,7 @@ object TreeOps {
} catch {
case _ => expr
}
- val res = simplifyArithmetic(expr0)
- println("simplified to: " + res)
- res
+ simplifyArithmetic(expr0)
}
//Simplify the expression, applying all the simplify for various theories
diff --git a/src/test/scala/leon/test/purescala/TreeOpsTests.scala b/src/test/scala/leon/test/purescala/TreeOpsTests.scala
index c77406e25..dc9d3737d 100644
--- a/src/test/scala/leon/test/purescala/TreeOpsTests.scala
+++ b/src/test/scala/leon/test/purescala/TreeOpsTests.scala
@@ -69,6 +69,22 @@ class TreeOpsTests extends FunSuite {
checkSameExpr(e6, simplify(e6), Set(xId))
}
+ test("expandAndSimplifyArithmetic") {
+ val e1 = Plus(IntLiteral(3), IntLiteral(2))
+ checkSameExpr(e1, expandAndSimplifyArithmetic(e1), Set())
+ val e2 = Plus(x, Plus(IntLiteral(3), IntLiteral(2)))
+ checkSameExpr(e2, expandAndSimplifyArithmetic(e2), Set(xId))
+
+ val e3 = Minus(IntLiteral(3), IntLiteral(2))
+ checkSameExpr(e3, expandAndSimplifyArithmetic(e3), Set())
+ val e4 = Plus(x, Minus(IntLiteral(3), IntLiteral(2)))
+ checkSameExpr(e4, expandAndSimplifyArithmetic(e4), Set(xId))
+ val e5 = Plus(x, Minus(x, IntLiteral(2)))
+ checkSameExpr(e5, expandAndSimplifyArithmetic(e5), Set(xId))
+
+ val e6 = Times(IntLiteral(9), Plus(Division(x, IntLiteral(3)), Division(x, IntLiteral(6))))
+ checkSameExpr(e6, expandAndSimplifyArithmetic(e6), Set(xId))
+ }
test("extractEquals") {
val eq = Equals(a, b)
--
GitLab