From 946add91d8a3d67cf5cc0b42149db643a92afdaa Mon Sep 17 00:00:00 2001
From: Nicolas Voirol <voirol.nicolas@gmail.com>
Date: Tue, 15 Nov 2016 15:28:23 +0100
Subject: [PATCH] More optimizations for assume lifting
---
src/main/scala/inox/ast/SymbolOps.scala | 14 +++++++-------
.../inox/solvers/unrolling/TemplateGenerator.scala | 10 ++++++++--
2 files changed, 15 insertions(+), 9 deletions(-)
diff --git a/src/main/scala/inox/ast/SymbolOps.scala b/src/main/scala/inox/ast/SymbolOps.scala
index cb072f84c..ec0179bd9 100644
--- a/src/main/scala/inox/ast/SymbolOps.scala
+++ b/src/main/scala/inox/ast/SymbolOps.scala
@@ -224,7 +224,7 @@ trait SymbolOps { self: TypeOps =>
* in order to increase the precision of polarity analysis for
* quantification instantiations.
*/
- def simplifyQuantifications(e: Expr): Expr = {
+ def simplifyForalls(e: Expr): Expr = {
def inlineFunctions(e: Expr): Expr = {
val fds = functionCallsOf(e).flatMap { fi =>
@@ -246,7 +246,7 @@ trait SymbolOps { self: TypeOps =>
fixpoint(inline)(e)
}
- def inlineQuantifications(e: Expr): Expr = {
+ def inlineForalls(e: Expr): Expr = {
def liftForalls(args: Seq[ValDef], es: Seq[Expr], recons: Seq[Expr] => Expr): Expr = {
val (allArgs, allBodies) = es.map {
case f: Forall =>
@@ -315,7 +315,7 @@ trait SymbolOps { self: TypeOps =>
case _ => e
}
- normalizeClauses(inlineQuantifications(inlineFunctions(e)))
+ normalizeClauses(inlineForalls(inlineFunctions(e)))
}
def simplifyLets(expr: Expr): Expr = postMap({
@@ -778,10 +778,10 @@ trait SymbolOps { self: TypeOps =>
def simplifyFormula(e: Expr, simplify: Boolean = true): Expr = {
if (simplify) {
val simp: Expr => Expr =
- ((e: Expr) => simplifyHOFunctions(e)) compose
- ((e: Expr) => simplifyByConstructors(e)) compose
- ((e: Expr) => simplifyAssumptions(e)) compose
- ((e: Expr) => simplifyQuantifications(e))
+ ((e: Expr) => simplifyHOFunctions(e)) compose
+ ((e: Expr) => simplifyByConstructors(e)) compose
+ ((e: Expr) => simplifyAssumptions(e)) compose
+ ((e: Expr) => simplifyForalls(e))
fixpoint(simp)(e)
} else {
simplifyHOFunctions(e, simplify = false)
diff --git a/src/main/scala/inox/solvers/unrolling/TemplateGenerator.scala b/src/main/scala/inox/solvers/unrolling/TemplateGenerator.scala
index 2a12e422b..55888023d 100644
--- a/src/main/scala/inox/solvers/unrolling/TemplateGenerator.scala
+++ b/src/main/scala/inox/solvers/unrolling/TemplateGenerator.scala
@@ -297,7 +297,7 @@ trait TemplateGenerator { self: Templates =>
}
}
- case l @ Lambda(args, body) =>
+ case l: Lambda =>
val idArgs : Seq[Variable] = lambdaArgs(l)
val trArgs : Seq[Encoded] = idArgs.map(id => substMap.getOrElse(id, encodeSymbol(id)))
@@ -386,7 +386,13 @@ trait TemplateGenerator { self: Templates =>
registerLambda(template)
lid
- case f @ Forall(args, body) =>
+ case f: Forall =>
+ val (assumptions, Forall(args, body)) = liftAssumptions(f)
+
+ for (a <- assumptions) {
+ rec(pathVar, a, Some(true))
+ }
+
val TopLevelAnds(conjuncts) = body
val conjunctQs = conjuncts.map { conjunct =>
--
GitLab