diff --git a/src/main/scala/leon/solvers/templates/QuantificationManager.scala b/src/main/scala/leon/solvers/templates/QuantificationManager.scala
index ae69427dceeec55049c8158437266720b3ed4c62..57dc368eb2bc5d467e56129cd91c45f21dccb999 100644
--- a/src/main/scala/leon/solvers/templates/QuantificationManager.scala
+++ b/src/main/scala/leon/solvers/templates/QuantificationManager.scala
@@ -67,27 +67,6 @@ object QuantificationTemplate {
class QuantificationManager[T](encoder: TemplateEncoder[T]) extends LambdaManager[T](encoder) {
- private val stdQuantifiers: MutableMap[TypeTree, Seq[T]] = MutableMap.empty
- private val quantified: MutableSet[T] = MutableSet.empty
-
- private def standardQuantifiers(tpe: TypeTree, count: Int): Seq[T] = {
- val quantifiers = stdQuantifiers.getOrElse(tpe, Seq.empty)
- val currentCount = quantifiers.size
-
- if (currentCount >= count) quantifiers.take(count) else {
- val newQuantifiers = List.range(0, count - currentCount).map(_ => encoder.encodeId(FreshIdentifier("x", tpe)))
- quantified ++= newQuantifiers
-
- val allQuantifiers = quantifiers ++ newQuantifiers
- stdQuantifiers(tpe) = allQuantifiers
- allQuantifiers
- }
- }
-
- private def freshQuantifierSubst: Map[T, T] = stdQuantifiers.flatMap { case (tpe, ids) =>
- ids zip List.range(0, ids.size).map(_ => encoder.encodeId(FreshIdentifier("x", tpe)))
- }.toMap
-
private val nextHolder: () => T = {
val id: Identifier = FreshIdentifier("ph", BooleanType)
() => encoder.encodeId(id)
@@ -98,47 +77,30 @@ class QuantificationManager[T](encoder: TemplateEncoder[T]) extends LambdaManage
() => encoder.encodeId(id)
}
- private type Bindings = Set[(Option[T], TypeTree, Int, T)]
- private var bindingsStack: List[Bindings] = List(Set.empty)
- private def bindings: Bindings = bindingsStack.head
- private def bindings_=(bs: Bindings): Unit = {
- bindingsStack = bs :: bindingsStack.tail
- }
-
private var quantificationsStack: List[Seq[Quantification]] = List(Seq.empty)
private def quantifications: Seq[Quantification] = quantificationsStack.head
private def quantifications_=(qs: Seq[Quantification]): Unit = {
quantificationsStack = qs :: quantificationsStack.tail
}
- private var instantiatedMatchersStack: List[Seq[(T, Matcher[T], Map[T,T])]] = List(Seq.empty)
- private def instantiatedMatchers: Seq[(T, Matcher[T], Map[T,T])] = instantiatedMatchersStack.head
- private def instantiatedMatchers_=(ias: Seq[(T, Matcher[T], Map[T,T])]): Unit = {
- instantiatedMatchersStack = ias :: instantiatedMatchersStack.tail
- }
-
- private var boundMatchersStack: List[Set[(T, Matcher[T])]] = List(Set.empty)
- private def boundMatchers: Set[(T, Matcher[T])] = boundMatchersStack.head
- private def boundMatchers_=(bas: Set[(T, Matcher[T])]): Unit = {
- boundMatchersStack = bas :: boundMatchersStack.tail
+ private var instantiatedStack: List[Set[(T, Matcher[T])]] = List(Set.empty)
+ private def instantiated: Set[(T, Matcher[T])] = instantiatedStack.head
+ private def instantiated_=(ias: Set[(T, Matcher[T])]): Unit = {
+ instantiatedStack = ias :: instantiatedStack.tail
}
private var knownStack: List[Set[T]] = List(Set.empty)
private def known(idT: T): Boolean = knownStack.head(idT) || byID.isDefinedAt(idT)
override def push(): Unit = {
- bindingsStack = bindings :: bindingsStack
quantificationsStack = quantifications :: quantificationsStack
- instantiatedMatchersStack = instantiatedMatchers :: instantiatedMatchersStack
- boundMatchersStack = boundMatchers :: boundMatchersStack
+ instantiatedStack = instantiated :: instantiatedStack
knownStack = knownStack.head :: knownStack
}
override def pop(lvl: Int): Unit = {
- bindingsStack = bindingsStack.drop(lvl)
quantificationsStack = quantificationsStack.drop(lvl)
- instantiatedMatchersStack = instantiatedMatchersStack.drop(lvl)
- boundMatchersStack = boundMatchersStack.drop(lvl)
+ instantiatedStack = instantiatedStack.drop(lvl)
knownStack = knownStack.drop(lvl)
}
@@ -154,6 +116,7 @@ class QuantificationManager[T](encoder: TemplateEncoder[T]) extends LambdaManage
val holdVar: T,
val guardVar: T,
var currentHolder: T,
+ val quantified: Set[T],
val condVars: Map[Identifier, T],
val exprVars: Map[Identifier, T],
val clauses: Seq[T],
@@ -163,11 +126,11 @@ class QuantificationManager[T](encoder: TemplateEncoder[T]) extends LambdaManage
val lambdas: Map[T, LambdaTemplate[T]]) {
def this(
- qVar: T, holdVar: T, guardVar: T,
+ qVar: T, holdVar: T, guardVar: T, quantified: Set[T],
condVars: Map[Identifier, T], exprVars: Map[Identifier, T],
clauses: Seq[T], blockers: Map[T, Set[TemplateCallInfo[T]]], applications: Map[T, Set[App[T]]],
matchers: Set[Matcher[T]], lambdas: Map[T, LambdaTemplate[T]]) = {
- this(qVar, holdVar, guardVar, nextHolder(),
+ this(qVar, holdVar, guardVar, nextHolder(), quantified,
condVars, exprVars, clauses, blockers, applications, matchers, lambdas)
}
@@ -176,7 +139,7 @@ class QuantificationManager[T](encoder: TemplateEncoder[T]) extends LambdaManage
new Quantification (
qVar, holdVar, guardVar, currentHolder,
- condVars, exprVars,
+ quantified, condVars, exprVars,
clauses map substituter,
blockers map { case (b, fis) =>
substituter(b) -> fis.map(fi => fi.copy(args = fi.args.map(substituter)))
@@ -191,7 +154,7 @@ class QuantificationManager[T](encoder: TemplateEncoder[T]) extends LambdaManage
)
}
- def instantiate(blocker: T, matcher: Matcher[T], quantifierSubst: Map[T, T]): Instantiation[T] = {
+ def instantiate(blocker: T, matcher: Matcher[T]): Instantiation[T] = {
val Matcher(caller, tpe, args) = matcher
// Build a mapping from applications in the quantified statement to all potential concrete
@@ -209,22 +172,19 @@ class QuantificationManager[T](encoder: TemplateEncoder[T]) extends LambdaManage
if (qm == bindingMatcher) {
bindingMatcher -> Set(blocker -> matcher)
} else {
- val instances: Seq[(T, Matcher[T])] = instantiatedMatchers.collect {
- case (b, m @ Matcher(caller, tpe, _), _) if tpe == qtpe && (qcaller == caller || !known(caller)) => (b, m)
+ val instances: Set[(T, Matcher[T])] = instantiated.filter {
+ case (b, m @ Matcher(caller, tpe, _)) => tpe == qtpe && (qcaller == caller || !known(caller))
}
// concrete applications can appear multiple times in the constraint, and this is also the case
// for the current application for which we are generating the constraints
val withCurrent = if (tpe == qtpe && (qcaller == caller || !known(caller))) {
- instances :+ (blocker -> matcher)
+ instances + (blocker -> matcher)
} else instances
- // add quantified application to instances for constraints that depend on free variables
- // this also make sure that constraints that don't depend on all variables will also be instantiated
- // Note: we can use `blocker` here as the blocker since it is guaranteed true in this branch
- val withAll = withCurrent :+ (blocker -> qm.copy(args = qm.args.map(a => quantifierSubst.getOrElse(a, a))))
+ println(qm -> withCurrent)
- qm -> withAll
+ qm -> withCurrent
}
}
// 2.2. based on the possible bindings for each quantified application, build a set of
@@ -247,41 +207,24 @@ class QuantificationManager[T](encoder: TemplateEncoder[T]) extends LambdaManage
_ = constraints :+= b
_ = if (qcaller != caller) constraints :+= encoder.mkEquals(qcaller, caller)
(qarg, arg) <- (qargs zip args)
- } if (subst.isDefinedAt(qarg) || !quantified(qarg)) {
+ } if (subst.isDefinedAt(qarg)) {
+ constraints :+= encoder.mkEquals(subst(qarg), arg)
+ } else if (!quantified(qarg)) {
constraints :+= encoder.mkEquals(qarg, arg)
} else {
subst += qarg -> arg
}
- for ((q,nq) <- quantifierSubst if !subst.isDefinedAt(q)) {
- subst += q -> nq
- }
-
val enabler = if (constraints.size == 1) constraints.head else encoder.mkAnd(constraints : _*)
val newHolder = nextHolder()
+ val baseSubstMap = (condVars ++ exprVars).map { case (id, idT) => idT -> encoder.encodeId(id) }
val lambdaSubstMap = lambdas map { case (idT, lambda) => idT -> encoder.encodeId(lambda.id) }
- val substMap = subst ++ lambdaSubstMap + (qVar -> currentHolder) + (guardVar -> enabler) + (holdVar -> newHolder)
- val substituter = encoder.substitute(substMap)
-
- val newClauses = clauses map substituter
- val newBlockers = blockers map { case (b, fis) =>
- substituter(b) -> fis.map(fi => fi.copy(args = fi.args.map(substituter)))
- }
-
- instantiation ++= (newClauses, newBlockers, Map.empty)
-
- for ((idT, lambda) <- lambdas) {
- val newIdT = substituter(idT)
- val newTemplate = lambda.substitute(substMap)
- instantiation ++= instantiateLambda(newIdT, newTemplate)
- }
-
- for ((b, apps) <- applications; bp = substituter(b); app <- apps) {
- val newApp = app.copy(caller = substituter(app.caller), args = app.args.map(substituter))
- instantiation ++= instantiateApp(bp, newApp)
- }
+ val substMap = subst ++ baseSubstMap ++ lambdaSubstMap +
+ (qVar -> currentHolder) + (guardVar -> enabler) + (holdVar -> newHolder)
+ instantiation ++= Template.instantiate(encoder, QuantificationManager.this,
+ clauses, blockers, applications, Seq.empty, Map.empty, lambdas, substMap)
currentHolder = newHolder
}
@@ -291,106 +234,56 @@ class QuantificationManager[T](encoder: TemplateEncoder[T]) extends LambdaManage
def instantiateQuantification(template: QuantificationTemplate[T], substMap: Map[T, T]): Instantiation[T] = {
- val (quantification, matchers) = {
- val quantified = template.quantifiers.map(_._2).toSet
-
- val allMatchers: Set[Matcher[T]] = {
- def rec(templates: Map[T, LambdaTemplate[T]]): Set[Matcher[T]] = templates.flatMap {
- case (_, template) => template.matchers.flatMap(_._2).toSet ++ rec(template.lambdas)
- }.toSet
-
- val allMatchers = template.matchers.flatMap(_._2).toSet ++ rec(template.lambdas)
- for (m @ Matcher(caller, tpe, args) <- allMatchers if args exists quantified) yield m
- }
+ val instantiationSubst: Map[T, T] = substMap +
+ (template.guardVar -> encoder.encodeExpr(Map.empty)(BooleanLiteral(true)))
- val q = new Quantification(
- template.qs._2,
- template.holdVar,
- template.guardVar,
- template.qs._2, // this Quantification will never be instantiated, so this increases sanity
- template.condVars,
- template.exprVars,
- template.clauses,
- template.blockers,
- template.applications,
- allMatchers,
- template.lambdas
- )
-
- val tpeCounts = template.quantifiers.groupBy(_._1.getType).mapValues(_.map(_._2).toSeq)
- val qSubst = tpeCounts.flatMap { case (tpe, idTs) => idTs zip standardQuantifiers(tpe, idTs.size) }.toMap
- val subst = substMap ++ qSubst
-
- val quantification = q.substitute(subst)
-
- val substituter = encoder.substitute(subst)
- val matchers = template.matchers.map { case (b, ms) =>
- substituter(b) -> ms.map(m => m.copy(caller = substituter(m.caller), args = m.args.map(substituter)))
- }
-
- (quantification, matchers)
+ val substituter = encoder.substitute(instantiationSubst)
+ val matchers = template.matchers.map { case (b, ms) =>
+ substituter(b) -> ms.map(m => m.copy(caller = substituter(m.caller), args = m.args.map(substituter)))
}
- val quantifierSubst: Map[T,T] = freshQuantifierSubst
-
var instantiation: Instantiation[T] = Template.instantiate(encoder, this,
- quantification.clauses, quantification.blockers, quantification.applications,
- Seq.empty, matchers, quantification.lambdas,
- quantifierSubst + (quantification.guardVar -> encoder.encodeExpr(Map.empty)(BooleanLiteral(true)))
- )
-
- val qBindings: Bindings = quantification.matchers.flatMap {
- case Matcher(caller, tpe, args) => args.zipWithIndex.collect {
- case (qid, idx) if quantified(qid) =>
- (if (known(caller)) Some(caller) else None, tpe, idx, qid)
- }
- }
+ template.clauses, template.blockers, template.applications,
+ Seq.empty, Map.empty, template.lambdas, instantiationSubst)
- val (callerBindings, typeBindings) = (bindings ++ qBindings).partition(_._1.isDefined)
+ val quantified = template.quantifiers.map(_._2).toSet
- val callerMap: Map[(T, Int), Set[T]] = callerBindings.groupBy(p => (p._1.get, p._3)).mapValues(_.map(_._4))
- val typeMap: Map[(TypeTree, Int), Set[T]] = typeBindings.groupBy(p => (p._2, p._3)).mapValues(_.map(_._4))
+ val allMatchers: Set[Matcher[T]] = {
+ def rec(templates: Map[T, LambdaTemplate[T]]): Set[Matcher[T]] = templates.flatMap {
+ case (_, template) => template.matchers.flatMap(_._2).toSet ++ rec(template.lambdas)
+ }.toSet
- val pairs: Set[(T, T)] = qBindings.flatMap { case (optIdT, tpe, idx, q) =>
- val matches = typeMap.getOrElse(tpe -> idx, Set.empty) ++ optIdT.toSeq.flatMap(idT => callerMap(idT -> idx))
- matches.map(q2 => q -> q2)
+ val allMatchers = template.matchers.flatMap(_._2).toSet ++ rec(template.lambdas)
+ for (m @ Matcher(caller, tpe, args) <- allMatchers if args exists quantified) yield m
}
- val mappings: List[Map[T, T]] =
- pairs.groupBy(_._1).toSeq.foldLeft(List(Map.empty[T, T])) {
- case (mappings, (_, pairs)) => pairs.toList.flatMap(p => mappings.map(mapping => mapping + p))
+ val matchQuorums: Seq[Set[Matcher[T]]] = allMatchers.subsets.filter { ms =>
+ var doubled: Boolean = false
+ var qs: Set[T] = Set.empty
+ for (m @ Matcher(_, _, args) <- ms) {
+ val qargs = (args filter quantified).toSet
+ if ((qs & qargs).nonEmpty) doubled = true
+ qs ++= qargs
}
- val newQuantifications = for (mapping <- mappings) yield {
- val newQ = encoder.encodeId(FreshIdentifier("q", BooleanType))
-
- val freshConds = quantification.condVars.map(p => p._1.freshen -> p._2)
- val freshExprs = quantification.exprVars.map(p => p._1.freshen -> p._2)
+ !doubled && (qs == quantified)
+ }.toSeq
- val substMap: Map[T, T] = mapping ++
- (freshConds ++ freshExprs).map { case (id, idT) => idT -> encoder.encodeId(id) } ++
- quantification.lambdas.map { case (idT, template) => idT -> encoder.encodeId(template.id) } +
- (quantification.qVar -> newQ)
-
- val substituter = encoder.substitute(substMap)
+ val newQuantifications = for (matchers <- matchQuorums) yield {
+ val newQ = nextQ()
new Quantification(newQ,
- quantification.holdVar, quantification.guardVar,
- newQ, // set the fresh qVar as `currentHolder` to ensure blocking before first unfolding
- freshConds mapValues substituter,
- freshExprs mapValues substituter,
- quantification.clauses map substituter,
- quantification.blockers map { case (b, fis) =>
- substituter(b) -> fis.map(fi => fi.copy(args = fi.args.map(substituter)))
- },
- quantification.applications map { case (b, fas) =>
- substituter(b) -> fas.map(fa => fa.copy(caller = substituter(fa.caller), args = fa.args.map(substituter)))
- },
- quantification.matchers map { case m @ Matcher(caller, _, args) =>
- m.copy(caller = substituter(caller), args = args.map(substituter))
- },
- quantification.lambdas map { case (idT, template) => substituter(idT) -> template.substitute(mapping) }
- )
+ template.holdVar, template.guardVar,
+ newQ, // set template `qVar` as `currentHolder` to ensure blocking before first unfolding
+ quantified,
+ template.condVars,
+ template.exprVars,
+ template.clauses,
+ template.blockers,
+ template.applications,
+ matchers,
+ template.lambdas
+ ).substitute(substMap)
}
val eqClause = {
@@ -401,39 +294,30 @@ class QuantificationManager[T](encoder: TemplateEncoder[T]) extends LambdaManage
instantiation = (instantiation._1 :+ eqClause, instantiation._2, instantiation._3)
- // ensure the `quantifierSubst` associated to each instantiated app covers all necessary
- // parameters for the current new quantifications
- instantiatedMatchers = for ((b, m, qSubst) <- instantiatedMatchers) yield {
- val nqSubst = if (qSubst.size == stdQuantifiers.map(_._2.size).sum) qSubst else {
- stdQuantifiers.flatMap { case (tpe, ids) =>
- val recent = ids.dropWhile(qSubst.isDefinedAt)
- recent zip recent.map(_ => encoder.encodeId(FreshIdentifier("x", tpe)))
- }.toMap
- }
+ val saved = instantiated
- (b, m, nqSubst)
+ for ((b, ms) <- matchers; bp = substituter(b); m <- ms) {
+ val newM = m.copy(caller = substituter(m.caller), args = m.args.map(substituter))
+ instantiation ++= instantiateMatcher(bp, newM)
}
- quantifications ++= newQuantifications
-
- for ((b, m, qSubst) <- instantiatedMatchers; q <- newQuantifications) {
- instantiation ++= q.instantiate(b, m, qSubst)
+ for ((b, m) <- saved; q <- newQuantifications) {
+ instantiation ++= q.instantiate(b, m)
}
+ quantifications ++= newQuantifications
+
instantiation
}
def instantiateMatcher(blocker: T, matcher: Matcher[T]): Instantiation[T] = {
- val qInst = if (boundMatchers(blocker -> matcher)) Instantiation.empty[T] else {
- val quantifierSubst: Map[T, T] = freshQuantifierSubst
-
+ val qInst = if (instantiated(blocker -> matcher)) Instantiation.empty[T] else {
var instantiation = Instantiation.empty[T]
for (q <- quantifications) {
- instantiation ++= q.instantiate(blocker, matcher, quantifierSubst)
+ instantiation ++= q.instantiate(blocker, matcher)
}
- instantiatedMatchers :+= (blocker, matcher, quantifierSubst)
- boundMatchers += (blocker -> matcher)
+ instantiated += (blocker -> matcher)
instantiation
}
diff --git a/src/main/scala/leon/solvers/templates/Templates.scala b/src/main/scala/leon/solvers/templates/Templates.scala
index ab63924ef3918cbd664d72261dabf31d6edb1d3e..376c411c2fcbb9fbfc53be6549ae60f624c34cc0 100644
--- a/src/main/scala/leon/solvers/templates/Templates.scala
+++ b/src/main/scala/leon/solvers/templates/Templates.scala
@@ -70,7 +70,8 @@ trait Template[T] { self =>
}
val lambdaSubstMap = lambdas.map { case (idT, lambda) => idT -> encoder.encodeId(lambda.id) }
- val substMap : Map[T,T] = baseSubstMap ++ lambdaSubstMap + (start -> aVar)
+ val quantificationSubstMap = quantifications.map(q => q.qs._2 -> encoder.encodeId(q.qs._1))
+ val substMap : Map[T,T] = baseSubstMap ++ lambdaSubstMap ++ quantificationSubstMap + (start -> aVar)
Template.instantiate(encoder, manager,
clauses, blockers, applications, quantifications, matchers, lambdas, substMap)
@@ -273,7 +274,7 @@ object FunctionTemplate {
lambdas: Map[T, LambdaTemplate[T]],
isRealFunDef: Boolean
) : FunctionTemplate[T] = {
-
+
val (clauses, blockers, applications, matchers, templateString) =
Template.encode(encoder, pathVar, arguments, condVars, exprVars, guardedExprs, lambdas,
substMap = quantifications.map(q => q.qs).toMap,