Finished up E-matching templates

src/main/scala/leon/solvers/templates/QuantificationManager.scala

@@ -10,8 +10,362 @@ import purescala.Types._
 
 import Instantiation._
 
+import scala.collection.mutable.{Map => MutableMap, Set => MutableSet}
+
+class QuantificationTemplate[T](
+  val quantificationManager: QuantificationManager[T],
+  val start: T,
+  val qs: (Identifier, T),
+  val holdVar: T,
+  val guardVar: T,
+  val quantifiers: Seq[(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]]) {
+
+  def instantiate(blocker: T): Instantiation[T] = {
+    quantificationManager.instantiateQuantification(blocker, this)
+  }
+}
+
+object QuantificationTemplate {
+  def apply[T](
+    encoder: TemplateEncoder[T],
+    quantificationManager: QuantificationManager[T],
+    pathVar: (Identifier, T),
+    qs: (Identifier, T),
+    holder: Identifier,
+    guard: Identifier,
+    quantifiers: Seq[(Identifier, T)],
+    condVars: Map[Identifier, T],
+    exprVars: Map[Identifier, T],
+    guardedExprs: Map[Identifier, Seq[Expr]],
+    lambdas: Map[T, LambdaTemplate[T]],
+    subst: Map[Identifier, T]
+  ): QuantificationTemplate[T] = {
+
+    val holders: (Identifier, T) = holder -> encoder.encodeId(holder)
+    val guards: (Identifier, T) = guard -> encoder.encodeId(guard)
+
+    val (clauses, blockers, applications, _) =
+      Template.encode(encoder, pathVar, quantifiers, condVars, exprVars, guardedExprs, lambdas,
+        substMap = subst + holders + guards)
+
+    new QuantificationTemplate[T](quantificationManager,
+      pathVar._2, qs, holders._2, guards._2, quantifiers,
+      condVars, exprVars, clauses, blockers, applications, lambdas)
+  }
+}
+
 trait QuantificationManager[T] { self : LambdaManager[T] =>
 
+  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, currentCount - count).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)
+  }
+
+  private type Bindings = Set[(Option[T], FunctionType, 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 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 def known(tpe: FunctionType, idT: T): Boolean = freeLambdas(tpe)(idT) || byID.isDefinedAt(idT)
+
+  private class Quantification (
+    var holdVar: T,
+    val guardVar: 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]]) {
+
+    def substitute(subst: Map[T, T]) = {
+      val substituter = encoder.substitute(subst)
+
+      new Quantification (
+        holdVar, guardVar, condVars, exprVars,
+        clauses map substituter,
+        blockers map { case (b, fis) =>
+          substituter(b) -> fis.map(fi => fi.copy(args = fi.args.map(substituter)))
+        },
+        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))
+        }
+      )
+    }
+
+    def instantiate(blocker: T, app: App[T], quantifierSubst: Map[T, T]): Instantiation[T] = {
+      val App(caller, tpe, args) = app
+
+      // 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
+        // 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)))
+        // 2. build the instantiation mapping associated to the chosen current application binding
+        .flatMap { bindingApp => binders
+          // 2.1. select all potential matches for each quantified application
+          .map { case qapp @ App(qcaller, qtpe, qargs) =>
+            if (qapp == bindingApp) {
+              bindingApp -> Set(blocker -> app)
+            } else {
+              val instances = self.applications(qtpe).filter {
+                case (b, app @ App(caller, _, _)) => qcaller == caller || !known(qtpe, 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 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)
+
+              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[(T, App[T], App[T])]]] (List(Nil)) {
+            case (mappings, (qapp, instances)) => instances.toList.flatMap {
+              case (b, app) => mappings.map(mapping => mapping :+ (b, app, qapp))
+            }
+          }
+        }
+
+      var instantiation = Instantiation.empty[T]
+
+      for (mapping <- appMappings) {
+        var constraints: List[T] = Nil
+        var subst: Map[T, T] = quantifierSubst
+
+        for {
+          (b, App(qcaller, _, qargs), App(caller, _, args)) <- mapping
+          _ = constraints :+= b
+          _ = 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
+        }
+
+        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 substMap = subst ++ lambdaSubstMap + (guardVar -> enabler) + (holdVar -> holder)
+        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 = 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 ++= self.instantiateLambda(newIdT, newTemplate)
+        }
+
+        for ((b, apps) <- newApplications; app <- apps) {
+          instantiation ++= self.instantiateApp(b, app)
+        }
+
+        holdVar = holder
+      }
+
+      instantiation
+    }
+  }
+
+  def instantiateQuantification(blocker: T, template: QuantificationTemplate[T]): Instantiation[T] = {
+
+    val quantification: Quantification = {
+      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)
+        }.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 q = new Quantification(
+        template.holdVar,
+        template.guardVar,
+        template.condVars,
+        template.exprVars,
+        template.clauses,
+        template.blockers,
+        template.applications,
+        template.lambdas,
+        bindingApps
+      )
+
+      val tpeCounts   = template.quantifiers.groupBy(_._1.getType).mapValues(_.map(_._2).toSeq)
+      val substMap    = tpeCounts.flatMap { case (tpe, idTs) => idTs zip standardQuantifiers(tpe, idTs.size) }.toMap
+      q.substitute(substMap + (template.start -> blocker))
+    }
+
+    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)
+    }
+
+    val qBindings: Bindings = quantification.binders.flatMap {
+      case App(caller, tpe, args) => args.zipWithIndex.collect {
+        case (qid, idx) if quantified(qid) =>
+          (if (known(tpe, 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 pairs: Set[(T, T)] = qBindings.flatMap { case (optIdT, tpe, idx, q) =>
+      val matches = typeMap(tpe -> idx) ++ optIdT.toSeq.flatMap(idT => callerMap(idT -> idx))
+      matches.map(q2 => q -> q2)
+    }
+
+    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 newQuantifications = for (mapping <- mappings) yield {
+      val ph = nextHolder()
+
+      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) }
+
+      val substituter = encoder.substitute(substMap)
+
+      new Quantification(ph, quantification.guardVar,
+        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.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))
+        }
+      )
+    }
+
+    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)
+    }
+
+    instantiation = (instantiation._1 :+ eqClause, instantiation._2, instantiation._3)
+
+    instantiatedApps = for ((b, app, qSubst) <- instantiatedApps) 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
+      }
+
+      for (q <- newQuantifications) {
+        instantiation ++= q.instantiate(b, app, nqSubst)
+      }
+
+      (b, app, nqSubst)
+    }
+
+    for ((b, apps) <- quantification.applications; app <- apps) {
+      instantiatedApps :+= (b, app, quantifierSubst)
+    }
+
+    instantiation
+  }
+
+  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)
+    }
+
+    instantiatedApps :+= (blocker, app, quantifierSubst)
+    instantiation
+  }
+
+  /*
   private class QuantificationScope(
     val quantifiedApps: List[App[T]],
     val quantifiers: Map[Identifier, T],
@@ -70,7 +424,7 @@ trait QuantificationManager[T] { self : LambdaManager[T] =>
 
     val quantifiers: Seq[(Identifier, T)] = quantifierVars.map(id => id -> encoder.encodeId(id))
     val quantified: Set[T] = quantifiers.map(_._2).toSet
-    val pathVar = startVar -> encoder.encodeId(startVar)
+    val pathVar = startVar -> subst(startVar)
     val (clauses, blockers, apps, _) = Template.encode(encoder, pathVar, quantifiers, condVars, exprVars, guardedExprs, lambdas, subst)
 
     val bindingApps: Set[App[T]] = {
@@ -125,11 +479,13 @@ trait QuantificationManager[T] { self : LambdaManager[T] =>
         case (mappings, (_, pairs)) => pairs.toList.flatMap(p => mappings.map(mapping => mapping + p))
       }
 
-    val (allClauses, allBlockers, allApps) = {
+    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)
@@ -145,17 +501,15 @@ trait QuantificationManager[T] { self : LambdaManager[T] =>
           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)
+      (allClauses, allBlockers, allApps, quantifiedApps)
     }
 
-    val quantifiedApps: Set[(T, App[T])] = for {
-      (b, bApps) <- allApps.toSet
-      app @ App(caller, tpe, args) <- bApps
-      if args exists quantified
-    } yield (b, app)
-
     scopes = new QuantificationScope(
       currentScope.quantifiedApps ++ quantifiedApps,
       currentScope.quantifiers ++ quantifiers,
@@ -233,14 +587,15 @@ trait QuantificationManager[T] { self : LambdaManager[T] =>
         case (id, idT) if !subst.isDefinedAt(idT) => idT -> encoder.encodeId(id)
       }
 
-      val bp = encoder.encodeId(startId)
+      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 = clauses.map(substituter)
+      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)))
       }
@@ -264,4 +619,5 @@ trait QuantificationManager[T] { self : LambdaManager[T] =>
 
     instantiation
   }
+  */
 }

src/main/scala/leon/solvers/templates/TemplateGenerator.scala

@@ -72,16 +72,16 @@ class TemplateGenerator[T](val encoder: TemplateEncoder[T],
 
     val substMap : Map[Identifier, T] = arguments.toMap + pathVar
 
-    val (bodyConds, bodyExprs, bodyGuarded, bodyLambdas) = if (isRealFunDef) {
+    val (bodyConds, bodyExprs, bodyGuarded, bodyLambdas, bodyQuantifications) = if (isRealFunDef) {
       invocationEqualsBody.map(expr => mkClauses(start, expr, substMap)).getOrElse {
-        (Map[Identifier,T](), Map[Identifier,T](), Map[Identifier,Seq[Expr]](), Map[T,LambdaTemplate[T]]())
+        (Map[Identifier,T](), Map[Identifier,T](), Map[Identifier,Seq[Expr]](), Map[T,LambdaTemplate[T]](), Seq[QuantificationTemplate[T]]())
       }
     } else {
       mkClauses(start, lambdaBody.get, substMap)
     }
 
     // Now the postcondition.
-    val (condVars, exprVars, guardedExprs, lambdas) = tfd.postcondition match {
+    val (condVars, exprVars, guardedExprs, lambdas, quantifications) = tfd.postcondition match {
       case Some(post) =>
         val newPost : Expr = application(matchToIfThenElse(post), Seq(invocation))
 
@@ -96,19 +96,19 @@ class TemplateGenerator[T](val encoder: TemplateEncoder[T],
             newPost
           }
 
-        val (postConds, postExprs, postGuarded, postLambdas) = mkClauses(start, postHolds, substMap)
+        val (postConds, postExprs, postGuarded, postLambdas, postQuantifications) = mkClauses(start, postHolds, substMap)
         val allGuarded = (bodyGuarded.keys ++ postGuarded.keys).map { k => 
           k -> (bodyGuarded.getOrElse(k, Seq.empty) ++ postGuarded.getOrElse(k, Seq.empty))
         }.toMap
 
-        (bodyConds ++ postConds, bodyExprs ++ postExprs, allGuarded, bodyLambdas ++ postLambdas)
+        (bodyConds ++ postConds, bodyExprs ++ postExprs, allGuarded, bodyLambdas ++ postLambdas, bodyQuantifications ++ postQuantifications)
 
       case None =>
-        (bodyConds, bodyExprs, bodyGuarded, bodyLambdas)
+        (bodyConds, bodyExprs, bodyGuarded, bodyLambdas, bodyQuantifications)
     }
 
     val template = FunctionTemplate(tfd, encoder, lambdaManager,
-      pathVar, arguments, condVars, exprVars, guardedExprs, lambdas, isRealFunDef)
+      pathVar, arguments, condVars, exprVars, guardedExprs, quantifications, lambdas, isRealFunDef)
     cache += tfd -> template
     template
   }
@@ -125,7 +125,7 @@ class TemplateGenerator[T](val encoder: TemplateEncoder[T],
   }
 
   def mkClauses(pathVar: Identifier, expr: Expr, substMap: Map[Identifier, T]):
-               (Map[Identifier,T], Map[Identifier,T], Map[Identifier, Seq[Expr]], Map[T, LambdaTemplate[T]]) = {
+               (Map[Identifier,T], Map[Identifier,T], Map[Identifier, Seq[Expr]], Map[T, LambdaTemplate[T]], Seq[QuantificationTemplate[T]]) = {
 
     var condVars = Map[Identifier, T]()
     @inline def storeCond(id: Identifier) : Unit = condVars += id -> encoder.encodeId(id)
@@ -152,6 +152,10 @@ class TemplateGenerator[T](val encoder: TemplateEncoder[T],
       idT
     }
 
+    var quantifications = Seq[QuantificationTemplate[T]]()
+    @inline def registerQuantification(quantification: QuantificationTemplate[T]): Unit =
+      quantifications :+= quantification
+
     var lambdas = Map[T, LambdaTemplate[T]]()
     @inline def registerLambda(idT: T, lambda: LambdaTemplate[T]) : Unit = lambdas += idT -> lambda
 
@@ -263,26 +267,49 @@ class TemplateGenerator[T](val encoder: TemplateEncoder[T],
           val lid = FreshIdentifier("lambda", l.getType, true)
           val clause = appliedEquals(Variable(lid), l)
 
-          val localSubst : Map[Identifier, T] = substMap ++ condVars ++ exprVars ++ lambdaVars
-          val clauseSubst : Map[Identifier, T] = localSubst ++ (idArgs zip trArgs)
-          val (lambdaConds, lambdaExprs, lambdaGuarded, lambdaTemplates) = mkClauses(pathVar, clause, clauseSubst)
+          val localSubst: Map[Identifier, T] = substMap ++ condVars ++ exprVars ++ lambdaVars
+          val clauseSubst: Map[Identifier, T] = localSubst ++ (idArgs zip trArgs)
+          val (lambdaConds, lambdaExprs, lambdaGuarded, lambdaTemplates, lambdaQuants) = mkClauses(pathVar, clause, clauseSubst)
+          assert(lambdaQuants.isEmpty, "Unhandled quantification in lambdas in " + clause)
 
           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), idArgs zip trArgs, lambdaConds, lambdaExprs, lambdaGuarded, lambdaTemplates, localSubst, dependencies, l)
+          val template = LambdaTemplate(ids, encoder, lambdaManager, pathVar -> encodedCond(pathVar),
+            idArgs zip trArgs, lambdaConds, lambdaExprs, lambdaGuarded, lambdaTemplates, localSubst, dependencies, l)
           registerLambda(ids._2, template)
 
           Variable(lid)
 
-        case Operator(as, r) => r(as.map(a => rec(pathVar, a)))
+        case f @ Forall(args, body) =>
+          val idQuantifiers : Seq[Identifier] = args.map(_.id)
+          val trQuantifiers : Seq[T] = idQuantifiers.map(encoder.encodeId)
+
+          val q: Identifier = FreshIdentifier("q", BooleanType)
+          val ph: Identifier = FreshIdentifier("ph", BooleanType)
+          val guard: Identifier = FreshIdentifier("guard", BooleanType)
+
+          val clause = Equals(Variable(q), And(Variable(ph), Implies(Variable(guard), body)))
 
+          val qs: (Identifier, T) = q -> encoder.encodeId(q)
+          val localSubst: Map[Identifier, T] = substMap ++ condVars ++ exprVars ++ lambdaVars
+          val clauseSubst: Map[Identifier, T] = localSubst ++ (idQuantifiers zip trQuantifiers)
+          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),
+            qs, ph, guard, idQuantifiers zip trQuantifiers, qConds, qExprs, qGuarded, qTemplates, localSubst)
+          registerQuantification(template)
+
+          Variable(q)
+
+        case Operator(as, r) => r(as.map(a => rec(pathVar, a)))
       }
     }
 
     val p = rec(pathVar, expr)
     storeGuarded(pathVar, p)
 
-    (condVars, exprVars, guardedExprs, lambdas)
+    (condVars, exprVars, guardedExprs, lambdas, quantifications)
   }
 
 }

src/main/scala/leon/solvers/templates/Templates.scala

@@ -54,6 +54,7 @@ trait Template[T] { self =>
   val clauses : Seq[T]
   val blockers : Map[T, Set[TemplateCallInfo[T]]]
   val applications : Map[T, Set[App[T]]]
+  val quantifications: Seq[QuantificationTemplate[T]]
   val lambdas : Map[T, LambdaTemplate[T]]
 
   private var substCache : Map[Seq[T],Map[T,T]] = Map.empty
@@ -232,6 +233,7 @@ object FunctionTemplate {
     condVars: Map[Identifier, T],
     exprVars: Map[Identifier, T],
     guardedExprs: Map[Identifier, Seq[Expr]],
+    quantifications: Seq[QuantificationTemplate[T]],
     lambdas: Map[T, LambdaTemplate[T]],
     isRealFunDef: Boolean
   ) : FunctionTemplate[T] = {
@@ -257,6 +259,7 @@ object FunctionTemplate {
       clauses,
       blockers,
       applications,
+      quantifications,
       lambdas,
       isRealFunDef,
       funString
@@ -275,6 +278,7 @@ class FunctionTemplate[T] private(
   val clauses: Seq[T],
   val blockers: Map[T, Set[TemplateCallInfo[T]]],
   val applications: Map[T, Set[App[T]]],
+  val quantifications: Seq[QuantificationTemplate[T]],
   val lambdas: Map[T, LambdaTemplate[T]],
   isRealFunDef: Boolean,
   stringRepr: () => String) extends Template[T] {
@@ -393,6 +397,9 @@ class LambdaTemplate[T] private (
   private[templates] val structuralKey: Lambda,
   stringRepr: () => String) extends Template[T] {
 
+  // Universal quantification is not allowed inside closure bodies!
+  val quantifications: Seq[QuantificationTemplate[T]] = Seq.empty
+
   val tpe = id.getType.asInstanceOf[FunctionType]
 
   def substitute(substMap: Map[T,T]): LambdaTemplate[T] = {