From c7f114e45995a188c6b36ccb34974e3b2e5dcf67 Mon Sep 17 00:00:00 2001
From: Nicolas Voirol <voirol.nicolas@gmail.com>
Date: Sat, 12 Nov 2016 00:08:49 +0100
Subject: [PATCH] Simplify formulas before going into solver
---
src/main/scala/inox/ast/SymbolOps.scala | 4 ++++
.../scala/inox/solvers/unrolling/TemplateGenerator.scala | 2 +-
src/main/scala/inox/solvers/unrolling/Templates.scala | 2 +-
src/main/scala/inox/tip/Parser.scala | 8 --------
4 files changed, 6 insertions(+), 10 deletions(-)
diff --git a/src/main/scala/inox/ast/SymbolOps.scala b/src/main/scala/inox/ast/SymbolOps.scala
index f78c4060c..49cd236dc 100644
--- a/src/main/scala/inox/ast/SymbolOps.scala
+++ b/src/main/scala/inox/ast/SymbolOps.scala
@@ -622,6 +622,10 @@ trait SymbolOps { self: TypeOps =>
liftToLambdas(expr)
}
+ def simplifyFormula(e: Expr): Expr = {
+ simplifyHOFunctions(simplifyByConstructors(simplifyQuantifications(e)))
+ }
+
// Use this only to debug isValueOfType
private implicit class BooleanAdder(b: Boolean) {
@inline def <(msg: => String) = {/*if(!b) println(msg); */b}
diff --git a/src/main/scala/inox/solvers/unrolling/TemplateGenerator.scala b/src/main/scala/inox/solvers/unrolling/TemplateGenerator.scala
index 2fc373f65..3b01c100e 100644
--- a/src/main/scala/inox/solvers/unrolling/TemplateGenerator.scala
+++ b/src/main/scala/inox/solvers/unrolling/TemplateGenerator.scala
@@ -43,7 +43,7 @@ trait TemplateGenerator { self: Templates =>
return cache(tfd)
}
- val lambdaBody : Expr = simplifyHOFunctions(tfd.fullBody)
+ val lambdaBody : Expr = simplifyFormula(tfd.fullBody)
val funDefArgs: Seq[Variable] = tfd.params.map(_.toVariable)
val lambdaArguments: Seq[Variable] = lambdaArgs(lambdaBody)
diff --git a/src/main/scala/inox/solvers/unrolling/Templates.scala b/src/main/scala/inox/solvers/unrolling/Templates.scala
index d2579e9a0..95f9f7b56 100644
--- a/src/main/scala/inox/solvers/unrolling/Templates.scala
+++ b/src/main/scala/inox/solvers/unrolling/Templates.scala
@@ -557,7 +557,7 @@ trait Templates extends TemplateGenerator
val tpeClauses = bindings.flatMap { case (v, s) => registerSymbol(encodedStart, s, v.getType) }.toSeq
- val instExpr = simplifyHOFunctions(simplifyQuantifications(expr))
+ val instExpr = simplifyFormula(expr)
val (condVars, exprVars, condTree, guardedExprs, eqs, lambdas, quants) =
mkClauses(start, instExpr, bindings + (start -> encodedStart), polarity = Some(true))
diff --git a/src/main/scala/inox/tip/Parser.scala b/src/main/scala/inox/tip/Parser.scala
index 0a5af026d..422cedd2b 100644
--- a/src/main/scala/inox/tip/Parser.scala
+++ b/src/main/scala/inox/tip/Parser.scala
@@ -43,14 +43,6 @@ class Parser(file: File) {
(for (cmd <- script.commands) yield cmd match {
case CheckSat() =>
val expr: Expr = locals.symbols.andJoin(assertions)
- for (fd <- locals.symbols.functions.values) {
- if (fd.fullBody.getType(locals.symbols) == Untyped) {
- println(locals.symbols.explainTyping(fd.fullBody)(PrinterOptions(printUniqueIds = true, symbols = Some(locals.symbols))))
- }
- }
- if (expr.getType(locals.symbols) == Untyped) {
- println(locals.symbols.explainTyping(expr)(PrinterOptions(printUniqueIds = true, symbols = Some(locals.symbols))))
- }
Some((locals.symbols, expr))
case _ =>
--
GitLab