From 5e222f54ba44f27c7c3782926b0d3d11903ab410 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?R=C3=A9gis=20Blanc?= <regwblanc@gmail.com>
Date: Thu, 29 Nov 2012 16:17:14 +0100
Subject: [PATCH] new simplification using expansion and grouping
---
src/main/scala/leon/purescala/TreeOps.scala | 18 ++++++++++++++++++
1 file changed, 18 insertions(+)
diff --git a/src/main/scala/leon/purescala/TreeOps.scala b/src/main/scala/leon/purescala/TreeOps.scala
index a7a47c8a6..0d4650149 100644
--- a/src/main/scala/leon/purescala/TreeOps.scala
+++ b/src/main/scala/leon/purescala/TreeOps.scala
@@ -1414,10 +1414,28 @@ object TreeOps {
val na = f(a)
if(a == na) a else fix(f)(na)
}
+
+
val res = fix(simplePostTransform(simplify0))(expr)
res
}
+ 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)
+ coefs.toList.zip(IntLiteral(1) :: freeVars.toList.map(Variable(_))).foldLeft[Expr](IntLiteral(0))((acc, t) => {
+ if(t._1 == IntLiteral(0)) acc else Plus(acc, Times(t._1, t._2))
+ })
+ } catch {
+ case _ => expr
+ }
+ val res = simplifyArithmetic(expr0)
+ println("simplified to: " + res)
+ res
+ }
+
//Simplify the expression, applying all the simplify for various theories
//Maybe it would be a good design decision to not have any simplify calling
//an underlying solver, to somehow keep it light and become a function we call often
--
GitLab