diff --git a/src/main/scala/leon/solvers/smtlib/SMTLIBTarget.scala b/src/main/scala/leon/solvers/smtlib/SMTLIBTarget.scala
index 8b24c2053de01c42becd5336dfce113d0043b75c..ce0656727dbca2499600a3b6ff84704aa9daa6b8 100644
--- a/src/main/scala/leon/solvers/smtlib/SMTLIBTarget.scala
+++ b/src/main/scala/leon/solvers/smtlib/SMTLIBTarget.scala
@@ -538,10 +538,8 @@ trait SMTLIBTarget extends Interruptible {
* ===== Everything else =====
*/
case ap @ Application(caller, args) =>
- FunctionApplication(
- declareLambda(caller.getType.asInstanceOf[FunctionType]),
- (caller +: args).map(toSMT)
- )
+ val dyn = declareLambda(caller.getType.asInstanceOf[FunctionType])
+ FunctionApplication(dyn, (caller +: args).map(toSMT))
case Not(u) => Core.Not(toSMT(u))
case UMinus(u) => Ints.Neg(toSMT(u))
diff --git a/src/main/scala/leon/solvers/templates/LambdaManager.scala b/src/main/scala/leon/solvers/templates/LambdaManager.scala
index 75d163815a17fbf31c56b684d58e3d26efe7feaa..d1aa0377a8f939830cb877c5aba78071d74c2de6 100644
--- a/src/main/scala/leon/solvers/templates/LambdaManager.scala
+++ b/src/main/scala/leon/solvers/templates/LambdaManager.scala
@@ -72,6 +72,36 @@ object LambdaTemplate {
}
}
+trait KeyedTemplate[T, E <: Expr] {
+ val dependencies: Map[Identifier, T]
+ val structuralKey: E
+
+ lazy val key: (E, Seq[T]) = {
+ def rec(e: Expr): Seq[Identifier] = e match {
+ case Variable(id) =>
+ if (dependencies.isDefinedAt(id)) {
+ Seq(id)
+ } else {
+ Seq.empty
+ }
+
+ case Operator(es, _) => es.flatMap(rec)
+
+ case _ => Seq.empty
+ }
+
+ structuralKey -> rec(structuralKey).distinct.map(dependencies)
+ }
+
+ override def equals(that: Any): Boolean = that match {
+ case t: KeyedTemplate[T, E] =>
+ key == t.key
+ case _ => false
+ }
+
+ override def hashCode: Int = key.hashCode
+}
+
class LambdaTemplate[T] private (
val ids: (Identifier, T),
val encoder: TemplateEncoder[T],
@@ -87,9 +117,9 @@ class LambdaTemplate[T] private (
val quantifications: Seq[QuantificationTemplate[T]],
val matchers: Map[T, Set[Matcher[T]]],
val lambdas: Seq[LambdaTemplate[T]],
- private[templates] val dependencies: Map[Identifier, T],
- private[templates] val structuralKey: Lambda,
- stringRepr: () => String) extends Template[T] {
+ val dependencies: Map[Identifier, T],
+ val structuralKey: Lambda,
+ stringRepr: () => String) extends Template[T] with KeyedTemplate[T, Lambda] {
val args = arguments.map(_._2)
val tpe = ids._1.getType.asInstanceOf[FunctionType]
@@ -139,43 +169,18 @@ class LambdaTemplate[T] private (
)
}
- private lazy val str : String = stringRepr()
- override def toString : String = str
-
- lazy val key: (Expr, Seq[T]) = {
- def rec(e: Expr): Seq[Identifier] = e match {
- case Variable(id) =>
- if (dependencies.isDefinedAt(id)) {
- Seq(id)
- } else {
- Seq.empty
- }
-
- case Operator(es, _) => es.flatMap(rec)
-
- case _ => Seq.empty
- }
-
- structuralKey -> rec(structuralKey).distinct.map(dependencies)
- }
-
- override def equals(that: Any): Boolean = that match {
- case t: LambdaTemplate[T] =>
- val (lambda1, deps1) = key
- val (lambda2, deps2) = t.key
- (lambda1 == lambda2) && {
- (deps1 zip deps2).forall { case (id1, id2) =>
- (manager.byID.get(id1), manager.byID.get(id2)) match {
- case (Some(t1), Some(t2)) => t1 == t2
- case _ => id1 == id2
- }
- }
- }
-
- case _ => false
+ def withId(idT: T): LambdaTemplate[T] = {
+ val substituter = encoder.substitute(Map(ids._2 -> idT))
+ new LambdaTemplate[T](
+ ids._1 -> idT, encoder, manager, pathVar, arguments, condVars, exprVars, condTree,
+ clauses map substituter, // make sure the body-defining clause is inlined!
+ blockers, applications, quantifications, matchers, lambdas,
+ dependencies, structuralKey, stringRepr
+ )
}
- override def hashCode: Int = key.hashCode
+ private lazy val str : String = stringRepr()
+ override def toString : String = str
override def instantiate(substMap: Map[T, T]): Instantiation[T] = {
super.instantiate(substMap) ++ manager.instantiateAxiom(this, substMap)
@@ -186,7 +191,7 @@ class LambdaManager[T](encoder: TemplateEncoder[T]) extends TemplateManager(enco
private[templates] lazy val trueT = encoder.encodeExpr(Map.empty)(BooleanLiteral(true))
protected[templates] val byID = new IncrementalMap[T, LambdaTemplate[T]]
- protected val byType = new IncrementalMap[FunctionType, Set[LambdaTemplate[T]]].withDefaultValue(Set.empty)
+ protected val byType = new IncrementalMap[FunctionType, Map[(Expr, Seq[T]), LambdaTemplate[T]]].withDefaultValue(Map.empty)
protected val applications = new IncrementalMap[FunctionType, Set[(T, App[T])]].withDefaultValue(Set.empty)
protected val freeLambdas = new IncrementalMap[FunctionType, Set[T]].withDefaultValue(Set.empty)
@@ -203,27 +208,30 @@ class LambdaManager[T](encoder: TemplateEncoder[T]) extends TemplateManager(enco
}
}
- def instantiateLambda(template: LambdaTemplate[T]): Instantiation[T] = {
- val idT = template.ids._2
- var clauses : Clauses[T] = equalityClauses(template)
- var appBlockers : AppBlockers[T] = Map.empty.withDefaultValue(Set.empty)
+ def instantiateLambda(template: LambdaTemplate[T]): (T, Instantiation[T]) = {
+ byType(template.tpe).get(template.key) match {
+ case Some(template) =>
+ (template.ids._2, Instantiation.empty)
- // make sure the new lambda isn't equal to any free lambda var
- clauses ++= freeLambdas(template.tpe).map(pIdT => encoder.mkNot(encoder.mkEquals(pIdT, idT)))
+ case None =>
+ val idT = encoder.encodeId(template.ids._1)
+ val newTemplate = template.withId(idT)
- byID += idT -> template
+ var clauses : Clauses[T] = equalityClauses(newTemplate)
+ var appBlockers : AppBlockers[T] = Map.empty.withDefaultValue(Set.empty)
- if (byType(template.tpe)(template)) {
- (clauses, Map.empty, Map.empty)
- } else {
- byType += template.tpe -> (byType(template.tpe) + template)
+ // make sure the new lambda isn't equal to any free lambda var
+ clauses ++= freeLambdas(newTemplate.tpe).map(pIdT => encoder.mkNot(encoder.mkEquals(pIdT, idT)))
- for (blockedApp @ (_, App(caller, tpe, args)) <- applications(template.tpe)) {
- val equals = encoder.mkEquals(idT, caller)
- appBlockers += (blockedApp -> (appBlockers(blockedApp) + TemplateAppInfo(template, equals, args)))
- }
+ byID += idT -> newTemplate
+ byType += newTemplate.tpe -> (byType(newTemplate.tpe) + (newTemplate.key -> newTemplate))
+
+ for (blockedApp @ (_, App(caller, tpe, args)) <- applications(newTemplate.tpe)) {
+ val equals = encoder.mkEquals(idT, caller)
+ appBlockers += (blockedApp -> (appBlockers(blockedApp) + TemplateAppInfo(newTemplate, equals, args)))
+ }
- (clauses, Map.empty, appBlockers)
+ (idT, (clauses, Map.empty, appBlockers))
}
}
@@ -244,7 +252,7 @@ class LambdaManager[T](encoder: TemplateEncoder[T]) extends TemplateManager(enco
// make sure that even if byType(tpe) is empty, app is recorded in blockers
// so that UnrollingBank will generate the initial block!
val init = instantiation withApps Map(key -> Set.empty)
- val inst = byType(tpe).foldLeft(init) {
+ val inst = byType(tpe).values.foldLeft(init) {
case (instantiation, template) =>
val equals = encoder.mkEquals(template.ids._2, caller)
instantiation withApp (key -> TemplateAppInfo(template, equals, args))
@@ -260,7 +268,7 @@ class LambdaManager[T](encoder: TemplateEncoder[T]) extends TemplateManager(enco
private def equalityClauses(template: LambdaTemplate[T]): Seq[T] = {
val (s1, deps1) = template.key
- byType(template.tpe).map { that =>
+ byType(template.tpe).values.map { that =>
val (s2, deps2) = that.key
val equals = encoder.mkEquals(template.ids._2, that.ids._2)
if (s1 == s2) {
diff --git a/src/main/scala/leon/solvers/templates/QuantificationManager.scala b/src/main/scala/leon/solvers/templates/QuantificationManager.scala
index c7f715b5eefe573d88eeb94b45293ba7cde646bf..314c7549c0899488ba9e78c9739e4718e350b608 100644
--- a/src/main/scala/leon/solvers/templates/QuantificationManager.scala
+++ b/src/main/scala/leon/solvers/templates/QuantificationManager.scala
@@ -58,7 +58,9 @@ class QuantificationTemplate[T](
val blockers: Map[T, Set[TemplateCallInfo[T]]],
val applications: Map[T, Set[App[T]]],
val matchers: Map[T, Set[Matcher[T]]],
- val lambdas: Seq[LambdaTemplate[T]]) {
+ val lambdas: Seq[LambdaTemplate[T]],
+ val dependencies: Map[Identifier, T],
+ val structuralKey: Forall) extends KeyedTemplate[T, Forall] {
lazy val start = pathVar._2
@@ -84,7 +86,9 @@ class QuantificationTemplate[T](
matchers.map { case (b, ms) =>
substituter(b) -> ms.map(_.substitute(substituter))
},
- lambdas.map(_.substitute(substituter))
+ lambdas.map(_.substitute(substituter)),
+ dependencies.map { case (id, value) => id -> substituter(value) },
+ structuralKey
)
}
}
@@ -104,7 +108,9 @@ object QuantificationTemplate {
condTree: Map[Identifier, Set[Identifier]],
guardedExprs: Map[Identifier, Seq[Expr]],
lambdas: Seq[LambdaTemplate[T]],
- subst: Map[Identifier, T]
+ baseSubstMap: Map[Identifier, T],
+ dependencies: Map[Identifier, T],
+ proposition: Forall
): QuantificationTemplate[T] = {
val q2s: (Identifier, T) = q2 -> encoder.encodeId(q2)
@@ -113,11 +119,15 @@ object QuantificationTemplate {
val (clauses, blockers, applications, matchers, _) =
Template.encode(encoder, pathVar, quantifiers, condVars, exprVars, guardedExprs, lambdas,
- substMap = subst + q2s + insts + guards + qs)
+ substMap = baseSubstMap + q2s + insts + guards + qs)
+
+ val (structuralQuant, structSubst) = normalizeStructure(proposition)
+ val keyDeps = dependencies.map { case (id, idT) => structSubst(id) -> idT }
+ val key = structuralQuant.asInstanceOf[Forall]
new QuantificationTemplate[T](quantificationManager,
- pathVar, qs, q2s, insts, guards._2, quantifiers,
- condVars, exprVars, condTree, clauses, blockers, applications, matchers, lambdas)
+ pathVar, qs, q2s, insts, guards._2, quantifiers, condVars, exprVars, condTree,
+ clauses, blockers, applications, matchers, lambdas, keyDeps, key)
}
}
@@ -130,9 +140,10 @@ class QuantificationManager[T](encoder: TemplateEncoder[T]) extends LambdaManage
private val known = new IncrementalSet[T]
private val lambdaAxioms = new IncrementalSet[(LambdaTemplate[T], Seq[(Identifier, T)])]
+ private val templates = new IncrementalMap[(Expr, Seq[T]), T]
override protected def incrementals: List[IncrementalState] =
- List(quantifications, instCtx, handled, ignored, known, lambdaAxioms) ++ super.incrementals
+ List(quantifications, instCtx, handled, ignored, known, lambdaAxioms, templates) ++ super.incrementals
private sealed abstract class MatcherKey(val tpe: TypeTree)
private case class CallerKey(caller: T, tt: TypeTree) extends MatcherKey(tt)
@@ -441,12 +452,12 @@ class QuantificationManager[T](encoder: TemplateEncoder[T]) extends LambdaManage
instantiation = instantiation withClause encoder.mkEquals(enabler, optEnabler.get)
}
- val baseSubstMap = exprVars.map { case (id, idT) => idT -> encoder.encodeId(id) } ++
- freshConds(pathVar._1 -> enabler, condVars, condTree)
- val lambdaSubstMap = lambdas map (lambda => lambda.ids._2 -> encoder.encodeId(lambda.ids._1))
- val substMap = subst.mapValues(Matcher.argValue) ++ baseSubstMap ++ lambdaSubstMap ++ instanceSubst(enablers)
+ val baseSubst = subst.mapValues(Matcher.argValue) ++ instanceSubst(enablers)
+ val (substMap, inst) = Template.substitution(encoder, QuantificationManager.this,
+ exprVars, condVars, condTree, Seq.empty, lambdas, baseSubst, pathVar._1, enabler)
if (!skip(substMap)) {
+ instantiation ++= inst
instantiation ++= Template.instantiate(encoder, QuantificationManager.this,
clauses, blockers, applications, Seq.empty, Map.empty[T, Set[Matcher[T]]], lambdas, substMap)
@@ -671,66 +682,63 @@ class QuantificationManager[T](encoder: TemplateEncoder[T]) extends LambdaManage
instantiation
}
- def instantiateQuantification(template: QuantificationTemplate[T], substMap: Map[T, T]): Instantiation[T] = {
- val quantified = template.quantifiers.map(_._2).toSet
- val matchQuorums = extractQuorums(quantified, template.matchers.flatMap(_._2).toSet, template.lambdas)
-
- var instantiation = Instantiation.empty[T]
-
- val qs = for (matchers <- matchQuorums) yield {
- val newQ = encoder.encodeId(template.qs._1)
- val subst = substMap + (template.qs._2 -> newQ)
+ def instantiateQuantification(template: QuantificationTemplate[T]): (T, Instantiation[T]) = {
+ templates.get(template.key) match {
+ case Some(idT) =>
+ (idT, Instantiation.empty)
- val substituter = encoder.substitute(subst)
- val quantification = new Quantification(
- template.pathVar._1 -> substituter(template.start),
- template.qs._1 -> newQ,
- template.q2s, template.insts, template.guardVar,
- quantified,
- matchers map (_.substitute(substituter)),
- template.matchers map { case (b, ms) => substituter(b) -> ms.map(_.substitute(substituter)) },
- template.condVars,
- template.exprVars,
- template.condTree,
- template.clauses map substituter,
- template.blockers map { case (b, fis) =>
- substituter(b) -> fis.map(fi => fi.copy(args = fi.args.map(substituter)))
- },
- template.applications map { case (b, fas) =>
- substituter(b) -> fas.map(fa => fa.copy(caller = substituter(fa.caller), args = fa.args.map(substituter)))
- },
- template.lambdas map (_.substitute(substituter))
- )
+ case None =>
+ val qT = encoder.encodeId(template.qs._1)
+ val quantified = template.quantifiers.map(_._2).toSet
+ val matchQuorums = extractQuorums(quantified, template.matchers.flatMap(_._2).toSet, template.lambdas)
- quantifications += quantification
+ var instantiation = Instantiation.empty[T]
- val newCtx = new InstantiationContext()
- for ((b,m) <- instCtx.instantiated) {
- instantiation ++= newCtx.instantiate(b, m)(quantification)
- }
- instCtx.merge(newCtx)
+ val qs = for (matchers <- matchQuorums) yield {
+ val newQ = encoder.encodeId(template.qs._1)
+ val substituter = encoder.substitute(Map(template.qs._2 -> newQ))
+
+ val quantification = new Quantification(
+ template.pathVar,
+ template.qs._1 -> newQ,
+ template.q2s, template.insts, template.guardVar,
+ quantified, matchers, template.matchers,
+ template.condVars, template.exprVars, template.condTree,
+ template.clauses map substituter, // one clause depends on 'q' (and therefore 'newQ')
+ template.blockers, template.applications, template.lambdas
+ )
+
+ quantifications += quantification
+
+ val newCtx = new InstantiationContext()
+ for ((b,m) <- instCtx.instantiated) {
+ instantiation ++= newCtx.instantiate(b, m)(quantification)
+ }
+ instCtx.merge(newCtx)
- quantification.qs._2
- }
+ quantification.qs._2
+ }
- instantiation = instantiation withClause {
- val newQs =
- if (qs.isEmpty) trueT
- else if (qs.size == 1) qs.head
- else encoder.mkAnd(qs : _*)
- encoder.mkImplies(substMap(template.start), encoder.mkEquals(substMap(template.qs._2), newQs))
- }
+ instantiation = instantiation withClause {
+ val newQs =
+ if (qs.isEmpty) trueT
+ else if (qs.size == 1) qs.head
+ else encoder.mkAnd(qs : _*)
+ encoder.mkImplies(template.start, encoder.mkEquals(qT, newQs))
+ }
- val quantifierSubst = uniformSubst(template.quantifiers)
- val substituter = encoder.substitute(substMap ++ quantifierSubst)
+ val quantifierSubst = uniformSubst(template.quantifiers)
+ val substituter = encoder.substitute(quantifierSubst)
- for {
- (_, ms) <- template.matchers; m <- ms
- sm = m.substitute(substituter)
- if !instCtx.corresponding(sm).exists(_._2.args == sm.args)
- } instantiation ++= instCtx.instantiate(Set.empty, sm)(quantifications.toSeq : _*)
+ for {
+ (_, ms) <- template.matchers; m <- ms
+ sm = m.substitute(substituter)
+ if !instCtx.corresponding(sm).exists(_._2.args == sm.args)
+ } instantiation ++= instCtx.instantiate(Set.empty, sm)(quantifications.toSeq : _*)
- instantiation
+ templates += template.key -> qT
+ (qT, instantiation)
+ }
}
def instantiateMatcher(blocker: T, matcher: Matcher[T]): Instantiation[T] = {
diff --git a/src/main/scala/leon/solvers/templates/TemplateGenerator.scala b/src/main/scala/leon/solvers/templates/TemplateGenerator.scala
index 60ddb145058eeb33b4bcb796307fba87d586d52f..fc570b83d85e5a4298ae52f01ead895f928a2061 100644
--- a/src/main/scala/leon/solvers/templates/TemplateGenerator.scala
+++ b/src/main/scala/leon/solvers/templates/TemplateGenerator.scala
@@ -453,8 +453,10 @@ class TemplateGenerator[T](val encoder: TemplateEncoder[T],
Equals(Variable(q), And(Variable(q2), Variable(inst)))
) ++ qGuarded.getOrElse(pathVar, Seq.empty)))
+ val dependencies: Map[Identifier, T] = vars.filterNot(quantifiers).map(id => id -> localSubst(id)).toMap
val template = QuantificationTemplate[T](encoder, manager, pathVar -> encodedCond(pathVar),
- qs, q2, inst, guard, idQuantifiers zip trQuantifiers, qConds, qExprs, qTree, allGuarded, qTemplates, localSubst)
+ qs, q2, inst, guard, idQuantifiers zip trQuantifiers, qConds, qExprs, qTree, allGuarded, qTemplates, localSubst,
+ dependencies, Forall(quantifiers.toSeq.sortBy(_.uniqueName).map(ValDef(_)), flatConj))
registerQuantification(template)
Variable(q)
}
diff --git a/src/main/scala/leon/solvers/templates/TemplateManager.scala b/src/main/scala/leon/solvers/templates/TemplateManager.scala
index bb6629ec16988a79eb686259aea4fa32c6111dbb..32f07a271ce45cbb76e2444f425b593561ce3358 100644
--- a/src/main/scala/leon/solvers/templates/TemplateManager.scala
+++ b/src/main/scala/leon/solvers/templates/TemplateManager.scala
@@ -76,24 +76,11 @@ trait Template[T] { self =>
lazy val start = pathVar._2
- private var substCache : Map[Seq[T],Map[T,T]] = Map.empty
-
def instantiate(aVar: T, args: Seq[T]): Instantiation[T] = {
-
- val baseSubstMap : Map[T,T] = substCache.get(args) match {
- case Some(subst) => subst
- case None =>
- val subst = exprVars.map { case (id, idT) => idT -> encoder.encodeId(id) } ++
- manager.freshConds(pathVar._1 -> aVar, condVars, condTree) ++
- (this.args zip args)
- substCache += args -> subst
- subst
- }
-
- val lambdaSubstMap = lambdas.map(lambda => lambda.ids._2 -> encoder.encodeId(lambda.ids._1))
- val quantificationSubstMap = quantifications.map(q => q.qs._2 -> encoder.encodeId(q.qs._1))
- val substMap : Map[T,T] = baseSubstMap ++ lambdaSubstMap ++ quantificationSubstMap + (start -> aVar)
- instantiate(substMap)
+ val (substMap, instantiation) = Template.substitution(encoder, manager,
+ condVars, exprVars, condTree, quantifications, lambdas,
+ (this.args zip args).toMap + (start -> aVar), pathVar._1, aVar)
+ instantiation ++ instantiate(substMap)
}
protected def instantiate(substMap: Map[T, T]): Instantiation[T] = {
@@ -231,6 +218,57 @@ object Template {
(clauses, encodedBlockers, encodedApps, encodedMatchers, stringRepr)
}
+ def substitution[T](
+ encoder: TemplateEncoder[T],
+ manager: QuantificationManager[T],
+ condVars: Map[Identifier, T],
+ exprVars: Map[Identifier, T],
+ condTree: Map[Identifier, Set[Identifier]],
+ quantifications: Seq[QuantificationTemplate[T]],
+ lambdas: Seq[LambdaTemplate[T]],
+ baseSubst: Map[T, T],
+ pathVar: Identifier,
+ aVar: T
+ ): (Map[T, T], Instantiation[T]) = {
+ var subst = exprVars.map { case (id, idT) => idT -> encoder.encodeId(id) } ++
+ manager.freshConds(pathVar -> aVar, condVars, condTree) ++
+ baseSubst
+
+ // /!\ CAREFUL /!\
+ // We have to be wary while computing the lambda subst map since lambdas can
+ // depend on each other. However, these dependencies cannot be cyclic so it
+ // suffices to make sure the traversal order is correct.
+ var instantiation : Instantiation[T] = Instantiation.empty
+ var seen : Set[LambdaTemplate[T]] = Set.empty
+
+ val lambdaKeys = lambdas.map(lambda => lambda.ids._1 -> lambda).toMap
+ def extractSubst(lambda: LambdaTemplate[T]): Unit = {
+ for {
+ dep <- lambda.dependencies.flatMap(p => lambdaKeys.get(p._1))
+ if !seen(dep)
+ } extractSubst(dep)
+
+ if (!seen(lambda)) {
+ val substLambda = lambda.substitute(encoder.substitute(subst))
+ val (idT, inst) = manager.instantiateLambda(substLambda)
+ instantiation ++= inst
+ subst += lambda.ids._2 -> idT
+ seen += lambda
+ }
+ }
+
+ for (l <- lambdas) extractSubst(l)
+
+ for (q <- quantifications) {
+ val substQuant = q.substitute(encoder.substitute(subst))
+ val (qT, inst) = manager.instantiateQuantification(substQuant)
+ instantiation ++= inst
+ subst += q.qs._2 -> qT
+ }
+
+ (subst, instantiation)
+ }
+
def instantiate[T](
encoder: TemplateEncoder[T],
manager: QuantificationManager[T],
@@ -252,10 +290,6 @@ object Template {
var instantiation: Instantiation[T] = (newClauses, newBlockers, Map.empty)
- for (lambda <- lambdas) {
- instantiation ++= manager.instantiateLambda(lambda.substitute(substituter))
- }
-
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)
@@ -265,10 +299,6 @@ object Template {
instantiation ++= manager.instantiateMatcher(bp, m.substitute(substituter))
}
- for (q <- quantifications) {
- instantiation ++= manager.instantiateQuantification(q, substMap)
- }
-
instantiation
}
}
diff --git a/src/main/scala/leon/solvers/templates/UnrollingBank.scala b/src/main/scala/leon/solvers/templates/UnrollingBank.scala
index d1c4432a3c69f1882c9b4a1787a12dc8cf64f520..f96d44239eef30f2c9ef4d758924c322036591f9 100644
--- a/src/main/scala/leon/solvers/templates/UnrollingBank.scala
+++ b/src/main/scala/leon/solvers/templates/UnrollingBank.scala
@@ -240,16 +240,22 @@ class UnrollingBank[T <% Printable](ctx: LeonContext, templateGenerator: Templat
callInfos --= ids
val apps = ids.flatMap(id => blockerToApps.get(id))
- val thisAppInfos = apps.map(app => app -> appInfos(app))
+ val thisAppInfos = apps.map(app => app -> {
+ val (gen, _, _, _, infos) = appInfos(app)
+ (gen, infos)
+ })
+
blockerToApps --= ids
appInfos --= apps
- for ((app, (_, _, _, _, infos)) <- thisAppInfos if infos.nonEmpty) {
+ for ((app, (_, infos)) <- thisAppInfos if infos.nonEmpty) {
val extension = extendAppBlock(app, infos)
reporter.debug(" -> extending lambda blocker: " + extension)
newClauses :+= extension
}
+ var fastAppInfos : Map[(T, App[T]), (Int, Set[TemplateAppInfo[T]])] = Map.empty
+
for ((id, (gen, _, _, infos)) <- newCallInfos; info @ TemplateCallInfo(tfd, args) <- infos) {
var newCls = Seq[T]()
@@ -268,13 +274,24 @@ class UnrollingBank[T <% Printable](ctx: LeonContext, templateGenerator: Templat
//reporter.debug(template)
val (newExprs, callBlocks, appBlocks) = template.instantiate(defBlocker, args)
- val blockExprs = freshAppBlocks(appBlocks.keys)
+
+ // we handle obvious appBlocks in an immediate manner in order to increase
+ // performance for folds that just pass a lambda around to recursive calls
+ val (fastApps, nextApps) = appBlocks.partition(p => p._2.toSeq match {
+ case Seq(TemplateAppInfo(_, equals, _)) if equals == manager.trueT => true
+ case _ => false
+ })
+
+ fastAppInfos ++= fastApps.mapValues(gen -> _)
+
+ val blockExprs = freshAppBlocks(nextApps.keys)
for((b, newInfos) <- callBlocks) {
registerCallBlocker(nextGeneration(gen), b, newInfos)
}
- for ((app, newInfos) <- appBlocks) {
+ for ((app, newInfos) <- nextApps) {
+ println(app -> newInfos)
registerAppBlocker(nextGeneration(gen), app, newInfos)
}
@@ -296,7 +313,7 @@ class UnrollingBank[T <% Printable](ctx: LeonContext, templateGenerator: Templat
newClauses ++= newCls
}
- for ((app @ (b, _), (gen, _, _, _, infos)) <- thisAppInfos; info @ TemplateAppInfo(template, equals, args) <- infos) {
+ for ((app @ (b, _), (gen, infos)) <- thisAppInfos ++ fastAppInfos; info @ TemplateAppInfo(template, equals, args) <- infos) {
var newCls = Seq.empty[T]
val lambdaBlocker = lambdaBlockers.get(info) match {