From ad4973722815928bfda74292973eb01437ddaa61 Mon Sep 17 00:00:00 2001
From: Nicolas Voirol <voirol.nicolas@gmail.com>
Date: Fri, 4 Nov 2016 12:57:56 +0100
Subject: [PATCH] Reworked lambda equality for models returned by underlying
solvers
---
src/main/scala/inox/ast/SymbolOps.scala | 15 +++++++--------
.../scala/inox/solvers/smtlib/SMTLIBTarget.scala | 3 ++-
.../solvers/unrolling/TemplateGenerator.scala | 6 +++---
.../inox/solvers/unrolling/UnrollingSolver.scala | 3 ++-
.../scala/inox/solvers/z3/AbstractZ3Solver.scala | 2 +-
5 files changed, 15 insertions(+), 14 deletions(-)
diff --git a/src/main/scala/inox/ast/SymbolOps.scala b/src/main/scala/inox/ast/SymbolOps.scala
index 199330771..9e170a10a 100644
--- a/src/main/scala/inox/ast/SymbolOps.scala
+++ b/src/main/scala/inox/ast/SymbolOps.scala
@@ -198,7 +198,7 @@ trait SymbolOps { self: TypeOps =>
/** Ensures the closure [[l]] can only be equal to some other closure if they share
* the same integer identifier [[id]]. This method makes sure this property is
* preserved after going through [[normalizeStructure(Lambda)]]. */
- def uniquateClosure(id: BigInt, res: Lambda): Lambda = {
+ def uniquateClosure(id: Int, res: Lambda): Lambda = {
def allArgs(l: Lambda): Seq[ValDef] = l.args ++ (l.body match {
case l2: Lambda => allArgs(l2)
case _ => Seq.empty
@@ -207,13 +207,12 @@ trait SymbolOps { self: TypeOps =>
val resArgs = allArgs(res)
if (resArgs.isEmpty) res else {
/* @nv: This is a hack to ensure that the notion of equality we define on closures
- * is respected by those returned by the model. The second `Let` is necessary
- * to keep [[normalizeStructure(Lambda)]] from lifting the first one out of
- * the closure's body. */
- Lambda(res.args,
- Let(ValDef(FreshIdentifier("id"), IntegerType), IntegerLiteral(id),
- Let(ValDef(FreshIdentifier("denormalize"), resArgs.head.tpe), resArgs.head.toVariable,
- res.body)))
+ * is respected by those returned by the model. */
+ Lambda(res.args, Let(
+ ValDef(FreshIdentifier("id"), tupleTypeWrap(List.fill(id)(resArgs.head.tpe))),
+ tupleWrap(List.fill(id)(resArgs.head.toVariable)),
+ res.body
+ ))
}
}
diff --git a/src/main/scala/inox/solvers/smtlib/SMTLIBTarget.scala b/src/main/scala/inox/solvers/smtlib/SMTLIBTarget.scala
index 2b71f2ccf..dfbeebdaa 100644
--- a/src/main/scala/inox/solvers/smtlib/SMTLIBTarget.scala
+++ b/src/main/scala/inox/solvers/smtlib/SMTLIBTarget.scala
@@ -477,7 +477,8 @@ trait SMTLIBTarget extends Interruptible with ADTManagers {
def extractLambda(n: BigInt, ft: FunctionType): Lambda = {
val FunctionType(from, to) = ft
- uniquateClosure(n, (lambdas.getB(ft) match {
+ val count = if (n < 0) -2 * n.toInt else 2 * n.toInt + 1
+ uniquateClosure(count, (lambdas.getB(ft) match {
case None => simplestValue(ft)
case Some(dynLambda) => letDefs.get(dynLambda) match {
case None => simplestValue(ft)
diff --git a/src/main/scala/inox/solvers/unrolling/TemplateGenerator.scala b/src/main/scala/inox/solvers/unrolling/TemplateGenerator.scala
index 12e758e6a..37e41c6aa 100644
--- a/src/main/scala/inox/solvers/unrolling/TemplateGenerator.scala
+++ b/src/main/scala/inox/solvers/unrolling/TemplateGenerator.scala
@@ -287,14 +287,14 @@ trait TemplateGenerator { self: Templates =>
case _ => (Seq.empty, e)
}
- extractBody(struct) match {
+ !l.getType.isInstanceOf[FunctionType] && (extractBody(struct) match {
case (params, ApplicationExtractor(caller: Variable, args)) =>
(params.map(_.toVariable) == args) && (deps.get(caller) match {
- case Some(_: Application | _: FunctionInvocation) => true
+ case Some(_: Application | _: FunctionInvocation | _: Variable) => true
case _ => false
})
case _ => false
- }
+ })
}
val depsByScope: Seq[(Variable, Expr)] = {
diff --git a/src/main/scala/inox/solvers/unrolling/UnrollingSolver.scala b/src/main/scala/inox/solvers/unrolling/UnrollingSolver.scala
index 28081283e..e08ece074 100644
--- a/src/main/scala/inox/solvers/unrolling/UnrollingSolver.scala
+++ b/src/main/scala/inox/solvers/unrolling/UnrollingSolver.scala
@@ -325,7 +325,8 @@ trait AbstractUnrollingSolver extends Solver { self =>
)=> Left(img)
}) match {
case Some(Right(enc)) => wrapped.eval(enc, tpe).get match {
- case Lambda(_, Let(_, IntegerLiteral(n), _)) => uniquateClosure(n, lambda)
+ case Lambda(_, Let(_, Tuple(es), _)) =>
+ uniquateClosure(if (es.size % 2 == 0) -es.size / 2 else es.size / 2, lambda)
case l => scala.sys.error("Unexpected extracted lambda format: " + l)
}
case Some(Left(img)) => img
diff --git a/src/main/scala/inox/solvers/z3/AbstractZ3Solver.scala b/src/main/scala/inox/solvers/z3/AbstractZ3Solver.scala
index 59a16643c..034d53dc2 100644
--- a/src/main/scala/inox/solvers/z3/AbstractZ3Solver.scala
+++ b/src/main/scala/inox/solvers/z3/AbstractZ3Solver.scala
@@ -581,7 +581,7 @@ trait AbstractZ3Solver
} else {
tpe match {
case ft @ FunctionType(fts, tt) =>
- val n = BigInt(t.toString.split("!").last.init)
+ val n = t.toString.split("!").last.init.toInt
uniquateClosure(n, (lambdas.getB(ft) match {
case None => simplestValue(ft)
case Some(decl) => model.getFuncInterpretations.find(_._1 == decl) match {
--
GitLab