diff --git a/src/main/scala/leon/purescala/TreeOps.scala b/src/main/scala/leon/purescala/TreeOps.scala index 0d465014979e7c11e5e2b980b7381bc057a0314a..234c0d6088d255ddf7c6c27b77516e474dbd27a9 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 c77406e25c833685e370603f80067146e4fd12b9..dc9d3737dc14c81b31f5c1060f9036a4c38063f3 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)