From 94e82a7bc285925fe7d72c12f39cf4e3d95ec43f Mon Sep 17 00:00:00 2001
From: Etienne Kneuss <ekneuss@gmail.com>
Date: Fri, 4 Jan 2013 16:57:35 +0100
Subject: [PATCH] Simplify preconditions when possible
---
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 1b5a4bb9f..c3cc7809d 100644
--- a/src/main/scala/leon/purescala/TreeOps.scala
+++ b/src/main/scala/leon/purescala/TreeOps.scala
@@ -7,6 +7,7 @@ object TreeOps {
import Common._
import TypeTrees._
import Definitions._
+ import xlang.Trees.LetDef
import Trees._
import Extractors._
@@ -1131,6 +1132,23 @@ object TreeOps {
def simplifyTautologies(solver : Solver)(expr : Expr) : Expr = {
def pre(e : Expr) = e match {
+ case LetDef(fd, expr) if fd.hasPrecondition =>
+ val pre = fd.precondition.get
+
+ solver.solve(pre) match {
+ case Some(true) =>
+ fd.precondition = None
+
+ case Some(false) => solver.solve(Not(pre)) match {
+ case Some(true) =>
+ fd.precondition = Some(BooleanLiteral(false))
+ case _ =>
+ }
+ case None =>
+ }
+
+ e
+
case IfExpr(cond, then, elze) =>
try {
solver.solve(cond) match {
--
GitLab