diff --git a/src/main/scala/inox/ast/CallGraph.scala b/src/main/scala/inox/ast/CallGraph.scala
index 12d68dd0fb28c4d5ad8b3879c8b60d29d300d513..a79b0ecaa122e1d6980a0cfaf686ee1e8dd38d77 100644
--- a/src/main/scala/inox/ast/CallGraph.scala
+++ b/src/main/scala/inox/ast/CallGraph.scala
@@ -96,7 +96,7 @@ trait CallGraph {
val (c1, c2) = (functionComponent(a), functionComponent(b))
if (c1.isEmpty && c2.isEmpty) a.id.uniqueName.compare(b.id.uniqueName)
else if (c1.isEmpty) -1
- else if (c2.isEmpty) -1
+ else if (c2.isEmpty) +1
else componentOrdering.compare(c1, c2)
}
}
diff --git a/src/main/scala/inox/ast/SymbolOps.scala b/src/main/scala/inox/ast/SymbolOps.scala
index 7a007f1143f27affd0a68bb5daa49c94113c8511..9ebfc07ba4ee0b3f05aa0e601599cef593d758eb 100644
--- a/src/main/scala/inox/ast/SymbolOps.scala
+++ b/src/main/scala/inox/ast/SymbolOps.scala
@@ -5,6 +5,8 @@ package ast
import utils._
+import scala.collection.mutable.{Map => MutableMap}
+
/** Provides functions to manipulate [[Expressions.Expr]] in cases where
* a symbol table is available (and required: see [[ExprOps]] for
* simpler tree manipulations).
@@ -88,8 +90,8 @@ trait SymbolOps { self: TypeOps =>
fixpoint(postMap(rec))(expr)
}
- private val typedIds: scala.collection.mutable.Map[Type, List[Identifier]] =
- scala.collection.mutable.Map.empty.withDefaultValue(List.empty)
+ private val typedIds: MutableMap[Type, List[Identifier]] =
+ MutableMap.empty.withDefaultValue(List.empty)
/** Normalizes identifiers in an expression to enable some notion of structural
* equality between expressions on which usual equality doesn't make sense
@@ -106,64 +108,71 @@ trait SymbolOps { self: TypeOps =>
*/
def normalizeStructure(args: Seq[ValDef], expr: Expr, onlySimple: Boolean = true):
(Seq[ValDef], Expr, Map[Variable, Expr]) = synchronized {
- val vars = args.map(_.toVariable).toSet
-
- class Normalizer extends SelfTreeTransformer {
- var subst: Map[Variable, Expr] = Map.empty
- var varSubst: Map[Identifier, Identifier] = Map.empty
- var remainingIds: Map[Type, List[Identifier]] = typedIds.toMap
-
- def getId(e: Expr): Identifier = {
- val tpe = bestRealType(e.getType)
- val newId = remainingIds.get(tpe) match {
- case Some(x :: xs) =>
- remainingIds += tpe -> xs
- x
- case _ =>
- val x = FreshIdentifier("x", true)
- typedIds(tpe) = typedIds(tpe) :+ x
- x
- }
- subst += Variable(newId, tpe) -> e
- newId
- }
- override def transform(id: Identifier, tpe: Type): (Identifier, Type) = subst.get(Variable(id, tpe)) match {
- case Some(Variable(newId, tpe)) => (newId, tpe)
- case Some(_) => scala.sys.error("Should never happen!")
- case None => varSubst.get(id) match {
- case Some(newId) => (newId, tpe)
- case None =>
- val newId = getId(Variable(id, tpe))
- varSubst += id -> newId
- (newId, tpe)
- }
+ val subst: MutableMap[Variable, Expr] = MutableMap.empty
+ val varSubst: MutableMap[Identifier, Identifier] = MutableMap.empty
+
+ // Note: don't use clone here, we want to drop the `withDefaultValue` feature of [[typeIds]]
+ val remainingIds: MutableMap[Type, List[Identifier]] = MutableMap.empty ++ typedIds.toMap
+
+ def getId(e: Expr): Identifier = {
+ val tpe = bestRealType(e.getType)
+ val newId = remainingIds.get(tpe) match {
+ case Some(x :: xs) =>
+ remainingIds += tpe -> xs
+ x
+ case _ =>
+ val x = FreshIdentifier("x", true)
+ typedIds(tpe) = typedIds(tpe) :+ x
+ x
}
+ subst += Variable(newId, tpe) -> e
+ newId
+ }
- override def transform(e: Expr): Expr = e match {
- case expr if (!onlySimple || isSimple(expr)) && (variablesOf(expr) & vars).isEmpty =>
- Variable(getId(expr), expr.getType)
- case f: Forall =>
- val (args, body, newSubst) = normalizeStructure(f.args, f.body, onlySimple)
- subst ++= newSubst
- Forall(args, body)
- case l: Lambda =>
- val (args, body, newSubst) = normalizeStructure(l.args, l.body, onlySimple)
- subst ++= newSubst
- Lambda(args, body)
- case _ => super.transform(e)
+ def transformId(id: Identifier, tpe: Type): (Identifier, Type) = subst.get(Variable(id, tpe)) match {
+ case Some(Variable(newId, tpe)) => (newId, tpe)
+ case Some(_) => scala.sys.error("Should never happen!")
+ case None => varSubst.get(id) match {
+ case Some(newId) => (newId, tpe)
+ case None =>
+ val newId = getId(Variable(id, tpe))
+ varSubst += id -> newId
+ (newId, tpe)
}
}
- val n = new Normalizer
- // this registers the argument images into n.subst
- val bindings = args map n.transform
- val normalized = n.transform(expr)
+ def rec(vars: Set[Variable], body: Expr): Expr = {
+
+ class Normalizer extends SelfTreeTransformer {
+ override def transform(id: Identifier, tpe: Type): (Identifier, Type) = transformId(id, tpe)
+
+ override def transform(e: Expr): Expr = e match {
+ case expr if (!onlySimple || isSimple(expr)) && (variablesOf(expr) & vars).isEmpty =>
+ Variable(getId(expr), expr.getType)
+ case f: Forall =>
+ val newBody = rec(vars ++ f.args.map(_.toVariable), f.body)
+ Forall(f.args.map(vd => vd.copy(id = varSubst(vd.id))), newBody)
+ case l: Lambda =>
+ val newBody = rec(vars ++ l.args.map(_.toVariable), l.body)
+ Lambda(l.args.map(vd => vd.copy(id = varSubst(vd.id))), newBody)
+ case _ => super.transform(e)
+ }
+ }
+
+ val n = new Normalizer
+
+ // this registers the argument images into subst
+ vars foreach n.transform
+ n.transform(body)
+ }
- val freeVars = variablesOf(normalized) -- bindings.map(_.toVariable)
- val bodySubst = n.subst.filter(p => freeVars(p._1))
+ val newExpr = rec(args.map(_.toVariable).toSet, expr)
+ val bindings = args.map(vd => vd.copy(id = varSubst(vd.id)))
+ val freeVars = variablesOf(newExpr) -- bindings.map(_.toVariable)
+ val bodySubst = subst.filter(p => freeVars(p._1)).toMap
- (bindings, normalized, bodySubst)
+ (bindings, newExpr, bodySubst)
}
def normalizeStructure(lambda: Lambda): (Lambda, Map[Variable, Expr]) = {
diff --git a/src/main/scala/inox/solvers/unrolling/LambdaTemplates.scala b/src/main/scala/inox/solvers/unrolling/LambdaTemplates.scala
index ad9640ddcc12047532445d3743891218dddec67f..16510afc7fe73c9c88d31b674bb3ccbb259a6e45 100644
--- a/src/main/scala/inox/solvers/unrolling/LambdaTemplates.scala
+++ b/src/main/scala/inox/solvers/unrolling/LambdaTemplates.scala
@@ -14,6 +14,7 @@ trait LambdaTemplates { self: Templates =>
import lambdasManager._
import datatypesManager._
+ import quantificationsManager._
/** Represents a POTENTIAL application of a first-class function in the unfolding procedure
*
@@ -83,7 +84,7 @@ trait LambdaTemplates { self: Templates =>
clauses, blockers, applications, matchers,
lambdas, quantifications,
structure,
- lambda, lambdaString
+ lambda, lambdaString, false
)
}
}
@@ -177,7 +178,7 @@ trait LambdaTemplates { self: Templates =>
val substituter = mkSubstituter(substMap.mapValues(_.encoded))
val deps = dependencies.map(substituter)
- val key = (lambda, pathVar._2, deps)
+ val key = (lambda, blockerPath(pathVar._2), deps)
val sortedDeps = exprOps.variablesOf(lambda).toSeq.sortBy(_.id.uniqueName)
val locals = sortedDeps zip deps
@@ -190,6 +191,10 @@ trait LambdaTemplates { self: Templates =>
}
override def hashCode: Int = key.hashCode
+
+ def subsumes(that: LambdaStructure): Boolean = {
+ key._1 == that.key._1 && key._3 == that.key._3 && key._2.subsetOf(that.key._2)
+ }
}
class LambdaTemplate private (
@@ -208,7 +213,8 @@ trait LambdaTemplates { self: Templates =>
val quantifications: Seq[QuantificationTemplate],
val structure: LambdaStructure,
val lambda: Lambda,
- private[unrolling] val stringRepr: () => String) extends Template {
+ private[unrolling] val stringRepr: () => String,
+ private val isConcrete: Boolean) extends Template {
val args = arguments.map(_._2)
val tpe = bestRealType(ids._1.getType).asInstanceOf[FunctionType]
@@ -224,10 +230,11 @@ trait LambdaTemplates { self: Templates =>
lambdas.map(_.substitute(substituter, msubst)),
quantifications.map(_.substitute(substituter, msubst)),
structure.substitute(substituter, msubst),
- lambda, stringRepr)
+ lambda, stringRepr, isConcrete)
/** This must be called right before returning the clauses in [[structure.instantiation]]! */
def concretize(idT: Encoded): LambdaTemplate = {
+ assert(!isConcrete, "Can't concretize concrete lambda template")
val substituter = mkSubstituter(Map(ids._2 -> idT) ++ (closures.map(_._2) zip structure.locals.map(_._2)))
new LambdaTemplate(
ids._1 -> idT,
@@ -238,7 +245,7 @@ trait LambdaTemplates { self: Templates =>
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)
+ structure, lambda, stringRepr, true)
}
override def instantiate(blocker: Encoded, args: Seq[Arg]): Clauses = {
@@ -262,6 +269,11 @@ trait LambdaTemplates { self: Templates =>
mkSubstituter(Map(vT -> caller) ++ (asT zip args))(app)
}
+ def mkFlatApp(caller: Encoded, tpe: FunctionType, args: Seq[Encoded]): Encoded = tpe.to match {
+ case ft: FunctionType => mkFlatApp(mkApp(caller, tpe, args.take(tpe.from.size)), ft, args.drop(tpe.from.size))
+ case _ => mkApp(caller, tpe, args)
+ }
+
def registerFunction(b: Encoded, tpe: FunctionType, f: Encoded): Clauses = {
val ft = bestRealType(tpe).asInstanceOf[FunctionType]
freeFunctions += ft -> (freeFunctions(ft) + (b -> f))
@@ -296,48 +308,50 @@ trait LambdaTemplates { self: Templates =>
}
def instantiateLambda(template: LambdaTemplate): (Encoded, Clauses) = {
- byType(template.tpe).get(template.structure) match {
- case Some(template) =>
- (template.ids._2, Seq.empty)
-
- case None =>
- val idT = encodeSymbol(template.ids._1)
- val newTemplate = template.concretize(idT)
+ byType(template.tpe).get(template.structure).map {
+ t => (t.ids._2, Seq.empty)
+ }.orElse {
+ byType(template.tpe).collectFirst {
+ case (s, t) if s subsumes template.structure => (t.ids._2, Seq.empty)
+ }
+ }.getOrElse {
+ val idT = encodeSymbol(template.ids._1)
+ val newTemplate = template.concretize(idT)
- val orderingClauses = newTemplate.structure.locals.flatMap {
- case (v, dep) => registerClosure(newTemplate.start, idT -> newTemplate.tpe, dep -> v.tpe)
- }
+ val orderingClauses = newTemplate.structure.locals.flatMap {
+ case (v, dep) => registerClosure(newTemplate.start, idT -> newTemplate.tpe, dep -> v.tpe)
+ }
- val extClauses = for ((oldB, freeF) <- freeBlockers(newTemplate.tpe) if canEqual(freeF, idT)) yield {
- val nextB = encodeSymbol(Variable(FreshIdentifier("b_or", true), BooleanType))
- val ext = mkOr(mkAnd(newTemplate.start, mkEquals(idT, freeF)), nextB)
- mkEquals(oldB, ext)
- }
+ val extClauses = for ((oldB, freeF) <- freeBlockers(newTemplate.tpe) if canEqual(freeF, idT)) yield {
+ val nextB = encodeSymbol(Variable(FreshIdentifier("b_or", true), BooleanType))
+ val ext = mkOr(mkAnd(newTemplate.start, mkEquals(idT, freeF)), nextB)
+ mkEquals(oldB, ext)
+ }
- val arglessEqClauses = if (newTemplate.tpe.from.nonEmpty) Seq.empty[Encoded] else {
- for ((b,f) <- freeFunctions(newTemplate.tpe) if canEqual(idT, f)) yield {
- val (tmplApp, fApp) = (mkApp(idT, newTemplate.tpe, Seq.empty), mkApp(f, newTemplate.tpe, Seq.empty))
- mkImplies(mkAnd(b, newTemplate.start, mkEquals(tmplApp, fApp)), mkEquals(idT, f))
- }
+ val arglessEqClauses = if (newTemplate.tpe.from.nonEmpty) Seq.empty[Encoded] else {
+ for ((b,f) <- freeFunctions(newTemplate.tpe) if canEqual(idT, f)) yield {
+ val (tmplApp, fApp) = (mkApp(idT, newTemplate.tpe, Seq.empty), mkApp(f, newTemplate.tpe, Seq.empty))
+ mkImplies(mkAnd(b, newTemplate.start, mkEquals(tmplApp, fApp)), mkEquals(idT, f))
}
+ }
- // make sure we have sound equality between the new lambda and previously defined ones
- val clauses = newTemplate.structure.instantiation ++
- equalityClauses(newTemplate) ++
- orderingClauses ++
- extClauses ++
- arglessEqClauses
+ // make sure we have sound equality between the new lambda and previously defined ones
+ val clauses = newTemplate.structure.instantiation ++
+ equalityClauses(newTemplate) ++
+ orderingClauses ++
+ extClauses ++
+ arglessEqClauses
- byID += idT -> newTemplate
- byType += newTemplate.tpe -> (byType(newTemplate.tpe) + (newTemplate.structure -> newTemplate))
+ byID += idT -> newTemplate
+ byType += newTemplate.tpe -> (byType(newTemplate.tpe) + (newTemplate.structure -> newTemplate))
- val gen = nextGeneration(currentGeneration)
- for (app @ (_, App(caller, _, args, _)) <- applications(newTemplate.tpe)) {
- val cond = mkAnd(newTemplate.start, mkEquals(idT, caller))
- registerAppBlocker(gen, app, Left(newTemplate), cond, args)
- }
+ val gen = nextGeneration(currentGeneration)
+ for (app @ (_, App(caller, _, args, _)) <- applications(newTemplate.tpe)) {
+ val cond = mkAnd(newTemplate.start, mkEquals(idT, caller))
+ registerAppBlocker(gen, app, Left(newTemplate), cond, args)
+ }
- (idT, clauses)
+ (idT, clauses)
}
}
diff --git a/src/main/scala/inox/solvers/unrolling/QuantificationTemplates.scala b/src/main/scala/inox/solvers/unrolling/QuantificationTemplates.scala
index 46d591a37568a05be17bfe8acd31a820b455188f..4e5bed2d032faf1933f3297bf4e5fe288d71e36d 100644
--- a/src/main/scala/inox/solvers/unrolling/QuantificationTemplates.scala
+++ b/src/main/scala/inox/solvers/unrolling/QuantificationTemplates.scala
@@ -81,8 +81,8 @@ trait QuantificationTemplates { self: Templates =>
*
* Instantiations of unknown polarity quantification with body {{{p}}} follows the schema:
* {{{
- * b ==> (q == (q2 && inst)
- * b ==> (inst == (guard ==> p))
+ * q == (q2 && inst)
+ * inst == (guard ==> p)
* }}}
* It is useful to keep the two clauses separate so that satisfying assignments can be
* constructed where only certain `inst` variables are falsified. This is used to enable
@@ -103,7 +103,7 @@ trait QuantificationTemplates { self: Templates =>
val matchers: Matchers,
val lambdas: Seq[LambdaTemplate],
val quantifications: Seq[QuantificationTemplate],
- val key: (Seq[ValDef], Expr, Seq[Encoded]),
+ val key: (Encoded, Seq[ValDef], Expr, Seq[Encoded]),
val body: Expr,
stringRepr: () => String) {
@@ -122,7 +122,7 @@ trait QuantificationTemplates { self: Templates =>
matchers.map { case (b, ms) => substituter(b) -> ms.map(_.substitute(substituter, msubst)) },
lambdas.map(_.substitute(substituter, msubst)),
quantifications.map(_.substitute(substituter, msubst)),
- (key._1, key._2, key._3.map(substituter)),
+ (substituter(key._1), key._2, key._3, key._4.map(substituter)),
body, stringRepr)
private lazy val str : String = stringRepr()
@@ -197,7 +197,8 @@ trait QuantificationTemplates { self: Templates =>
extraGuarded merge guardedExprs, extraEqs ++ equations,
lambdas, quantifications, substMap = substMap ++ extraSubst)
- val key = templateKey(proposition.args, proposition.body, substMap)
+ val tk = templateKey(proposition.args, proposition.body, substMap)
+ val key = (pathVar._2, tk._1, tk._2, tk._3)
(optVar, new QuantificationTemplate(
pathVar, polarity, quantifiers, condVars, exprVars, condTree, clauses,
@@ -218,8 +219,8 @@ trait QuantificationTemplates { self: Templates =>
val handledSubsts = new IncrementalMap[Quantification, Set[(Set[Encoded], Map[Encoded,Arg])]]
val ignoredGrounds = new IncrementalMap[Int, Set[Quantification]]
- val lambdaAxioms = new IncrementalSet[(LambdaStructure, Seq[(Variable, Encoded)])]
- val templates = new IncrementalMap[(Seq[ValDef], Expr, Seq[Encoded]), Map[Encoded, Encoded]]
+ val lambdaAxioms = new IncrementalSet[LambdaStructure]
+ val templates = new IncrementalMap[(Encoded, Seq[ValDef], Expr, Seq[Encoded]), (QuantificationTemplate, Map[Encoded, Encoded])]
val incrementals: Seq[IncrementalState] = Seq(quantifications, lambdaAxioms, templates,
ignoredMatchers, handledMatchers, ignoredSubsts, handledSubsts, ignoredGrounds)
@@ -338,14 +339,14 @@ trait QuantificationTemplates { self: Templates =>
@inline
private def matcherKey(m: Matcher): MatcherKey = matcherKey(m.key)
- private def correspond(k1: MatcherKey, k2: MatcherKey): Option[Boolean] = (k1, k2) match {
+ protected def correspond(k1: MatcherKey, k2: MatcherKey): Option[Boolean] = (k1, k2) match {
case (`k2`, _) => Some(true)
case (tp1: TypedKey, tp2: TypedKey) if tp1.tpe == tp2.tpe => Some(false)
case _ => None
}
@inline
- private def correspond(m1: Matcher, m2: Matcher): Option[Boolean] =
+ protected def correspond(m1: Matcher, m2: Matcher): Option[Boolean] =
correspond(matcherKey(m1), matcherKey(m2))
private trait BlockedSet[Element] extends Iterable[(Set[Encoded], Element)] with IncrementalState {
@@ -691,6 +692,14 @@ trait QuantificationTemplates { self: Templates =>
}
}
+ for (tmpl <- lambdas.map(t => byID(substituter(t.ids._2)))) {
+ instantiation ++= instantiateAxiom(tmpl)
+ }
+
+ for ((_, apps) <- applications; App(caller, _, _, _) <- apps; tmpl <- byID.get(substituter(caller))) {
+ instantiation ++= instantiateAxiom(tmpl)
+ }
+
instantiation.toSeq
}
@@ -821,63 +830,54 @@ trait QuantificationTemplates { self: Templates =>
}
def instantiateAxiom(template: LambdaTemplate): Clauses = {
- val quantifiers = template.arguments.map { p => p._1.freshen -> encodeSymbol(p._1) }
-
- val app = mkApplication(template.ids._1, quantifiers.map(_._1))
- val appT = mkEncoder(quantifiers.toMap + template.ids)(app)
- val selfMatcher = Matcher(Left(template.ids._2 -> template.tpe), quantifiers.map(p => Left(p._2)), appT)
-
- val blocker = Variable(FreshIdentifier("blocker", true), BooleanType)
- val blockerT = encodeSymbol(blocker)
-
- val guard = Variable(FreshIdentifier("guard", true), BooleanType)
- val guardT = encodeSymbol(guard)
-
- val enablingClause = mkEquals(mkAnd(guardT, template.start), blockerT)
-
- /* Compute Axiom's unique key to avoid redudant instantiations */
+ if (lambdaAxioms(template.structure) || lambdaAxioms.exists(s => s.subsumes(template.structure))) {
+ Seq.empty
+ } else {
+ lambdaAxioms += template.structure
+ val quantifiers = template.arguments
+ val app = mkFlatApp(template.ids._2, template.tpe, quantifiers.map(_._2))
+ val matcher = Matcher(Left(template.ids._2 -> template.tpe), quantifiers.map(p => Left(p._2)), app)
+
+ val guard = encodeSymbol(Variable(FreshIdentifier("guard", true), BooleanType))
+ val substituter = mkSubstituter(Map(template.start -> guard))
+
+ val body: Expr = {
+ def rec(caller: Expr, body: Expr): Expr = body match {
+ case Lambda(args, body) => rec(Application(caller, args.map(_.toVariable)), body)
+ case _ => Equals(caller, body)
+ }
+ rec(template.ids._1, template.structure.lambda)
+ }
- def flattenLambda(e: Expr): (Seq[ValDef], Expr) = e match {
- case Lambda(args, body) =>
- val (recArgs, recBody) = flattenLambda(body)
- (args ++ recArgs, recBody)
- case _ => (Seq.empty, e)
+ val tk = QuantificationTemplate.templateKey(
+ quantifiers.map(_._1.toVal),
+ body,
+ template.structure.locals.toMap + template.ids
+ )
+ val key = (template.pathVar._2, tk._1, tk._2, tk._3)
+
+ instantiateQuantification(new QuantificationTemplate(
+ template.pathVar,
+ Positive(guard),
+ quantifiers,
+ template.condVars,
+ template.exprVars,
+ template.condTree,
+ template.clauses map substituter,
+ template.blockers.map { case (b, fis) => substituter(b) -> fis.map(_.substitute(substituter, Map.empty)) },
+ template.applications.map { case (b, fas) => substituter(b) -> fas.map(_.substitute(substituter, Map.empty)) },
+ template.matchers.map { case (b, ms) =>
+ substituter(b) -> ms.map(_.substitute(substituter, Map.empty))
+ } merge Map(guard -> Set(matcher)),
+ template.lambdas.map(_.substitute(substituter, Map.empty)),
+ template.quantifications.map(_.substitute(substituter, Map.empty)),
+ key, body, template.stringRepr))._2 // mapping is guaranteed empty!!
}
-
- val (structArgs, structBody) = flattenLambda(template.structure.lambda)
- assert(quantifiers.size == structArgs.size, "Expecting lambda templates to contain flattened lamdbas")
-
- val lambdaBody = exprOps.replaceFromSymbols((structArgs zip quantifiers.map(_._1)).toMap, structBody)
- val quantBody = Equals(app, lambdaBody)
-
- val substMap = template.structure.locals.toMap + template.ids
-
- val key = QuantificationTemplate.templateKey(quantifiers.map(_._1.toVal), quantBody, substMap)
-
- val substituter = mkSubstituter((template.args zip quantifiers.map(_._2)).toMap + (template.start -> blockerT))
- val msubst = Map.empty[Encoded, Matcher]
-
- instantiateQuantification(new QuantificationTemplate(
- template.pathVar,
- Positive(guardT),
- quantifiers,
- template.condVars + (blocker -> blockerT),
- template.exprVars,
- template.condTree,
- (template.clauses map substituter) :+ enablingClause,
- template.blockers.map { case (b, fis) => substituter(b) -> fis.map(_.substitute(substituter, msubst)) },
- template.applications.map { case (b, fas) => substituter(b) -> fas.map(_.substitute(substituter, msubst)) },
- template.matchers.map { case (b, ms) =>
- substituter(b) -> ms.map(_.substitute(substituter, msubst))
- } merge Map(blockerT -> Set(selfMatcher)),
- template.lambdas.map(_.substitute(substituter, msubst)),
- template.quantifications.map(_.substitute(substituter, msubst)),
- key, quantBody, template.stringRepr))._2 // mapping is guaranteed empty!!
}
def instantiateQuantification(template: QuantificationTemplate): (Map[Encoded, Encoded], Clauses) = {
templates.get(template.key) match {
- case Some(map) =>
+ case Some((_, map)) =>
(map, Seq.empty)
case None =>
@@ -908,9 +908,8 @@ trait QuantificationTemplates { self: Templates =>
clauses ++= substClauses
// this will call `instantiateMatcher` on all matchers in `template.matchers`
- val instClauses = Template.instantiate(template.clauses,
+ clauses ++= Template.instantiate(template.clauses,
template.blockers, template.applications, template.matchers, substMap)
- clauses ++= instClauses
Map(insts._2 -> instT)
@@ -931,7 +930,8 @@ trait QuantificationTemplates { self: Templates =>
clauses ++= quantification.instantiate(bs, m)
}
- val freshSubst = mkSubstituter(template.quantifiers.map(p => p._2 -> encodeSymbol(p._1)).toMap)
+ val freshQuantifiers = template.quantifiers.map(p => encodeSymbol(p._1))
+ val freshSubst = mkSubstituter((template.quantifiers.map(_._2) zip freshQuantifiers).toMap)
for ((b,ms) <- template.matchers; m <- ms) {
clauses ++= instantiateMatcher(Set.empty[Encoded], m, false)
// it is very rare that such instantiations are actually required, so we defer them
@@ -943,7 +943,7 @@ trait QuantificationTemplates { self: Templates =>
Map(qs._2 -> qT)
}
- templates += template.key -> mapping
+ templates += template.key -> ((template, mapping))
(mapping, clauses.toSeq)
}
}