From 7b01175f85ea561dbdb2a250e72c6402f5869105 Mon Sep 17 00:00:00 2001
From: Nicolas Voirol <voirol.nicolas@gmail.com>
Date: Wed, 2 Nov 2016 15:46:41 +0100
Subject: [PATCH] Fixed some stuff with lambda equality
---
.../solvers/unrolling/LambdaTemplates.scala | 20 +++++++++----------
1 file changed, 10 insertions(+), 10 deletions(-)
diff --git a/src/main/scala/inox/solvers/unrolling/LambdaTemplates.scala b/src/main/scala/inox/solvers/unrolling/LambdaTemplates.scala
index d3f9e12cc..14fdc53e3 100644
--- a/src/main/scala/inox/solvers/unrolling/LambdaTemplates.scala
+++ b/src/main/scala/inox/solvers/unrolling/LambdaTemplates.scala
@@ -168,20 +168,19 @@ trait LambdaTemplates { self: Templates =>
* already been found, then the associated instantiations must already appear
* in those handled by the solver.
*/
- lazy val (key, instantiation) = {
+ lazy val (key, instantiation, locals) = {
val (substMap, substInst) = Template.substitution(
condVars, exprVars, condTree, lambdas, quantifications, Map.empty, pathVar._2)
val tmplInst = Template.instantiate(clauses, blockers, applications, matchers, substMap)
+ val instantiation = substInst ++ tmplInst
val substituter = mkSubstituter(substMap.mapValues(_.encoded))
- val key = (lambda, pathVar._2, dependencies.map(substituter))
- val instantiation = substInst ++ tmplInst
- (key, instantiation)
- }
+ val deps = dependencies.map(substituter)
+ val key = (lambda, pathVar._2, deps)
- lazy val locals: Seq[(Variable, Encoded)] = {
val sortedDeps = exprOps.variablesOf(lambda).toSeq.sortBy(_.id.uniqueName)
- sortedDeps zip dependencies
+ val locals = sortedDeps zip deps
+ (key, instantiation, locals)
}
override def equals(that: Any): Boolean = that match {
@@ -297,7 +296,7 @@ trait LambdaTemplates { self: Templates =>
val idT = encodeSymbol(template.ids._1)
val newTemplate = template.withId(idT)
- val orderingClauses: Clauses = newTemplate.structure.locals.flatMap {
+ val orderingClauses = newTemplate.structure.locals.flatMap {
case (v, dep) => registerClosure(newTemplate.start, idT -> newTemplate.tpe, dep -> v.tpe)
}
@@ -321,6 +320,7 @@ trait LambdaTemplates { self: Templates =>
extClauses ++
arglessEqClauses
+
byID += idT -> newTemplate
byType += newTemplate.tpe -> (byType(newTemplate.tpe) + (newTemplate.structure -> newTemplate))
@@ -416,12 +416,12 @@ trait LambdaTemplates { self: Templates =>
mkImplies(
mkAnd(template.start, that.start),
if (template.structure.lambda == that.structure.lambda) {
- val pairs = template.structure.dependencies zip that.structure.dependencies
+ val pairs = template.structure.locals zip that.structure.locals
val filtered = pairs.filter(p => p._1 != p._2)
if (filtered.isEmpty) {
equals
} else {
- val eqs = filtered.map(p => mkEquals(p._1, p._2))
+ val eqs = filtered.map(p => mkEquals(p._1._2, p._2._2))
mkEquals(mkAnd(eqs : _*), equals)
}
} else {
--
GitLab