From f454f3fa176a5644cd27c3148d6d98d371c941f4 Mon Sep 17 00:00:00 2001
From: Etienne Kneuss <colder@php.net>
Date: Wed, 23 Oct 2013 16:23:17 +0200
Subject: [PATCH] Improve simplification of simple let-tuples, remove MBQI
warnings
---
src/main/scala/leon/purescala/TreeOps.scala | 23 ++++++++++++++-----
.../scala/leon/solvers/z3/FairZ3Solver.scala | 1 -
.../solvers/z3/UninterpretedZ3Solver.scala | 1 -
3 files changed, 17 insertions(+), 8 deletions(-)
diff --git a/src/main/scala/leon/purescala/TreeOps.scala b/src/main/scala/leon/purescala/TreeOps.scala
index 2ac6b102e..d31c7a392 100644
--- a/src/main/scala/leon/purescala/TreeOps.scala
+++ b/src/main/scala/leon/purescala/TreeOps.scala
@@ -449,9 +449,11 @@ object TreeOps {
* Note that the code is simple but far from optimal (many traversals...)
*/
def simplifyLets(expr: Expr) : Expr = {
+
def simplerLet(t: Expr) : Option[Expr] = t match {
- case letExpr @ Let(i, t: Terminal, b) if !containsChoose(b) => Some(replace(Map((Variable(i) -> t)), b))
+ case letExpr @ Let(i, t: Terminal, b) if !containsChoose(b) =>
+ Some(replace(Map((Variable(i) -> t)), b))
case letExpr @ Let(i,e,b) if !containsChoose(b) => {
val occurences = treeCatamorphism[Int]((e:Expr) => e match {
@@ -468,7 +470,6 @@ object TreeOps {
}
case letTuple @ LetTuple(ids, Tuple(exprs), body) if !containsChoose(body) =>
-
var newBody = body
val (remIds, remExprs) = (ids zip exprs).filter {
@@ -501,15 +502,24 @@ object TreeOps {
Some(LetTuple(remIds, Tuple(remExprs), newBody))
}
+ case l @ LetTuple(ids, tExpr: Terminal, body) if !containsChoose(body) =>
+ val substMap : Map[Expr,Expr] = ids.map(Variable(_) : Expr).zipWithIndex.toMap.map {
+ case (v,i) => (v -> TupleSelect(tExpr, i + 1).setType(v.getType))
+ }
+
+ Some(replace(substMap, body))
+
case l @ LetTuple(ids, tExpr, body) if !containsChoose(body) =>
- val TupleType(types) = tExpr.getType
val arity = ids.size
- // A map containing vectors of the form (0, ..., 1, ..., 0) where the one corresponds to the index of the identifier in the
- // LetTuple. The idea is that we can sum such vectors up to compute the occurences of all variables in one traversal of the
- // expression.
val zeroVec = Seq.fill(arity)(0)
val idMap = ids.zipWithIndex.toMap.mapValues(i => zeroVec.updated(i, 1))
+ // A map containing vectors of the form (0, ..., 1, ..., 0) where
+ // the one corresponds to the index of the identifier in the
+ // LetTuple. The idea is that we can sum such vectors up to compute
+ // the occurences of all variables in one traversal of the
+ // expression.
+
val occurences : Seq[Int] = treeCatamorphism[Seq[Int]]((e : Expr) => e match {
case Variable(x) => idMap.getOrElse(x, zeroVec)
case _ => zeroVec
@@ -531,6 +541,7 @@ object TreeOps {
case _ => None
}
+
searchAndReplaceDFS(simplerLet)(expr)
}
diff --git a/src/main/scala/leon/solvers/z3/FairZ3Solver.scala b/src/main/scala/leon/solvers/z3/FairZ3Solver.scala
index 63abcb42a..c402b865c 100644
--- a/src/main/scala/leon/solvers/z3/FairZ3Solver.scala
+++ b/src/main/scala/leon/solvers/z3/FairZ3Solver.scala
@@ -66,7 +66,6 @@ class FairZ3Solver(val context : LeonContext, val program: Program)
// This is fixed.
protected[leon] val z3cfg = new Z3Config(
"MODEL" -> true,
- "MBQI" -> false,
"TYPE_CHECK" -> true,
"WELL_SORTED_CHECK" -> true
)
diff --git a/src/main/scala/leon/solvers/z3/UninterpretedZ3Solver.scala b/src/main/scala/leon/solvers/z3/UninterpretedZ3Solver.scala
index 78b75ee5e..d9f2696ca 100644
--- a/src/main/scala/leon/solvers/z3/UninterpretedZ3Solver.scala
+++ b/src/main/scala/leon/solvers/z3/UninterpretedZ3Solver.scala
@@ -31,7 +31,6 @@ class UninterpretedZ3Solver(val context : LeonContext, val program: Program)
// this is fixed
protected[leon] val z3cfg = new Z3Config(
"MODEL" -> true,
- "MBQI" -> false,
"TYPE_CHECK" -> true,
"WELL_SORTED_CHECK" -> true
)
--
GitLab