From d49d33dbab679524408b5fbd4a0939e03a172fee Mon Sep 17 00:00:00 2001
From: Nicolas Voirol <voirol.nicolas@gmail.com>
Date: Fri, 19 Jun 2015 13:21:11 +0200
Subject: [PATCH] Extended e-matching to generic matchers
---
.../solvers/combinators/UnrollingSolver.scala | 4 +-
.../templates/QuantificationManager.scala | 501 +++++-------------
.../leon/solvers/templates/Templates.scala | 138 +++--
.../solvers/templates/UnrollingBank.scala | 4 +-
.../scala/leon/solvers/z3/FairZ3Solver.scala | 4 +-
5 files changed, 244 insertions(+), 407 deletions(-)
diff --git a/src/main/scala/leon/solvers/combinators/UnrollingSolver.scala b/src/main/scala/leon/solvers/combinators/UnrollingSolver.scala
index 494f4b9b6..aa936b283 100644
--- a/src/main/scala/leon/solvers/combinators/UnrollingSolver.scala
+++ b/src/main/scala/leon/solvers/combinators/UnrollingSolver.scala
@@ -152,7 +152,7 @@ class UnrollingSolver(val context: LeonContext, program: Program, underlying: So
reporter.debug(" - Running search...")
solver.push()
- solver.assertCnstr(andJoin((assumptions ++ unrollingBank.currentBlockers).toSeq))
+ solver.assertCnstr(andJoin((assumptions ++ unrollingBank.currentBlockers ++ unrollingBank.quantificationAssumptions).toSeq))
val res = solver.check
reporter.debug(" - Finished search with blocked literals")
@@ -188,7 +188,7 @@ class UnrollingSolver(val context: LeonContext, program: Program, underlying: So
}
solver.push()
- solver.assertCnstr(andJoin(assumptions.toSeq))
+ solver.assertCnstr(andJoin(assumptions.toSeq ++ unrollingBank.quantificationAssumptions))
val res2 = solver.check
res2 match {
diff --git a/src/main/scala/leon/solvers/templates/QuantificationManager.scala b/src/main/scala/leon/solvers/templates/QuantificationManager.scala
index 2b76e02a9..ae69427dc 100644
--- a/src/main/scala/leon/solvers/templates/QuantificationManager.scala
+++ b/src/main/scala/leon/solvers/templates/QuantificationManager.scala
@@ -12,6 +12,10 @@ import Instantiation._
import scala.collection.mutable.{Map => MutableMap, Set => MutableSet}
+case class Matcher[T](caller: T, tpe: TypeTree, args: Seq[T]) {
+ override def toString = "M(" + caller + " : " + tpe + ", " + args.mkString("(",",",")") + ")"
+}
+
class QuantificationTemplate[T](
val quantificationManager: QuantificationManager[T],
val start: T,
@@ -24,6 +28,7 @@ class QuantificationTemplate[T](
val clauses: Seq[T],
val blockers: Map[T, Set[TemplateCallInfo[T]]],
val applications: Map[T, Set[App[T]]],
+ val matchers: Map[T, Set[Matcher[T]]],
val lambdas: Map[T, LambdaTemplate[T]]) {
def instantiate(substMap: Map[T, T]): Instantiation[T] = {
@@ -50,13 +55,13 @@ object QuantificationTemplate {
val holders: (Identifier, T) = holder -> encoder.encodeId(holder)
val guards: (Identifier, T) = guard -> encoder.encodeId(guard)
- val (clauses, blockers, applications, _) =
+ val (clauses, blockers, applications, matchers, _) =
Template.encode(encoder, pathVar, quantifiers, condVars, exprVars, guardedExprs, lambdas,
substMap = subst + holders + guards + qs)
new QuantificationTemplate[T](quantificationManager,
pathVar._2, qs, holders._2, guards._2, quantifiers,
- condVars, exprVars, clauses, blockers, applications, lambdas)
+ condVars, exprVars, clauses, blockers, applications, matchers, lambdas)
}
}
@@ -93,7 +98,7 @@ class QuantificationManager[T](encoder: TemplateEncoder[T]) extends LambdaManage
() => encoder.encodeId(id)
}
- private type Bindings = Set[(Option[T], FunctionType, Int, T)]
+ 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 = {
@@ -106,32 +111,72 @@ class QuantificationManager[T](encoder: TemplateEncoder[T]) extends LambdaManage
quantificationsStack = qs :: quantificationsStack.tail
}
- private var instantiatedAppsStack: List[Seq[(T, App[T], Map[T,T])]] = List(Seq.empty)
- private def instantiatedApps: Seq[(T, App[T], Map[T,T])] = instantiatedAppsStack.head
- private def instantiatedApps_=(ias: Seq[(T, App[T], Map[T,T])]): Unit = {
- instantiatedAppsStack = ias :: instantiatedAppsStack.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 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
+ 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)
+ knownStack = knownStack.drop(lvl)
}
def blockers: Seq[T] = quantifications.map(_.holdVar)
- private def known(tpe: FunctionType, idT: T): Boolean = freeLambdas(tpe)(idT) || byID.isDefinedAt(idT)
+ override def registerFree(ids: Seq[(TypeTree, T)]): Unit = {
+ super.registerFree(ids)
+ knownStack = (knownStack.head ++ ids.map(_._2)) :: knownStack.tail
+ }
private class Quantification (
- var holdVar: T,
+ val qVar: T,
+ val holdVar: T,
val guardVar: T,
+ var currentHolder: T,
val condVars: Map[Identifier, T],
val exprVars: Map[Identifier, T],
val clauses: Seq[T],
val blockers: Map[T, Set[TemplateCallInfo[T]]],
val applications: Map[T, Set[App[T]]],
- val lambdas: Map[T, LambdaTemplate[T]],
- val binders: Set[App[T]]) {
+ val matchers: Set[Matcher[T]],
+ val lambdas: Map[T, LambdaTemplate[T]]) {
+
+ def this(
+ qVar: T, holdVar: T, guardVar: 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(),
+ condVars, exprVars, clauses, blockers, applications, matchers, lambdas)
+ }
def substitute(subst: Map[T, T]) = {
val substituter = encoder.substitute(subst)
new Quantification (
- holdVar, guardVar, condVars, exprVars,
+ qVar, holdVar, guardVar, currentHolder,
+ condVars, exprVars,
clauses map substituter,
blockers map { case (b, fis) =>
substituter(b) -> fis.map(fi => fi.copy(args = fi.args.map(substituter)))
@@ -139,64 +184,66 @@ class QuantificationManager[T](encoder: TemplateEncoder[T]) extends LambdaManage
applications map { case (b, fas) =>
substituter(b) -> fas.map(fa => fa.copy(caller = substituter(fa.caller), args = fa.args.map(substituter)))
},
- lambdas map { case (idT, template) => substituter(idT) -> template.substitute(subst) },
- binders map { case app @ App(caller, _, args) =>
- app.copy(caller = substituter(caller), args = args.map(substituter))
- }
+ matchers map { case m @ Matcher(caller, _, args) =>
+ m.copy(caller = substituter(caller), args = args.map(substituter))
+ },
+ lambdas map { case (idT, template) => substituter(idT) -> template.substitute(subst) }
)
}
- def instantiate(blocker: T, app: App[T], quantifierSubst: Map[T, T]): Instantiation[T] = {
- val App(caller, tpe, args) = app
+ def instantiate(blocker: T, matcher: Matcher[T], quantifierSubst: Map[T, T]): Instantiation[T] = {
+ val Matcher(caller, tpe, args) = matcher
// Build a mapping from applications in the quantified statement to all potential concrete
// applications previously encountered. Also make sure the current `app` is in the mapping
// as other instantiations have been performed previously when the associated applications
// were first encountered.
- val appMappings: List[List[(T, App[T], App[T])]] = binders.toList
+ val matcherMappings: Set[Set[(T, Matcher[T], Matcher[T])]] = matchers
// 1. select an application in the quantified proposition for which the current app can
// be bound when generating the new constraints
- .filter(qapp => qapp.caller == caller || (qapp.tpe == tpe && !known(qapp.tpe, qapp.caller)))
+ .filter(qm => qm.caller == caller || (qm.tpe == tpe && !known(qm.caller)))
// 2. build the instantiation mapping associated to the chosen current application binding
- .flatMap { bindingApp => binders
+ .flatMap { bindingMatcher => matchers
// 2.1. select all potential matches for each quantified application
- .map { case qapp @ App(qcaller, qtpe, qargs) =>
- if (qapp == bindingApp) {
- bindingApp -> Set(blocker -> app)
+ .map { case qm @ Matcher(qcaller, qtpe, qargs) =>
+ if (qm == bindingMatcher) {
+ bindingMatcher -> Set(blocker -> matcher)
} else {
- val instances: Seq[(T, App[T])] = instantiatedApps.collect {
- case (b, app @ App(caller, tpe, _), _) if tpe == qtpe && (qcaller == caller || !known(qtpe, caller)) => (b, app)
+ val instances: Seq[(T, Matcher[T])] = instantiatedMatchers.collect {
+ case (b, m @ Matcher(caller, tpe, _), _) if tpe == qtpe && (qcaller == caller || !known(caller)) => (b, m)
}
// 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 withApp = if (qcaller == caller || !known(tpe, caller)) instances :+ (blocker -> app) else instances
+ val withCurrent = if (tpe == qtpe && (qcaller == caller || !known(caller))) {
+ 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 = withApp :+ (blocker -> qapp)
+ val withAll = withCurrent :+ (blocker -> qm.copy(args = qm.args.map(a => quantifierSubst.getOrElse(a, a))))
- qapp -> withAll
+ qm -> withAll
}
}
// 2.2. based on the possible bindings for each quantified application, build a set of
// instantiation mappings that can be used to instantiate all necessary constraints
- .foldLeft[List[List[(T, App[T], App[T])]]] (List(Nil)) {
- case (mappings, (qapp, instances)) => instances.toList.flatMap {
- case (b, app) => mappings.map(mapping => mapping :+ (b, qapp, app))
- }
+ .foldLeft[Set[Set[(T, Matcher[T], Matcher[T])]]] (Set(Set.empty)) {
+ case (mappings, (qm, instances)) => Set(instances.toSeq.flatMap {
+ case (b, m) => mappings.map(mapping => mapping + ((b, qm, m)))
+ } : _*)
}
}
var instantiation = Instantiation.empty[T]
- for (mapping <- appMappings) {
+ for (mapping <- matcherMappings) {
var constraints: List[T] = Nil
var subst: Map[T, T] = Map.empty
for {
- (b, App(qcaller, _, qargs), App(caller, _, args)) <- mapping
+ (b, Matcher(qcaller, _, qargs), Matcher(caller, _, args)) <- mapping
_ = constraints :+= b
_ = if (qcaller != caller) constraints :+= encoder.mkEquals(qcaller, caller)
(qarg, arg) <- (qargs zip args)
@@ -211,10 +258,10 @@ class QuantificationManager[T](encoder: TemplateEncoder[T]) extends LambdaManage
}
val enabler = if (constraints.size == 1) constraints.head else encoder.mkAnd(constraints : _*)
- val holder = nextHolder()
+ val newHolder = nextHolder()
val lambdaSubstMap = lambdas map { case (idT, lambda) => idT -> encoder.encodeId(lambda.id) }
- val substMap = subst ++ lambdaSubstMap + (guardVar -> enabler) + (holdVar -> holder)
+ val substMap = subst ++ lambdaSubstMap + (qVar -> currentHolder) + (guardVar -> enabler) + (holdVar -> newHolder)
val substituter = encoder.substitute(substMap)
val newClauses = clauses map substituter
@@ -222,23 +269,20 @@ class QuantificationManager[T](encoder: TemplateEncoder[T]) extends LambdaManage
substituter(b) -> fis.map(fi => fi.copy(args = fi.args.map(substituter)))
}
- val newApplications = applications map { case (b, fas) =>
- substituter(b) -> fas.map(fa => fa.copy(caller = substituter(fa.caller), args = fa.args.map(substituter)))
- }
-
instantiation ++= (newClauses, newBlockers, Map.empty)
for ((idT, lambda) <- lambdas) {
val newIdT = substituter(idT)
val newTemplate = lambda.substitute(substMap)
- instantiation ++= QuantificationManager.super.instantiateLambda(newIdT, newTemplate)
+ instantiation ++= instantiateLambda(newIdT, newTemplate)
}
- for ((b, apps) <- newApplications; app <- apps) {
- instantiation ++= QuantificationManager.super.instantiateApp(b, app)
+ 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)
}
- holdVar = holder
+ currentHolder = newHolder
}
instantiation
@@ -247,67 +291,65 @@ class QuantificationManager[T](encoder: TemplateEncoder[T]) extends LambdaManage
def instantiateQuantification(template: QuantificationTemplate[T], substMap: Map[T, T]): Instantiation[T] = {
- val quantification: Quantification = {
+ val (quantification, matchers) = {
val quantified = template.quantifiers.map(_._2).toSet
- val bindingApps: Set[App[T]] = {
- def rec(templates: Map[T, LambdaTemplate[T]]): Set[App[T]] = templates.flatMap {
- case (_, template) => template.applications.flatMap(_._2).toSet ++ rec(template.lambdas)
+ 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 allApps = template.applications.flatMap(_._2).toSet ++ rec(template.lambdas)
- for (app @ App(caller, tpe, args) <- allApps if args exists quantified) yield app
+ val allMatchers = template.matchers.flatMap(_._2).toSet ++ rec(template.lambdas)
+ for (m @ Matcher(caller, tpe, args) <- allMatchers if args exists quantified) yield m
}
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,
- template.lambdas,
- bindingApps
+ 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
- q.substitute(substMap ++ qSubst)
- }
+ val subst = substMap ++ qSubst
- val quantifierSubst: Map[T,T] = freshQuantifierSubst
+ val quantification = q.substitute(subst)
- var qs: Seq[T] = Seq.empty
- var instantiation: Instantiation[T] = {
- val q = nextQ()
- qs :+= q
-
- val trueT = encoder.encodeExpr(Map.empty)(BooleanLiteral(true))
- val base = quantification.substitute(Map(
- quantification.guardVar -> trueT,
- quantification.holdVar -> trueT,
- template.qs._2 -> q
- ))
-
- var instantiation: Instantiation[T] = (base.clauses, base.blockers, Map.empty)
- for (q <- quantifications; (b, apps) <- quantification.applications; app <- apps) {
- instantiation ++= q.instantiate(b, app, quantifierSubst)
+ 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)))
}
- instantiation
+
+ (quantification, matchers)
}
- val qBindings: Bindings = quantification.binders.flatMap {
- case App(caller, tpe, args) => args.zipWithIndex.collect {
+ 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(tpe, caller)) Some(caller) else None, tpe, idx, qid)
+ (if (known(caller)) Some(caller) else None, tpe, idx, qid)
}
}
val (callerBindings, typeBindings) = (bindings ++ qBindings).partition(_._1.isDefined)
val callerMap: Map[(T, Int), Set[T]] = callerBindings.groupBy(p => (p._1.get, p._3)).mapValues(_.map(_._4))
- val typeMap: Map[(FunctionType, Int), Set[T]] = typeBindings.groupBy(p => (p._2, p._3)).mapValues(_.map(_._4))
+ val typeMap: Map[(TypeTree, Int), Set[T]] = typeBindings.groupBy(p => (p._2, p._3)).mapValues(_.map(_._4))
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))
@@ -320,9 +362,7 @@ class QuantificationManager[T](encoder: TemplateEncoder[T]) extends LambdaManage
}
val newQuantifications = for (mapping <- mappings) yield {
- val ph = nextHolder()
- val q = nextQ()
- qs :+= q
+ 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)
@@ -330,11 +370,13 @@ class QuantificationManager[T](encoder: TemplateEncoder[T]) extends LambdaManage
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) } +
- (template.holdVar -> ph) + (template.qs._2 -> q)
+ (quantification.qVar -> newQ)
val substituter = encoder.substitute(substMap)
- new Quantification(ph, quantification.guardVar,
+ 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,
@@ -344,21 +386,24 @@ class QuantificationManager[T](encoder: TemplateEncoder[T]) extends LambdaManage
quantification.applications map { case (b, fas) =>
substituter(b) -> fas.map(fa => fa.copy(caller = substituter(fa.caller), args = fa.args.map(substituter)))
},
- quantification.lambdas map { case (idT, template) => substituter(idT) -> template.substitute(mapping) },
- quantification.binders map { case app @ App(caller, _, args) =>
- app.copy(caller = substituter(caller), args = 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) }
)
}
val eqClause = {
+ val qs = newQuantifications.map(_.qVar)
val newQs = if (qs.size > 1) encoder.mkAnd(qs : _*) else qs.head
- encoder.mkImplies(substMap(template.start), encoder.mkEquals(template.qs._2, newQs))
+ encoder.mkImplies(substMap(template.start), encoder.mkEquals(template.holdVar, newQs))
}
instantiation = (instantiation._1 :+ eqClause, instantiation._2, instantiation._3)
- instantiatedApps = for ((b, app, qSubst) <- instantiatedApps) yield {
+ // 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)
@@ -366,286 +411,34 @@ class QuantificationManager[T](encoder: TemplateEncoder[T]) extends LambdaManage
}.toMap
}
- for (q <- newQuantifications) {
- instantiation ++= q.instantiate(b, app, nqSubst)
- }
-
- (b, app, nqSubst)
- }
-
- for ((b, apps) <- quantification.applications; app <- apps) {
- instantiatedApps :+= (b, app, quantifierSubst)
+ (b, m, nqSubst)
}
- instantiation
- }
+ quantifications ++= newQuantifications
- override def instantiateApp(blocker: T, app: App[T]): Instantiation[T] = {
- val quantifierSubst: Map[T, T] = freshQuantifierSubst
-
- var instantiation = Instantiation.empty[T]
- for (q <- quantifications) {
- instantiation ++= q.instantiate(blocker, app, quantifierSubst)
+ for ((b, m, qSubst) <- instantiatedMatchers; q <- newQuantifications) {
+ instantiation ++= q.instantiate(b, m, qSubst)
}
- instantiatedApps :+= (blocker, app, quantifierSubst)
-
- instantiation ++ super.instantiateApp(blocker, app)
- }
-
- /*
- private class QuantificationScope(
- val quantifiedApps: List[App[T]],
- val quantifiers: Map[Identifier, T],
- val condVars: Map[Identifier, T],
- val exprVars: Map[Identifier, T],
- val clauses: Seq[T],
- val blockers: Map[T, Set[TemplateCallInfo[T]]],
- val applications: Map[T, Set[App[T]]],
- val lambdas: Map[T, LambdaTemplate[T]],
- val res: Set[T]
- ) {
- def this() = this(Nil, Map.empty, Map.empty, Map.empty, Seq.empty, Map.empty, Map.empty, Map.empty, Set.empty)
- def this(scope: QuantificationScope) = this(
- scope.quantifiedApps,
- scope.quantifiers,
- scope.condVars,
- scope.exprVars,
- scope.clauses,
- scope.blockers,
- scope.applications,
- scope.lambdas,
- scope.res
- )
-
- lazy val quantified: Set[T] = quantifiers.values.toSet
- def free(tpe: FunctionType, idT: T): Boolean = res(idT) || freeLambdas(tpe)(idT)
+ instantiation
}
- private var scopes: List[QuantificationScope] = List(new QuantificationScope)
- private def scope: QuantificationScope = scopes.head
-
- override def push(): Unit = {
- self.push()
-
- val currentScope = scope
- scopes = new QuantificationScope(currentScope) :: scopes.tail
- }
+ 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
- override def pop(lvl: Int): Unit = {
- self.pop(lvl)
- scopes = scopes.drop(lvl)
- }
-
- def registerQuantified(
- startVar: Identifier,
- quantifierVars: Seq[Identifier],
- condVars: Map[Identifier, T],
- exprVars: Map[Identifier, T],
- guardedExprs: Map[Identifier, Seq[Expr]],
- lambdas: Map[T, LambdaTemplate[T]],
- subst: Map[Identifier, T],
- res: Option[T]
- ): Unit = {
- val currentScope = scope
- def free(tpe: FunctionType, idT: T): Boolean = currentScope.free(tpe, idT) || res.exists(_ == idT)
-
- val quantifiers: Seq[(Identifier, T)] = quantifierVars.map(id => id -> encoder.encodeId(id))
- val quantified: Set[T] = quantifiers.map(_._2).toSet
- val pathVar = startVar -> subst(startVar)
- val (clauses, blockers, apps, _) = Template.encode(encoder, pathVar, quantifiers, condVars, exprVars, guardedExprs, lambdas, subst)
-
- val bindingApps: Set[App[T]] = {
- def rec(templates: Map[T, LambdaTemplate[T]]): Set[App[T]] = templates.flatMap {
- case (_, template) => template.applications.flatMap(_._2).toSet ++ rec(template.lambdas)
- }.toSet
-
- val allApps = apps.flatMap(_._2).toSet
- for (app @ App(caller, tpe, args) <- (allApps ++ rec(lambdas)) if args exists quantified) yield app
- }
-
- val argumentBindings: Set[(Option[T], FunctionType, Int, T)] = bindingApps.flatMap {
- case App(caller, tpe, args) => args.zipWithIndex.collect {
- case (qid, idx) if quantified(qid) => (if (free(tpe, caller)) Some(caller) else None, tpe, idx, qid)
- }
- }
-
- val (callerBindings, typeBindings) = argumentBindings.partition(_._1.isDefined)
-
- val typeMap: Map[FunctionType, Set[(Int, T)]] = typeBindings.groupBy(_._2).mapValues(_.map(p => (p._3, p._4)))
- val typePairs: Seq[(T, T)] = typeMap.toSeq.flatMap {
- case (_, argBinds) => argBinds.groupBy(_._1).mapValues(_.map(_._2)).toSeq.flatMap {
- case (_, options) => options.flatMap(o1 => options.map(o2 => o1 -> o2))
- }
- }
-
- val callerPairs: Seq[(T, T)] = callerBindings.groupBy(p => (p._1.get, p._2)).toSeq.flatMap {
- case ((freeFunction, tpe), arguments) =>
- val callerIdentified: Set[(Int, T)] = arguments.map(p => (p._3, p._4))
- val typeIdentified: Set[(Int, T)] = typeMap.getOrElse(tpe, Set.empty)
-
- (callerIdentified ++ typeIdentified).groupBy(_._1).mapValues(_.map(_._2)).toSeq.flatMap {
- case (_, options) => options.flatMap(o1 => options.map(o2 => o1 -> o2))
- }
- }
-
- val filteredPairs: Set[(T, T)] = {
- def rec(
- mappings: Seq[(T, T)],
- result: Set[(T, T)]
- ): Set[(T, T)] = mappings match {
- case (p @ (x, y)) +: tail if !result(p) && !result(y -> x) => rec(tail, result + p)
- case p +: tail => rec(tail, result)
- case Seq() => result
- }
-
- rec(callerPairs ++ typePairs, Set.empty)
- }
-
- val mappings: List[Map[T, T]] =
- filteredPairs.groupBy(_._1).toSeq.foldLeft(List(Map.empty[T, T])) {
- case (mappings, (_, pairs)) => pairs.toList.flatMap(p => mappings.map(mapping => mapping + p))
+ var instantiation = Instantiation.empty[T]
+ for (q <- quantifications) {
+ instantiation ++= q.instantiate(blocker, matcher, quantifierSubst)
}
- val (allClauses, allBlockers, allApps, quantifiedApps) = {
- var allClauses : Seq[T] = Seq.empty
- var allBlockers : Map[T, Set[TemplateCallInfo[T]]] = Map.empty.withDefaultValue(Set.empty)
- var allApps : Map[T, Set[App[T]]] = Map.empty.withDefaultValue(Set.empty)
-
- var quantifiedApps : Set[App[T]] = Set.empty
-
- for (mapping <- mappings) {
- val substituter = encoder.substitute(mapping)
- allClauses ++= clauses.map(substituter)
-
- blockers.foreach { case (b, fis) =>
- val bp = substituter(b)
- val fisp = fis.map(fi => fi.copy(args = fi.args.map(substituter)))
- allBlockers += bp -> (allBlockers(bp) ++ fisp)
- }
+ instantiatedMatchers :+= (blocker, matcher, quantifierSubst)
+ boundMatchers += (blocker -> matcher)
- apps.foreach { case (b, fas) =>
- val bp = substituter(b)
- val fasp = fas.map(fa => fa.copy(caller = substituter(fa.caller), args = fa.args.map(substituter)))
- allApps += bp -> (allApps(bp) ++ fasp)
- }
-
- quantifiedApps ++= bindingApps.map { case app @ App(caller, _, args) =>
- app.copy(caller = substituter(caller), args = args.map(substituter))
- }
- }
-
- (allClauses, allBlockers, allApps, quantifiedApps)
+ instantiation
}
- scopes = new QuantificationScope(
- currentScope.quantifiedApps ++ quantifiedApps,
- currentScope.quantifiers ++ quantifiers,
- currentScope.condVars ++ condVars,
- currentScope.exprVars ++ exprVars,
- currentScope.clauses ++ allClauses,
- currentScope.blockers merge allBlockers,
- currentScope.applications merge allApps,
- currentScope.lambdas ++ lambdas,
- currentScope.res ++ res
- ) :: scopes.tail
+ qInst
}
- override def instantiateApp(blocker: T, app: App[T]): Instantiation[T] = {
- val App(caller, tpe, args) = app
- val currentScope = scope
- import currentScope._
-
- // Build a mapping from applications in the quantified statement to all potential concrete
- // applications previously encountered. Also make sure the current `app` is in the mapping
- // as other instantiations have been performed previously when the associated applications
- // were first encountered.
- val appMappings: List[List[(App[T], App[T])]] = quantifiedApps
- // 1. select an application in the quantified proposition for which the current app can
- // be bound when generating the new constraints
- .filter(qapp => qapp.caller == caller || (qapp.tpe == tpe && !free(qapp.tpe, qapp.caller)))
- // 2. build the instantiation mapping associated to the chosen current application binding
- .flatMap { bindingApp => quantifiedApps
- // 2.1. select all potential matches for each quantified application
- .map { case qapp @ App(qcaller, qtpe, qargs) =>
- if (qapp == bindingApp) {
- bindingApp -> Set(app)
- } else {
- val instances = self.applications(qtpe).collect {
- case (_, app @ App(caller, _, _)) if qcaller == caller || !free(qtpe, caller) => app
- }
-
- // 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 withApp = if (qcaller == caller || !free(tpe, caller)) instances + app 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
- val withAll = withApp + qapp
-
- qapp -> withAll
- }
- }
- // 2.2. based on the possible bindings for each quantified application, build a set of
- // instantiation mappings that can be used to instantiate all necessary constraints
- .foldLeft[List[List[(App[T], App[T])]]] (List(Nil)) {
- case (mappings, (qapp, instances)) =>
- instances.toList.flatMap(app => mappings.map(mapping => mapping :+ (app -> qapp)))
- }
- }
-
- var instantiation = Instantiation.empty[T]
-
- for (mapping <- appMappings) {
- var constraints: List[T] = Nil
- var subst: Map[T, T] = Map.empty
-
- for {
- (App(qcaller, _, qargs), App(caller, _, args)) <- mapping
- _ = if (qcaller != caller) constraints :+= encoder.mkEquals(qcaller, caller)
- (qarg, arg) <- (qargs zip args)
- } if (subst.isDefinedAt(qarg) || !quantified(qarg)) {
- constraints :+= encoder.mkEquals(qarg, arg)
- } else {
- subst += qarg -> arg
- }
-
- // make sure we freshen quantified variables that haven't been bound by concrete calls
- subst ++= quantifiers.collect {
- case (id, idT) if !subst.isDefinedAt(idT) => idT -> encoder.encodeId(id)
- }
-
- val bp = encoder.encodeId(FreshIdentifier("qb", BooleanType))
- // TODO: empty `constraints`
- val enabler = encoder.mkEquals(bp, encoder.mkAnd(constraints : _*))
-
- val lambdaSubstMap = lambdas.map { case (idT, lambda) => idT -> encoder.encodeId(lambda.id) }
- val substMap = subst ++ lambdaSubstMap + (start -> enabler)
- val substituter = encoder.substitute(subst)
-
- val newClauses = enabler +: clauses.map(substituter)
- val newBlockers = blockers.map { case (b, fis) =>
- substituter(b) -> fis.map(fi => fi.copy(args = fi.args.map(substituter)))
- }
-
- val newApplications = currentScope.applications.map { case (b, fas) =>
- substituter(b) -> fas.map(fa => fa.copy(caller = substituter(fa.caller), args = fa.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) <- newApplications; app <- apps) {
- instantiation ++= instantiateApp(b, app)
- }
- }
-
- instantiation
- }
- */
}
diff --git a/src/main/scala/leon/solvers/templates/Templates.scala b/src/main/scala/leon/solvers/templates/Templates.scala
index 91c8ca699..ab63924ef 100644
--- a/src/main/scala/leon/solvers/templates/Templates.scala
+++ b/src/main/scala/leon/solvers/templates/Templates.scala
@@ -12,9 +12,7 @@ import purescala.Types._
import purescala.Definitions._
case class App[T](caller: T, tpe: FunctionType, args: Seq[T]) {
- override def toString = {
- "(" + caller + " : " + tpe + ")" + args.mkString("(", ",", ")")
- }
+ override def toString = "(" + caller + " : " + tpe + ")" + args.mkString("(", ",", ")")
}
object Instantiation {
@@ -45,7 +43,7 @@ import Instantiation.{empty => _, _}
trait Template[T] { self =>
val encoder : TemplateEncoder[T]
- val lambdaManager : LambdaManager[T]
+ val manager : QuantificationManager[T]
val start : T
val args : Seq[T]
@@ -55,6 +53,7 @@ trait Template[T] { self =>
val blockers : Map[T, Set[TemplateCallInfo[T]]]
val applications : Map[T, Set[App[T]]]
val quantifications: Seq[QuantificationTemplate[T]]
+ val matchers: Map[T, Set[Matcher[T]]]
val lambdas : Map[T, LambdaTemplate[T]]
private var substCache : Map[Seq[T],Map[T,T]] = Map.empty
@@ -71,36 +70,10 @@ 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 substituter : T => T = 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)))
- }
-
- val newApplications = applications.map { case (b,fas) =>
- substituter(b) -> fas.map(fa => fa.copy(caller = substituter(fa.caller), args = fa.args.map(substituter)))
- }
-
- var instantiation: Instantiation[T] = (newClauses, newBlockers, Map.empty)
-
- for ((idT, lambda) <- lambdas) {
- val newIdT = substituter(idT)
- val newTemplate = lambda.substitute(substMap)
- instantiation ++= lambdaManager.instantiateLambda(newIdT, newTemplate)
- }
-
- for ((b,apps) <- newApplications; app <- apps) {
- instantiation ++= lambdaManager.instantiateApp(b, app)
- }
-
- for (q <- quantifications) {
- instantiation ++= q.instantiate(substMap)
- }
- instantiation
+ Template.instantiate(encoder, manager,
+ clauses, blockers, applications, quantifications, matchers, lambdas, substMap)
}
override def toString : String = "Instantiated template"
@@ -150,6 +123,11 @@ object Template {
(templates, apps)
}
+ private def matchersOf[T](encodeExpr: Expr => T)(expr: Expr): Set[Matcher[T]] = collect[Matcher[T]] {
+ case Application(caller, args) => Set(Matcher(encodeExpr(caller), caller.getType, args.map(encodeExpr)))
+ case _ => Set.empty
+ }(expr)
+
def encode[T](
encoder: TemplateEncoder[T],
pathVar: (Identifier, T),
@@ -161,7 +139,7 @@ object Template {
substMap: Map[Identifier, T] = Map.empty[Identifier, T],
optCall: Option[TypedFunDef] = None,
optApp: Option[(T, FunctionType)] = None
- ) : (Seq[T], Map[T, Set[TemplateCallInfo[T]]], Map[T, Set[App[T]]], () => String) = {
+ ) : (Seq[T], Map[T, Set[TemplateCallInfo[T]]], Map[T, Set[App[T]]], Map[T, Set[Matcher[T]]], () => String) = {
val idToTrId : Map[Identifier, T] = {
condVars ++ exprVars + pathVar ++ arguments ++ substMap ++
@@ -175,21 +153,27 @@ object Template {
}).toSeq
val extractInfos : Expr => (Set[TemplateCallInfo[T]], Set[App[T]]) = functionCallInfos(encodeExpr)
+ val extractMatchers: Expr => Set[Matcher[T]] = matchersOf(encodeExpr)
+
val optIdCall = optCall.map(tfd => TemplateCallInfo[T](tfd, arguments.map(_._2)))
val optIdApp = optApp.map { case (idT, tpe) => App(idT, tpe, arguments.map(_._2)) }
+ val optIdMatch = optIdApp.map { case App(caller, tpe, args) => Matcher(caller, tpe, args) }
- val (blockers, applications) : (Map[Identifier, Set[TemplateCallInfo[T]]], Map[Identifier, Set[App[T]]]) = {
+ val (blockers, applications, matchers) = {
var blockers : Map[Identifier, Set[TemplateCallInfo[T]]] = Map.empty
var applications : Map[Identifier, Set[App[T]]] = Map.empty
+ var matchers : Map[Identifier, Set[Matcher[T]]] = Map.empty
for ((b,es) <- guardedExprs) {
- var funInfos : Set[TemplateCallInfo[T]] = Set.empty
- var appInfos : Set[App[T]] = Set.empty
+ var funInfos : Set[TemplateCallInfo[T]] = Set.empty
+ var appInfos : Set[App[T]] = Set.empty
+ var matchInfos : Set[Matcher[T]] = Set.empty
for (e <- es) {
val (newFunInfos, newAppInfos) = extractInfos(e)
funInfos ++= newFunInfos
appInfos ++= newAppInfos
+ matchInfos ++= extractMatchers(e)
}
val calls = funInfos -- optIdCall
@@ -197,13 +181,17 @@ object Template {
val apps = appInfos -- optIdApp
if (apps.nonEmpty) applications += b -> apps
+
+ val matchs = matchInfos -- optIdMatch
+ if (matchs.nonEmpty) matchers += b -> matchs
}
- (blockers, applications)
+ (blockers, applications, matchers)
}
val encodedBlockers : Map[T, Set[TemplateCallInfo[T]]] = blockers.map(p => idToTrId(p._1) -> p._2)
val encodedApps : Map[T, Set[App[T]]] = applications.map(p => idToTrId(p._1) -> p._2)
+ val encodedMatchers : Map[T, Set[Matcher[T]]] = matchers.map(p => idToTrId(p._1) -> p._2)
val stringRepr : () => String = () => {
" * Activating boolean : " + pathVar._1 + "\n" +
@@ -222,7 +210,51 @@ object Template {
}.mkString("\n")
}
- (clauses, encodedBlockers, encodedApps, stringRepr)
+ (clauses, encodedBlockers, encodedApps, encodedMatchers, stringRepr)
+ }
+
+ def instantiate[T](
+ encoder: TemplateEncoder[T],
+ manager: QuantificationManager[T],
+ clauses: Seq[T],
+ blockers: Map[T, Set[TemplateCallInfo[T]]],
+ applications: Map[T, Set[App[T]]],
+ quantifications: Seq[QuantificationTemplate[T]],
+ matchers: Map[T, Set[Matcher[T]]],
+ lambdas: Map[T, LambdaTemplate[T]],
+ substMap: Map[T, T]
+ ): Instantiation[T] = {
+
+ val substituter : T => T = 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)))
+ }
+
+ var instantiation: Instantiation[T] = (newClauses, newBlockers, Map.empty)
+
+ for ((idT, lambda) <- lambdas) {
+ val newIdT = substituter(idT)
+ val newTemplate = lambda.substitute(substMap)
+ instantiation ++= manager.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 ++= manager.instantiateApp(bp, newApp)
+ }
+
+ for ((b, matchs) <- matchers; bp = substituter(b); m <- matchs) {
+ val newM = m.copy(caller = substituter(m.caller), args = m.args.map(substituter))
+ instantiation ++= manager.instantiateMatcher(bp, newM)
+ }
+
+ for (q <- quantifications) {
+ instantiation ++= q.instantiate(substMap)
+ }
+
+ instantiation
}
}
@@ -231,7 +263,7 @@ object FunctionTemplate {
def apply[T](
tfd: TypedFunDef,
encoder: TemplateEncoder[T],
- lambdaManager: LambdaManager[T],
+ manager: QuantificationManager[T],
pathVar: (Identifier, T),
arguments: Seq[(Identifier, T)],
condVars: Map[Identifier, T],
@@ -242,7 +274,7 @@ object FunctionTemplate {
isRealFunDef: Boolean
) : FunctionTemplate[T] = {
- val (clauses, blockers, applications, templateString) =
+ val (clauses, blockers, applications, matchers, templateString) =
Template.encode(encoder, pathVar, arguments, condVars, exprVars, guardedExprs, lambdas,
substMap = quantifications.map(q => q.qs).toMap,
optCall = Some(tfd))
@@ -256,7 +288,7 @@ object FunctionTemplate {
new FunctionTemplate[T](
tfd,
encoder,
- lambdaManager,
+ manager,
pathVar._2,
arguments.map(_._2),
condVars,
@@ -265,6 +297,7 @@ object FunctionTemplate {
blockers,
applications,
quantifications,
+ matchers,
lambdas,
isRealFunDef,
funString
@@ -275,7 +308,7 @@ object FunctionTemplate {
class FunctionTemplate[T] private(
val tfd: TypedFunDef,
val encoder: TemplateEncoder[T],
- val lambdaManager: LambdaManager[T],
+ val manager: QuantificationManager[T],
val start: T,
val args: Seq[T],
val condVars: Map[Identifier, T],
@@ -284,6 +317,7 @@ class FunctionTemplate[T] private(
val blockers: Map[T, Set[TemplateCallInfo[T]]],
val applications: Map[T, Set[App[T]]],
val quantifications: Seq[QuantificationTemplate[T]],
+ val matchers: Map[T, Set[Matcher[T]]],
val lambdas: Map[T, LambdaTemplate[T]],
isRealFunDef: Boolean,
stringRepr: () => String) extends Template[T] {
@@ -292,7 +326,7 @@ class FunctionTemplate[T] private(
override def toString : String = str
override def instantiate(aVar: T, args: Seq[T]): (Seq[T], Map[T, Set[TemplateCallInfo[T]]], Map[(T, App[T]), Set[TemplateAppInfo[T]]]) = {
- if (!isRealFunDef) lambdaManager.registerFree(tfd.params.map(_.getType) zip args)
+ if (!isRealFunDef) manager.registerFree(tfd.params.map(_.getType) zip args)
super.instantiate(aVar, args)
}
}
@@ -343,7 +377,7 @@ object LambdaTemplate {
def apply[T](
ids: (Identifier, T),
encoder: TemplateEncoder[T],
- lambdaManager: LambdaManager[T],
+ manager: QuantificationManager[T],
pathVar: (Identifier, T),
arguments: Seq[(Identifier, T)],
condVars: Map[Identifier, T],
@@ -357,7 +391,7 @@ object LambdaTemplate {
val id = ids._2
val tpe = ids._1.getType.asInstanceOf[FunctionType]
- val (clauses, blockers, applications, templateString) =
+ val (clauses, blockers, applications, matchers, templateString) =
Template.encode(encoder, pathVar, arguments, condVars, exprVars, guardedExprs, lambdas,
substMap = baseSubstMap + ids, optApp = Some(id -> tpe))
@@ -370,7 +404,7 @@ object LambdaTemplate {
new LambdaTemplate[T](
ids._1,
encoder,
- lambdaManager,
+ manager,
pathVar._2,
arguments.map(_._2),
condVars,
@@ -378,6 +412,7 @@ object LambdaTemplate {
clauses,
blockers,
applications,
+ matchers,
lambdas,
keyDeps,
key,
@@ -389,7 +424,7 @@ object LambdaTemplate {
class LambdaTemplate[T] private (
val id: Identifier,
val encoder: TemplateEncoder[T],
- val lambdaManager: LambdaManager[T],
+ val manager: QuantificationManager[T],
val start: T,
val args: Seq[T],
val condVars: Map[Identifier, T],
@@ -397,6 +432,7 @@ class LambdaTemplate[T] private (
val clauses: Seq[T],
val blockers: Map[T, Set[TemplateCallInfo[T]]],
val applications: Map[T, Set[App[T]]],
+ val matchers: Map[T, Set[Matcher[T]]],
val lambdas: Map[T, LambdaTemplate[T]],
private[templates] val dependencies: Map[Identifier, T],
private[templates] val structuralKey: Lambda,
@@ -422,6 +458,11 @@ class LambdaTemplate[T] private (
bp -> fas.map(fa => fa.copy(caller = substituter(fa.caller), args = fa.args.map(substituter)))
}
+ val newMatchers = matchers.map { case (b, ms) =>
+ val bp = if (b == start) newStart else b
+ bp -> ms.map(m => m.copy(caller = substituter(m.caller), args = m.args.map(substituter)))
+ }
+
val newLambdas = lambdas.map { case (idT, template) => idT -> template.substitute(substMap) }
val newDependencies = dependencies.map(p => p._1 -> substituter(p._2))
@@ -429,7 +470,7 @@ class LambdaTemplate[T] private (
new LambdaTemplate[T](
id,
encoder,
- lambdaManager,
+ manager,
newStart,
args,
condVars,
@@ -437,6 +478,7 @@ class LambdaTemplate[T] private (
newClauses,
newBlockers,
newApplications,
+ newMatchers,
newLambdas,
newDependencies,
structuralKey,
diff --git a/src/main/scala/leon/solvers/templates/UnrollingBank.scala b/src/main/scala/leon/solvers/templates/UnrollingBank.scala
index abd50bb39..c1912d9d5 100644
--- a/src/main/scala/leon/solvers/templates/UnrollingBank.scala
+++ b/src/main/scala/leon/solvers/templates/UnrollingBank.scala
@@ -91,7 +91,9 @@ class UnrollingBank[T <% Printable](ctx: LeonContext, templateGenerator: Templat
def canUnroll = callInfo.nonEmpty || appInfo.nonEmpty
- def currentBlockers = callInfo.map(_._2._3).toSeq ++ appInfo.map(_._2._4).toSeq ++ manager.blockers
+ def currentBlockers = callInfo.map(_._2._3).toSeq ++ appInfo.map(_._2._4).toSeq
+
+ def quantificationAssumptions = manager.blockers
def getBlockersToUnlock: Seq[T] = {
if (callInfo.isEmpty && appInfo.isEmpty) {
diff --git a/src/main/scala/leon/solvers/z3/FairZ3Solver.scala b/src/main/scala/leon/solvers/z3/FairZ3Solver.scala
index f858ef12d..b8eeeafab 100644
--- a/src/main/scala/leon/solvers/z3/FairZ3Solver.scala
+++ b/src/main/scala/leon/solvers/z3/FairZ3Solver.scala
@@ -268,7 +268,7 @@ class FairZ3Solver(val context: LeonContext, val program: Program)
val timer = context.timers.solvers.z3.check.start()
solver.push() // FIXME: remove when z3 bug is fixed
- val res = solver.checkAssumptions((assumptionsAsZ3 ++ unrollingBank.currentBlockers) :_*)
+ val res = solver.checkAssumptions((assumptionsAsZ3 ++ unrollingBank.currentBlockers ++ unrollingBank.quantificationAssumptions) :_*)
solver.pop() // FIXME: remove when z3 bug is fixed
timer.stop()
@@ -359,7 +359,7 @@ class FairZ3Solver(val context: LeonContext, val program: Program)
val timer = context.timers.solvers.z3.check.start()
solver.push() // FIXME: remove when z3 bug is fixed
- val res2 = solver.checkAssumptions(assumptionsAsZ3 : _*)
+ val res2 = solver.checkAssumptions((assumptionsAsZ3 ++ unrollingBank.quantificationAssumptions) : _*)
solver.pop() // FIXME: remove when z3 bug is fixed
timer.stop()
--
GitLab