diff --git a/src/main/scala/leon/solvers/templates/QuantificationManager.scala b/src/main/scala/leon/solvers/templates/QuantificationManager.scala index a8c4f96c9726bbf945171341c37f80c1ccf7af7b..2b76e02a958c57de36f32e61792e0dd8685a119f 100644 --- a/src/main/scala/leon/solvers/templates/QuantificationManager.scala +++ b/src/main/scala/leon/solvers/templates/QuantificationManager.scala @@ -52,7 +52,7 @@ object QuantificationTemplate { val (clauses, blockers, applications, _) = Template.encode(encoder, pathVar, quantifiers, condVars, exprVars, guardedExprs, lambdas, - substMap = subst + holders + guards) + substMap = subst + holders + guards + qs) new QuantificationTemplate[T](quantificationManager, pathVar._2, qs, holders._2, guards._2, quantifiers, @@ -60,7 +60,7 @@ object QuantificationTemplate { } } -trait QuantificationManager[T] { self : LambdaManager[T] => +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 @@ -70,7 +70,7 @@ trait QuantificationManager[T] { self : LambdaManager[T] => val currentCount = quantifiers.size if (currentCount >= count) quantifiers.take(count) else { - val newQuantifiers = List.range(0, currentCount - count).map(_ => encoder.encodeId(FreshIdentifier("x", tpe))) + val newQuantifiers = List.range(0, count - currentCount).map(_ => encoder.encodeId(FreshIdentifier("x", tpe))) quantified ++= newQuantifiers val allQuantifiers = quantifiers ++ newQuantifiers @@ -88,6 +88,11 @@ trait QuantificationManager[T] { self : LambdaManager[T] => () => encoder.encodeId(id) } + private val nextQ: () => T = { + val id: Identifier = FreshIdentifier("q", BooleanType) + () => encoder.encodeId(id) + } + private type Bindings = Set[(Option[T], FunctionType, Int, T)] private var bindingsStack: List[Bindings] = List(Set.empty) private def bindings: Bindings = bindingsStack.head @@ -107,6 +112,8 @@ trait QuantificationManager[T] { self : LambdaManager[T] => instantiatedAppsStack = ias :: instantiatedAppsStack.tail } + def blockers: Seq[T] = quantifications.map(_.holdVar) + private def known(tpe: FunctionType, idT: T): Boolean = freeLambdas(tpe)(idT) || byID.isDefinedAt(idT) private class Quantification ( @@ -157,18 +164,18 @@ trait QuantificationManager[T] { self : LambdaManager[T] => if (qapp == bindingApp) { bindingApp -> Set(blocker -> app) } else { - val instances = self.applications(qtpe).filter { - case (b, app @ App(caller, _, _)) => qcaller == caller || !known(qtpe, caller) + val instances: Seq[(T, App[T])] = instantiatedApps.collect { + case (b, app @ App(caller, tpe, _), _) if tpe == qtpe && (qcaller == caller || !known(qtpe, caller)) => (b, 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 || !known(tpe, caller)) instances + (blocker -> app) else instances + val withApp = if (qcaller == caller || !known(tpe, caller)) instances :+ (blocker -> 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 // Note: we can use `blocker` here as the blocker since it is guaranteed true in this branch - val withAll = withApp + (blocker -> qapp) + val withAll = withApp :+ (blocker -> qapp) qapp -> withAll } @@ -177,7 +184,7 @@ trait QuantificationManager[T] { self : LambdaManager[T] => // 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, app, qapp)) + case (b, app) => mappings.map(mapping => mapping :+ (b, qapp, app)) } } } @@ -186,7 +193,7 @@ trait QuantificationManager[T] { self : LambdaManager[T] => for (mapping <- appMappings) { var constraints: List[T] = Nil - var subst: Map[T, T] = quantifierSubst + var subst: Map[T, T] = Map.empty for { (b, App(qcaller, _, qargs), App(caller, _, args)) <- mapping @@ -199,19 +206,23 @@ trait QuantificationManager[T] { self : LambdaManager[T] => 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 holder = nextHolder() - val lambdaSubstMap = lambdas.map { case (idT, lambda) => idT -> encoder.encodeId(lambda.id) } + val lambdaSubstMap = lambdas map { case (idT, lambda) => idT -> encoder.encodeId(lambda.id) } val substMap = subst ++ lambdaSubstMap + (guardVar -> enabler) + (holdVar -> holder) - val substituter = encoder.substitute(subst) + val substituter = encoder.substitute(substMap) - val newClauses = enabler +: clauses.map(substituter) - val newBlockers = blockers.map { case (b, fis) => + 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) => + val newApplications = applications map { case (b, fas) => substituter(b) -> fas.map(fa => fa.copy(caller = substituter(fa.caller), args = fa.args.map(substituter))) } @@ -220,11 +231,11 @@ trait QuantificationManager[T] { self : LambdaManager[T] => for ((idT, lambda) <- lambdas) { val newIdT = substituter(idT) val newTemplate = lambda.substitute(substMap) - instantiation ++= self.instantiateLambda(newIdT, newTemplate) + instantiation ++= QuantificationManager.super.instantiateLambda(newIdT, newTemplate) } for ((b, apps) <- newApplications; app <- apps) { - instantiation ++= self.instantiateApp(b, app) + instantiation ++= QuantificationManager.super.instantiateApp(b, app) } holdVar = holder @@ -267,9 +278,23 @@ trait QuantificationManager[T] { self : LambdaManager[T] => val quantifierSubst: Map[T,T] = freshQuantifierSubst - var instantiation: Instantiation[T] = (quantification.clauses, quantification.blockers, Map.empty) - for (q <- quantifications; (b, apps) <- quantification.applications; app <- apps) { - instantiation ++= q.instantiate(b, app, quantifierSubst) + 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) + } + instantiation } val qBindings: Bindings = quantification.binders.flatMap { @@ -285,7 +310,7 @@ trait QuantificationManager[T] { self : LambdaManager[T] => val typeMap: Map[(FunctionType, 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(tpe -> idx) ++ optIdT.toSeq.flatMap(idT => callerMap(idT -> idx)) + val matches = typeMap.getOrElse(tpe -> idx, Set.empty) ++ optIdT.toSeq.flatMap(idT => callerMap(idT -> idx)) matches.map(q2 => q -> q2) } @@ -296,13 +321,16 @@ trait QuantificationManager[T] { self : LambdaManager[T] => val newQuantifications = for (mapping <- mappings) yield { val ph = nextHolder() + val q = nextQ() + qs :+= q val freshConds = quantification.condVars.map(p => p._1.freshen -> p._2) val freshExprs = quantification.exprVars.map(p => p._1.freshen -> p._2) 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.lambdas.map { case (idT, template) => idT -> encoder.encodeId(template.id) } + + (template.holdVar -> ph) + (template.qs._2 -> q) val substituter = encoder.substitute(substMap) @@ -324,9 +352,8 @@ trait QuantificationManager[T] { self : LambdaManager[T] => } val eqClause = { - val holders = newQuantifications.map(_.holdVar) - val newHolders = if (holders.size > 1) encoder.mkAnd(holders : _*) else holders.head - encoder.mkEquals(template.qs._2, newHolders) + val newQs = if (qs.size > 1) encoder.mkAnd(qs : _*) else qs.head + encoder.mkImplies(substMap(template.start), encoder.mkEquals(template.qs._2, newQs)) } instantiation = (instantiation._1 :+ eqClause, instantiation._2, instantiation._3) @@ -362,7 +389,8 @@ trait QuantificationManager[T] { self : LambdaManager[T] => } instantiatedApps :+= (blocker, app, quantifierSubst) - instantiation + + instantiation ++ super.instantiateApp(blocker, app) } /* diff --git a/src/main/scala/leon/solvers/templates/TemplateGenerator.scala b/src/main/scala/leon/solvers/templates/TemplateGenerator.scala index ef2ca6e91855e80f34e520158859d93bfeed7fe5..9b974a8de371f7e26a7c71d64729ce4cb4b90780 100644 --- a/src/main/scala/leon/solvers/templates/TemplateGenerator.scala +++ b/src/main/scala/leon/solvers/templates/TemplateGenerator.scala @@ -17,7 +17,7 @@ class TemplateGenerator[T](val encoder: TemplateEncoder[T], private var cache = Map[TypedFunDef, FunctionTemplate[T]]() private var cacheExpr = Map[Expr, FunctionTemplate[T]]() - private val lambdaManager = new LambdaManager[T](encoder) with QuantificationManager[T] + val manager = new QuantificationManager[T](encoder) def mkTemplate(body: Expr): FunctionTemplate[T] = { if (cacheExpr contains body) { @@ -107,7 +107,7 @@ class TemplateGenerator[T](val encoder: TemplateEncoder[T], (bodyConds, bodyExprs, bodyGuarded, bodyLambdas, bodyQuantifications) } - val template = FunctionTemplate(tfd, encoder, lambdaManager, + val template = FunctionTemplate(tfd, encoder, manager, pathVar, arguments, condVars, exprVars, guardedExprs, quantifications, lambdas, isRealFunDef) cache += tfd -> template template @@ -274,7 +274,7 @@ class TemplateGenerator[T](val encoder: TemplateEncoder[T], val ids: (Identifier, T) = lid -> storeLambda(lid) val dependencies: Map[Identifier, T] = variablesOf(l).map(id => id -> localSubst(id)).toMap - val template = LambdaTemplate(ids, encoder, lambdaManager, pathVar -> encodedCond(pathVar), + val template = LambdaTemplate(ids, encoder, manager, pathVar -> encodedCond(pathVar), idArgs zip trArgs, lambdaConds, lambdaExprs, lambdaGuarded, lambdaTemplates, localSubst, dependencies, l) registerLambda(ids._2, template) @@ -296,7 +296,7 @@ class TemplateGenerator[T](val encoder: TemplateEncoder[T], val (qConds, qExprs, qGuarded, qTemplates, qQuants) = mkClauses(pathVar, clause, clauseSubst) assert(qQuants.isEmpty, "Unhandled nested quantification in "+clause) - val template = QuantificationTemplate[T](encoder, lambdaManager, pathVar -> encodedCond(pathVar), + val template = QuantificationTemplate[T](encoder, manager, pathVar -> encodedCond(pathVar), qs, ph, guard, idQuantifiers zip trQuantifiers, qConds, qExprs, qGuarded, qTemplates, localSubst) registerQuantification(template) diff --git a/src/main/scala/leon/solvers/templates/Templates.scala b/src/main/scala/leon/solvers/templates/Templates.scala index ae9e4e3e03b4504682d15993960600e6db377146..91c8ca699070c5e24443b8101a8693f1892b4614 100644 --- a/src/main/scala/leon/solvers/templates/Templates.scala +++ b/src/main/scala/leon/solvers/templates/Templates.scala @@ -244,6 +244,7 @@ object FunctionTemplate { val (clauses, blockers, applications, templateString) = Template.encode(encoder, pathVar, arguments, condVars, exprVars, guardedExprs, lambdas, + substMap = quantifications.map(q => q.qs).toMap, optCall = Some(tfd)) val funString : () => String = () => { diff --git a/src/main/scala/leon/solvers/templates/UnrollingBank.scala b/src/main/scala/leon/solvers/templates/UnrollingBank.scala index 07bc7de6dae3d4e741a901889b9f27e6cfcb41ba..abd50bb394115bfc7e7efddbcb2d9eb82f27b3a6 100644 --- a/src/main/scala/leon/solvers/templates/UnrollingBank.scala +++ b/src/main/scala/leon/solvers/templates/UnrollingBank.scala @@ -16,6 +16,7 @@ class UnrollingBank[T <% Printable](ctx: LeonContext, templateGenerator: Templat val reporter = ctx.reporter private val encoder = templateGenerator.encoder + private val manager = templateGenerator.manager // Keep which function invocation is guarded by which guard, // also specify the generation of the blocker. @@ -90,7 +91,7 @@ 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 + def currentBlockers = callInfo.map(_._2._3).toSeq ++ appInfo.map(_._2._4).toSeq ++ manager.blockers def getBlockersToUnlock: Seq[T] = { if (callInfo.isEmpty && appInfo.isEmpty) {