From 53a5faee13e7ea78d9a1914a6d524452e0a9c36c Mon Sep 17 00:00:00 2001
From: Etienne Kneuss <etienne.kneuss@epfl.ch>
Date: Tue, 7 Oct 2014 13:08:06 +0200
Subject: [PATCH] Simplify flattened pre/post
---
src/main/scala/leon/purescala/TreeOps.scala | 10 +++++++---
1 file changed, 7 insertions(+), 3 deletions(-)
diff --git a/src/main/scala/leon/purescala/TreeOps.scala b/src/main/scala/leon/purescala/TreeOps.scala
index 1b0222094..eece54ca8 100644
--- a/src/main/scala/leon/purescala/TreeOps.scala
+++ b/src/main/scala/leon/purescala/TreeOps.scala
@@ -3,6 +3,8 @@
package leon
package purescala
+import utils.Simplifiers
+
import leon.solvers._
import scala.collection.concurrent.TrieMap
@@ -1805,7 +1807,7 @@ object TreeOps {
* if (..) { foo(b, a) } else { .. }
* }
**/
- def flattenFunctions(fdOuter: FunDef): FunDef = {
+ def flattenFunctions(fdOuter: FunDef, ctx: LeonContext, p: Program): FunDef = {
fdOuter.body match {
case Some(LetDef(fdInner, FunctionInvocation(tfdInner2, args))) if fdInner == tfdInner2.fd =>
val argsDef = fdOuter.params.map(_.id)
@@ -1851,9 +1853,11 @@ object TreeOps {
val newFd = fdOuter.duplicate
+ val simp = Simplifiers.bestEffort(ctx, p) _
+
newFd.body = fdInner.body.map(b => simplePreTransform(pre)(b))
- newFd.precondition = mergePre(fdOuter.precondition, fdInner.precondition)
- newFd.postcondition = mergePost(fdOuter.postcondition, fdInner.postcondition)
+ newFd.precondition = mergePre(fdOuter.precondition, fdInner.precondition).map(simp)
+ newFd.postcondition = mergePost(fdOuter.postcondition, fdInner.postcondition).map{ case (id, ex) => id -> simp(ex) }
newFd
} else {
--
GitLab