From 1ba68eab543958a376fa969cb1c2b7718a0510f3 Mon Sep 17 00:00:00 2001
From: Nicolas Voirol <voirol.nicolas@gmail.com>
Date: Thu, 3 Nov 2016 10:41:43 +0100
Subject: [PATCH] Better separation between lambda templates and their
structure key
---
.../solvers/unrolling/LambdaTemplates.scala | 27 ++++++++++++-------
.../unrolling/QuantificationTemplates.scala | 1 +
.../solvers/unrolling/TemplateGenerator.scala | 23 +++++++++-------
3 files changed, 31 insertions(+), 20 deletions(-)
diff --git a/src/main/scala/inox/solvers/unrolling/LambdaTemplates.scala b/src/main/scala/inox/solvers/unrolling/LambdaTemplates.scala
index 14fdc53e3..ad9640ddc 100644
--- a/src/main/scala/inox/solvers/unrolling/LambdaTemplates.scala
+++ b/src/main/scala/inox/solvers/unrolling/LambdaTemplates.scala
@@ -54,6 +54,7 @@ trait LambdaTemplates { self: Templates =>
ids: (Variable, Encoded),
pathVar: (Variable, Encoded),
arguments: Seq[(Variable, Encoded)],
+ closures: Seq[(Variable, Encoded)],
condVars: Map[Variable, Encoded],
exprVars: Map[Variable, Encoded],
condTree: Map[Variable, Set[Variable]],
@@ -70,14 +71,14 @@ trait LambdaTemplates { self: Templates =>
val tpe = ids._1.getType.asInstanceOf[FunctionType]
val (clauses, blockers, applications, matchers, templateString) =
Template.encode(pathVar, arguments, condVars, exprVars, guardedExprs, equations,
- lambdas, quantifications, substMap = baseSubstMap + ids, optApp = Some(id -> tpe))
+ lambdas, quantifications, substMap = baseSubstMap + ids ++ closures, optApp = Some(id -> tpe))
val lambdaString : () => String = () => {
"Template for lambda " + ids._1 + ": " + lambda + " is :\n" + templateString()
}
new LambdaTemplate(
- ids, pathVar, arguments,
+ ids, pathVar, arguments, closures,
condVars, exprVars, condTree,
clauses, blockers, applications, matchers,
lambdas, quantifications,
@@ -195,6 +196,7 @@ trait LambdaTemplates { self: Templates =>
val ids: (Variable, Encoded),
val pathVar: (Variable, Encoded),
val arguments: Seq[(Variable, Encoded)],
+ val closures: Seq[(Variable, Encoded)],
val condVars: Map[Variable, Encoded],
val exprVars: Map[Variable, Encoded],
val condTree: Map[Variable, Set[Variable]],
@@ -214,7 +216,7 @@ trait LambdaTemplates { self: Templates =>
def substitute(substituter: Encoded => Encoded, msubst: Map[Encoded, Matcher]): LambdaTemplate = new LambdaTemplate(
ids._1 -> substituter(ids._2),
pathVar._1 -> substituter(pathVar._2),
- arguments, condVars, exprVars, condTree,
+ arguments, closures, condVars, exprVars, condTree,
clauses.map(substituter),
blockers.map { case (b, fis) => substituter(b) -> fis.map(_.substitute(substituter, msubst)) },
applications.map { case (b, apps) => substituter(b) -> apps.map(_.substitute(substituter, msubst)) },
@@ -224,12 +226,18 @@ trait LambdaTemplates { self: Templates =>
structure.substitute(substituter, msubst),
lambda, stringRepr)
- def withId(idT: Encoded): LambdaTemplate = {
- val substituter = mkSubstituter(Map(ids._2 -> idT))
+ /** This must be called right before returning the clauses in [[structure.instantiation]]! */
+ def concretize(idT: Encoded): LambdaTemplate = {
+ val substituter = mkSubstituter(Map(ids._2 -> idT) ++ (closures.map(_._2) zip structure.locals.map(_._2)))
new LambdaTemplate(
- ids._1 -> idT, pathVar, arguments, condVars, exprVars, condTree,
- clauses map substituter, // make sure the body-defining clause is inlined!
- blockers, applications, matchers, lambdas, quantifications,
+ ids._1 -> idT,
+ pathVar, arguments, closures, condVars, exprVars, condTree,
+ clauses map substituter,
+ blockers.map { case (b, fis) => b -> fis.map(_.substitute(substituter, Map.empty)) },
+ applications.map { case (b, apps) => b -> apps.map(_.substitute(substituter, Map.empty)) },
+ matchers.map { case (b, ms) => b -> ms.map(_.substitute(substituter, Map.empty)) },
+ lambdas.map(_.substitute(substituter, Map.empty)),
+ quantifications.map(_.substitute(substituter, Map.empty)),
structure, lambda, stringRepr)
}
@@ -294,7 +302,7 @@ trait LambdaTemplates { self: Templates =>
case None =>
val idT = encodeSymbol(template.ids._1)
- val newTemplate = template.withId(idT)
+ val newTemplate = template.concretize(idT)
val orderingClauses = newTemplate.structure.locals.flatMap {
case (v, dep) => registerClosure(newTemplate.start, idT -> newTemplate.tpe, dep -> v.tpe)
@@ -320,7 +328,6 @@ trait LambdaTemplates { self: Templates =>
extClauses ++
arglessEqClauses
-
byID += idT -> newTemplate
byType += newTemplate.tpe -> (byType(newTemplate.tpe) + (newTemplate.structure -> newTemplate))
diff --git a/src/main/scala/inox/solvers/unrolling/QuantificationTemplates.scala b/src/main/scala/inox/solvers/unrolling/QuantificationTemplates.scala
index 0cce88476..46d591a37 100644
--- a/src/main/scala/inox/solvers/unrolling/QuantificationTemplates.scala
+++ b/src/main/scala/inox/solvers/unrolling/QuantificationTemplates.scala
@@ -308,6 +308,7 @@ trait QuantificationTemplates { self: Templates =>
if (handledMatchers(relevantBlockers -> matcher)) {
Seq.empty
} else {
+ ctx.reporter.debug(" -> instantiating matcher " + blockers.mkString("{",",","}") + " ==> " + matcher)
handledMatchers += relevantBlockers -> matcher
quantifications.flatMap(_.instantiate(relevantBlockers, matcher, defer))
}
diff --git a/src/main/scala/inox/solvers/unrolling/TemplateGenerator.scala b/src/main/scala/inox/solvers/unrolling/TemplateGenerator.scala
index 9d4f63a07..96cdd6408 100644
--- a/src/main/scala/inox/solvers/unrolling/TemplateGenerator.scala
+++ b/src/main/scala/inox/solvers/unrolling/TemplateGenerator.scala
@@ -276,24 +276,25 @@ trait TemplateGenerator { self: Templates =>
val idArgs : Seq[Variable] = lambdaArgs(l)
val trArgs : Seq[Encoded] = idArgs.map(id => substMap.getOrElse(id, encodeSymbol(id)))
+ val (struct, deps) = normalizeStructure(l)
+ val sortedDeps = deps.toSeq.sortBy(_._1.id.uniqueName)
+ val idDeps = sortedDeps.map(_._1)
+ val trDeps = idDeps.map(id => encodeSymbol(id))
+
val lid = Variable(FreshIdentifier("lambda", true), bestRealType(l.getType))
- val clauses = liftedEquals(lid, l, idArgs, inlineFirst = true)
+ val clauses = liftedEquals(lid, struct, idArgs, inlineFirst = true)
val localSubst: Map[Variable, Encoded] = substMap ++ condVars ++ exprVars ++ lambdaVars
- val clauseSubst: Map[Variable, Encoded] = localSubst ++ (idArgs zip trArgs)
+ val clauseSubst: Map[Variable, Encoded] = localSubst ++ (idArgs zip trArgs) ++ (idDeps zip trDeps)
val (lambdaConds, lambdaExprs, lambdaTree, lambdaGuarded, lambdaEqs, lambdaTemplates, lambdaQuants) =
clauses.foldLeft(emptyClauses)((clsSet, cls) => clsSet ++ mkClauses(pathVar, cls, clauseSubst))
val ids: (Variable, Encoded) = lid -> storeLambda(lid)
- val (struct, deps) = normalizeStructure(l)
- val sortedDeps = deps.toSeq.sortBy(_._1.id.uniqueName)
-
val (dependencies, (depConds, depExprs, depTree, depGuarded, depEqs, depLambdas, depQuants)) =
sortedDeps.foldLeft[(Seq[Encoded], TemplateClauses)](Seq.empty -> emptyClauses) {
- case ((dependencies, clsSet), (id, expr)) =>
+ case ((dependencies, clsSet), (_, expr)) =>
if (!exprOps.isSimple(expr)) {
- val encoded = encodeSymbol(id)
val (e, cls @ (_, _, _, _, _, lmbds, quants)) = mkExprClauses(pathVar, expr, localSubst)
val clauseSubst = localSubst ++ lmbds.map(_.ids) ++ quants.flatMap(_.mapping)
(dependencies :+ mkEncoder(clauseSubst)(e), clsSet ++ cls)
@@ -307,9 +308,11 @@ trait TemplateGenerator { self: Templates =>
depConds, depExprs, depGuarded, depEqs, depLambdas, depQuants, localSubst)
val depClosures: Seq[Encoded] = {
- val vars = exprOps.variablesOf(l)
var cls: Seq[Variable] = Seq.empty
- exprOps.preTraversal { case v: Variable if vars(v) => cls :+= v case _ => } (l)
+ for ((_, e) <- sortedDeps) {
+ val vars = exprOps.variablesOf(e).toSet
+ exprOps.preTraversal { case v: Variable if vars(v) => cls :+= v case _ => } (e)
+ }
cls.distinct.map(localSubst)
}
@@ -318,7 +321,7 @@ trait TemplateGenerator { self: Templates =>
depConds, depExprs, depTree, depClauses, depCalls, depApps, depMatchers, depLambdas, depQuants)
val template = LambdaTemplate(ids, pathVar -> encodedCond(pathVar),
- idArgs zip trArgs, lambdaConds, lambdaExprs, lambdaTree,
+ idArgs zip trArgs, idDeps zip trDeps, lambdaConds, lambdaExprs, lambdaTree,
lambdaGuarded, lambdaEqs, lambdaTemplates, lambdaQuants, structure, localSubst, l)
registerLambda(template)
lid
--
GitLab