diff --git a/src/main/scala/leon/solvers/templates/LambdaManager.scala b/src/main/scala/leon/solvers/templates/LambdaManager.scala
index d82a03e5562bba04afe7c6d53f7026318f42a4d0..e7282e4f18b293bc37dd4f560794f3a18ca4e271 100644
--- a/src/main/scala/leon/solvers/templates/LambdaManager.scala
+++ b/src/main/scala/leon/solvers/templates/LambdaManager.scala
@@ -10,37 +10,50 @@ import purescala.TreeOps._
import purescala.TypeTrees._
class LambdaManager[T](encoder: TemplateEncoder[T]) {
- private var byID : Map[T, LambdaTemplate[T]] = Map.empty
- private var byType : Map[TypeTree, Set[(T, LambdaTemplate[T])]] = Map.empty.withDefaultValue(Set.empty)
- private var quantified : Map[TypeTree, Set[T]] = Map.empty.withDefaultValue(Set.empty)
- private var applications : Map[TypeTree, Set[(T, App[T])]] = Map.empty.withDefaultValue(Set.empty)
- private var blockedApplications : Map[(T, App[T]), Set[T]] = Map.empty.withDefaultValue(Set.empty)
+ private type IdMap = Map[T, LambdaTemplate[T]]
+ private var byIDStack : List[IdMap] = List(Map.empty)
+ private def byID : IdMap = byIDStack.head
+ private def byID_=(map: IdMap) : Unit = {
+ byIDStack = map :: byIDStack.tail
+ }
+
+ private type TypeMap = Map[TypeTree, Set[(T, LambdaTemplate[T])]]
+ private var byTypeStack : List[TypeMap] = List(Map.empty.withDefaultValue(Set.empty))
+ private def byType : TypeMap = byTypeStack.head
+ private def byType_=(map: TypeMap) : Unit = {
+ byTypeStack = map :: byTypeStack.tail
+ }
- private var globalBlocker : Option[T] = None
- private var previousGlobals : Set[T] = Set.empty
+ private type ApplicationMap = Map[TypeTree, Set[(T, App[T])]]
+ private var applicationsStack : List[ApplicationMap] = List(Map.empty.withDefaultValue(Set.empty))
+ private def applications : ApplicationMap = applicationsStack.head
+ private def applications_=(map: ApplicationMap) : Unit = {
+ applicationsStack = map :: applicationsStack.tail
+ }
- def quantify(args: Seq[(TypeTree, T)]): Unit = {
- args.foreach(p => quantified += p._1 -> (quantified(p._1) + p._2))
+ def push(): Unit = {
+ byIDStack = byID :: byIDStack
+ byTypeStack = byType :: byTypeStack
+ applicationsStack = applications :: applicationsStack
}
- def instantiate(apps: Map[T, Set[App[T]]], lambdas: Map[T, LambdaTemplate[T]]) : (Seq[T], Map[T, Set[TemplateInfo[T]]]) = {
+ def pop(lvl: Int): Unit = {
+ byIDStack = byIDStack.drop(lvl)
+ byTypeStack = byTypeStack.drop(lvl)
+ applicationsStack = applicationsStack.drop(lvl)
+ }
+
+ def instantiate(apps: Map[T, Set[App[T]]], lambdas: Map[T, LambdaTemplate[T]]) : (Seq[T], Map[T, Set[TemplateCallInfo[T]]], Map[(T, App[T]), Set[TemplateAppInfo[T]]]) = {
var clauses : Seq[T] = Seq.empty
- var blockers : Map[T, Set[TemplateInfo[T]]] = Map.empty.withDefaultValue(Set.empty)
+ var callBlockers : Map[T, Set[TemplateCallInfo[T]]] = Map.empty.withDefaultValue(Set.empty)
+ var appBlockers : Map[(T, App[T]), Set[TemplateAppInfo[T]]] = Map.empty.withDefaultValue(Set.empty)
def mkBlocker(blockedApp: (T, App[T]), lambda: (T, LambdaTemplate[T])) : Unit = {
val (_, App(caller, tpe, args)) = blockedApp
val (idT, template) = lambda
- val unrollingBlocker = encoder.encodeId(FreshIdentifier("unrolled", true).setType(BooleanType))
-
- val conj = encoder.mkAnd(encoder.mkEquals(idT, caller), template.start, unrollingBlocker)
-
- val templateBlocker = encoder.encodeId(FreshIdentifier("b", true).setType(BooleanType))
- val constraint = encoder.mkEquals(templateBlocker, conj)
-
- clauses :+= constraint
- blockedApplications += (blockedApp -> (blockedApplications(blockedApp) + templateBlocker))
- blockers += (unrollingBlocker -> Set(TemplateAppInfo(template, templateBlocker, args)))
+ val equals = encoder.mkEquals(idT, caller)
+ appBlockers += (blockedApp -> (appBlockers(blockedApp) + TemplateAppInfo(template, equals, args)))
}
for (lambda @ (idT, template) <- lambdas) {
@@ -54,35 +67,28 @@ class LambdaManager[T](encoder: TemplateEncoder[T]) {
for ((b, fas) <- apps; app @ App(caller, tpe, args) <- fas) {
if (byID contains caller) {
- val (newClauses, newBlockers) = byID(caller).instantiate(b, args)
+ val (newClauses, newCalls, newApps) = byID(caller).instantiate(b, args)
+
clauses ++= newClauses
- newBlockers.foreach(p => blockers += p._1 -> (blockers(p._1) ++ p._2))
+ newCalls.foreach(p => callBlockers += p._1 -> (callBlockers(p._1) ++ p._2))
+ newApps.foreach(p => appBlockers += p._1 -> (appBlockers(p._1) ++ p._2))
} else {
+ val key = b -> app
+
+ // make sure that even if byType(tpe) is empty, app is recorded in blockers
+ // so that UnrollingBank will generate the initial block!
+ if (!(appBlockers contains key)) appBlockers += key -> Set.empty
+
for (lambda <- byType(tpe)) {
- mkBlocker(b -> app, lambda)
+ mkBlocker(key, lambda)
}
- applications += tpe -> (applications(tpe) + (b -> app))
+ applications += tpe -> (applications(tpe) + key)
}
}
- (clauses, blockers)
- }
-
- def guards : Seq[T] = {
- previousGlobals ++= globalBlocker
- val globalGuard = encoder.encodeId(FreshIdentifier("lambda_phaser", true).setType(BooleanType))
- globalBlocker = Some(globalGuard)
-
- (for (((b, App(caller, tpe, _)), tbs) <- blockedApplications) yield {
- val qbs = quantified(tpe).map(l => encoder.mkEquals(caller, l))
- val or = encoder.mkOr((tbs ++ qbs).toSeq : _*)
- // TODO: get global blocker
- val guard = encoder.mkAnd(globalGuard, encoder.mkNot(or))
- encoder.mkImplies(guard, encoder.mkNot(b))
- }).toSeq ++ previousGlobals.map(encoder.mkNot(_))
+ (clauses, callBlockers, appBlockers)
}
- def assumption : T = globalBlocker.get
}
diff --git a/src/main/scala/leon/solvers/templates/TemplateGenerator.scala b/src/main/scala/leon/solvers/templates/TemplateGenerator.scala
index 114eafe8d4ceb12a50947605be3a1c16b934c671..75fd757a69704a170e0afd95648a4bfc8648bc80 100644
--- a/src/main/scala/leon/solvers/templates/TemplateGenerator.scala
+++ b/src/main/scala/leon/solvers/templates/TemplateGenerator.scala
@@ -18,7 +18,7 @@ class TemplateGenerator[T](val encoder: TemplateEncoder[T]) {
private var cache = Map[TypedFunDef, FunctionTemplate[T]]()
private var cacheExpr = Map[Expr, FunctionTemplate[T]]()
- private[templates] val lambdaManager = new LambdaManager[T](encoder)
+ private val lambdaManager = new LambdaManager[T](encoder)
def mkTemplate(body: Expr): FunctionTemplate[T] = {
if (cacheExpr contains body) {
diff --git a/src/main/scala/leon/solvers/templates/TemplateInfo.scala b/src/main/scala/leon/solvers/templates/TemplateInfo.scala
index 80ed670fd0844b673202748227a75b6bfc9b2a30..110e658a301c2805968124905d9137d8e267114c 100644
--- a/src/main/scala/leon/solvers/templates/TemplateInfo.scala
+++ b/src/main/scala/leon/solvers/templates/TemplateInfo.scala
@@ -7,16 +7,14 @@ package templates
import purescala.Definitions.TypedFunDef
import purescala.TypeTrees.TypeTree
-sealed abstract class TemplateInfo[T]
-
-case class TemplateCallInfo[T](tfd: TypedFunDef, args: Seq[T]) extends TemplateInfo[T] {
+case class TemplateCallInfo[T](tfd: TypedFunDef, args: Seq[T]) {
override def toString = {
tfd.signature+args.mkString("(", ", ", ")")
}
}
-case class TemplateAppInfo[T](template: LambdaTemplate[T], b: T, args: Seq[T]) extends TemplateInfo[T] {
+case class TemplateAppInfo[T](template: LambdaTemplate[T], equals: T, args: Seq[T]) {
override def toString = {
- template.id + "|" + b + "|" + args.mkString("(", ",", ")")
+ template.id + "|" + equals + args.mkString("(", ",", ")")
}
}
diff --git a/src/main/scala/leon/solvers/templates/Templates.scala b/src/main/scala/leon/solvers/templates/Templates.scala
index 05e7a4c01708938d0066c01bf751ba0170dc1f9d..c9273660c8b99259e72a959b39029987f1401564 100644
--- a/src/main/scala/leon/solvers/templates/Templates.scala
+++ b/src/main/scala/leon/solvers/templates/Templates.scala
@@ -35,7 +35,7 @@ trait Template[T] { self =>
private var substCache : Map[Seq[T],Map[T,T]] = Map.empty
private var lambdaCache : Map[(T, Map[T,T]), T] = Map.empty
- def instantiate(aVar: T, args: Seq[T]): (Seq[T], Map[T, Set[TemplateInfo[T]]]) = {
+ def instantiate(aVar: T, args: Seq[T]): (Seq[T], Map[T, Set[TemplateCallInfo[T]]], Map[(T, App[T]), Set[TemplateAppInfo[T]]]) = {
val baseSubstMap : Map[T,T] = substCache.get(args) match {
case Some(subst) => subst
@@ -80,14 +80,14 @@ trait Template[T] { self =>
substituter(idT) -> lambda.substitute(substMap)
}
- val (appClauses, appBlockers) = lambdaManager.instantiate(newApplications, newLambdas)
+ val (appClauses, appBlockers, appApps) = lambdaManager.instantiate(newApplications, newLambdas)
val allClauses = newClauses ++ appClauses ++ lambdaClauses
val allBlockers = (newBlockers.keys ++ appBlockers.keys).map { k =>
k -> (newBlockers.getOrElse(k, Set.empty) ++ appBlockers.getOrElse(k, Set.empty))
}.toMap
- (allClauses, allBlockers)
+ (allClauses, allBlockers, appApps)
}
override def toString : String = "Instantiated template"
diff --git a/src/main/scala/leon/solvers/templates/UnrollingBank.scala b/src/main/scala/leon/solvers/templates/UnrollingBank.scala
index 8d8b604de83a4f31951580761dbf25f52b44a157..fc6782dd1fecc021dcdbaff195b7792a8800359d 100644
--- a/src/main/scala/leon/solvers/templates/UnrollingBank.scala
+++ b/src/main/scala/leon/solvers/templates/UnrollingBank.scala
@@ -18,58 +18,99 @@ class UnrollingBank[T](reporter: Reporter, templateGenerator: TemplateGenerator[
implicit val debugSection = utils.DebugSectionSolver
private val encoder = templateGenerator.encoder
- private val lambdaManager = templateGenerator.lambdaManager
// Keep which function invocation is guarded by which guard,
// also specify the generation of the blocker.
- private var blockersInfoStack = List[Map[T, (Int, Int, T, Set[TemplateInfo[T]])]](Map())
+ private var callInfoStack = List[Map[T, (Int, Int, T, Set[TemplateCallInfo[T]])]](Map())
+ private def callInfo = callInfoStack.head
+ private def callInfo_= (v: Map[T, (Int, Int, T, Set[TemplateCallInfo[T]])]) = {
+ callInfoStack = v :: callInfoStack.tail
+ }
// Function instantiations have their own defblocker
- private var defBlockers = Map[TemplateInfo[T], T]()
+ private var defBlockersStack = List[Map[TemplateCallInfo[T], T]](Map.empty)
+ private def defBlockers = defBlockersStack.head
+ private def defBlockers_= (v: Map[TemplateCallInfo[T], T]) : Unit = {
+ defBlockersStack = v :: defBlockersStack.tail
+ }
+
+ private var appInfoStack = List[Map[(T, App[T]), (Int, Int, T, T, Set[TemplateAppInfo[T]])]](Map())
+ private def appInfo = appInfoStack.head
+ private def appInfo_= (v: Map[(T, App[T]), (Int, Int, T, T, Set[TemplateAppInfo[T]])]) : Unit = {
+ appInfoStack = v :: appInfoStack.tail
+ }
- def blockersInfo = blockersInfoStack.head
+ private var appBlockersStack = List[Map[(T, App[T]), T]](Map.empty)
+ private def appBlockers = appBlockersStack.head
+ private def appBlockers_= (v: Map[(T, App[T]), T]) : Unit = {
+ appBlockersStack = v :: appBlockersStack.tail
+ }
+
+ private var blockerToAppStack = List[Map[T, (T, App[T])]](Map.empty)
+ private def blockerToApp = blockerToAppStack.head
+ private def blockerToApp_= (v: Map[T, (T, App[T])]) : Unit = {
+ blockerToAppStack = v :: blockerToAppStack.tail
+ }
- def blockersInfo_= (v: Map[T, (Int, Int, T, Set[TemplateInfo[T]])]) = {
- blockersInfoStack = v :: blockersInfoStack.tail
+ private var functionVarsStack = List[Map[TypeTree, Set[T]]](Map.empty.withDefaultValue(Set.empty))
+ private def functionVars = functionVarsStack.head
+ private def functionVars_= (v: Map[TypeTree, Set[T]]) : Unit = {
+ functionVarsStack = v :: functionVarsStack.tail
}
def push() {
- blockersInfoStack = blockersInfo :: blockersInfoStack
+ appInfoStack = appInfo :: appInfoStack
+ callInfoStack = callInfo :: callInfoStack
+ defBlockersStack = defBlockers :: defBlockersStack
+ blockerToAppStack = blockerToApp :: blockerToAppStack
+ functionVarsStack = functionVars :: functionVarsStack
+ appBlockersStack = appBlockers :: appBlockersStack
}
def pop(lvl: Int) {
- blockersInfoStack = blockersInfoStack.drop(lvl)
+ appInfoStack = appInfoStack.drop(lvl)
+ callInfoStack = callInfoStack.drop(lvl)
+ defBlockersStack = defBlockersStack.drop(lvl)
+ blockerToAppStack = blockerToAppStack.drop(lvl)
+ functionVarsStack = functionVarsStack.drop(lvl)
+ appBlockersStack = appBlockersStack.drop(lvl)
}
def dumpBlockers = {
- blockersInfo.groupBy(_._2._1).toSeq.sortBy(_._1).foreach { case (gen, entries) =>
- reporter.debug("--- "+gen)
+ val generations = (callInfo.map(_._2._1).toSet ++ appInfo.map(_._2._1).toSet).toSeq.sorted
+ generations.foreach { generation =>
+ reporter.debug("--- " + generation)
- for (((bast), (gen, origGen, ast, fis)) <- entries) {
- reporter.debug(f". $bast%15s ~> "+fis.mkString(", "))
+ for ((b, (gen, origGen, ast, fis)) <- callInfo if gen == generation) {
+ reporter.debug(f". $b%15s ~> "+fis.mkString(", "))
+ }
+
+ for ((app, (gen, origGen, b, notB, infos)) <- appInfo if gen == generation) {
+ reporter.debug(f". $b%15s ~> "+infos.mkString(", "))
}
}
}
- def canUnroll = !blockersInfo.isEmpty
+ def canUnroll = !callInfo.isEmpty || !appInfo.isEmpty
- def currentBlockers = blockersInfo.map(_._2._3).toSeq :+ lambdaManager.assumption
+ def currentBlockers = callInfo.map(_._2._3).toSeq ++ appInfo.map(_._2._4).toSeq
def getBlockersToUnlock: Seq[T] = {
- if (!blockersInfo.isEmpty) {
- val minGeneration = blockersInfo.values.map(_._1).min
-
- blockersInfo.filter(_._2._1 == minGeneration).toSeq.map(_._1)
+ if (callInfo.isEmpty && appInfo.isEmpty) {
+ Seq.empty
} else {
- Seq()
+ val minGeneration = (callInfo.values.map(_._1) ++ appInfo.values.map(_._1)).min
+ val callBlocks = callInfo.filter(_._2._1 == minGeneration).toSeq.map(_._1)
+ val appBlocks = appInfo.values.filter(_._1 == minGeneration).toSeq.map(_._3)
+ callBlocks ++ appBlocks
}
}
- private def registerBlocker(gen: Int, id: T, fis: Set[TemplateInfo[T]]) {
+ private def registerCallBlocker(gen: Int, id: T, fis: Set[TemplateCallInfo[T]]) {
val notId = encoder.mkNot(id)
- blockersInfo.get(id) match {
+ callInfo.get(id) match {
case Some((exGen, origGen, _, exFis)) =>
// PS: when recycling `b`s, this assertion becomes dangerous.
// It's better to simply take the max of the generations.
@@ -77,12 +118,54 @@ class UnrollingBank[T](reporter: Reporter, templateGenerator: TemplateGenerator[
val minGen = gen min exGen
- blockersInfo += id -> (minGen, origGen, notId, fis++exFis)
+ callInfo += id -> (minGen, origGen, notId, fis++exFis)
+ case None =>
+ callInfo += id -> (gen, gen, notId, fis)
+ }
+ }
+
+ private def registerAppBlocker(gen: Int, app: (T, App[T]), info: Set[TemplateAppInfo[T]]) : Unit = {
+ appInfo.get(app) match {
+ case Some((exGen, origGen, b, notB, exInfo)) =>
+ val minGen = gen min exGen
+ appInfo += app -> (minGen, origGen, b, notB, exInfo ++ info)
+
case None =>
- blockersInfo += id -> (gen, gen, notId, fis)
+ val b = appBlockers.get(app) match {
+ case Some(b) => b
+ case None => encoder.encodeId(FreshIdentifier("b_lambda", true).setType(BooleanType))
+ }
+
+ val notB = encoder.mkNot(b)
+ appInfo += app -> (gen, gen, b, notB, info)
+ blockerToApp += b -> app
}
}
+ private def freshAppBlocks(apps: Traversable[(T, App[T])]) : Seq[T] = {
+ apps.filter(!appBlockers.isDefinedAt(_)).toSeq.map { case app @ (blocker, App(caller, tpe, _)) =>
+
+ val firstB = encoder.encodeId(FreshIdentifier("b_lambda", true).setType(BooleanType))
+ val freeEq = functionVars(tpe).toSeq.map(t => encoder.mkEquals(t, caller))
+ val clause = encoder.mkImplies(encoder.mkNot(encoder.mkOr((freeEq :+ firstB) : _*)), encoder.mkNot(blocker))
+
+ appBlockers += app -> firstB
+ clause
+ }
+ }
+
+ private def extendAppBlock(app: (T, App[T]), infos: Set[TemplateAppInfo[T]]) : T = {
+ assert(!appInfo.isDefinedAt(app), "appInfo -= app must have been called to ensure blocker freshness")
+ assert(appBlockers.isDefinedAt(app), "freshAppBlocks must have been called on app before it can be unlocked")
+
+ val nextB = encoder.encodeId(FreshIdentifier("b_lambda", true).setType(BooleanType))
+ val extension = encoder.mkOr((infos.map(_.equals).toSeq :+ nextB) : _*)
+ val clause = encoder.mkEquals(appBlockers(app), extension)
+
+ appBlockers += app -> nextB
+ clause
+ }
+
def getClauses(expr: Expr, bindings: Map[Expr, T]): Seq[T] = {
// OK, now this is subtle. This `getTemplate` will return
// a template for a "fake" function. Now, this template will
@@ -91,110 +174,146 @@ class UnrollingBank[T](reporter: Reporter, templateGenerator: TemplateGenerator[
val trArgs = template.tfd.params.map(vd => bindings(Variable(vd.id)))
- lambdaManager.quantify(template.tfd.params.collect {
- case vd if vd.tpe.isInstanceOf[FunctionType] =>
- vd.tpe -> bindings(vd.toVariable)
- })
+ for (vd <- template.tfd.params if vd.tpe.isInstanceOf[FunctionType]) {
+ functionVars += vd.tpe -> (functionVars(vd.tpe) + bindings(vd.toVariable))
+ }
// ...now this template defines clauses that are all guarded
// by that activating boolean. If that activating boolean is
// undefined (or false) these clauses have no effect...
- val (newClauses, newBlocks) =
- template.instantiate(template.start, trArgs)
+ val (newClauses, callBlocks, appBlocks) = template.instantiate(template.start, trArgs)
- for((i, fis) <- newBlocks) {
- registerBlocker(nextGeneration(0), i, fis)
+ val blockClauses = freshAppBlocks(appBlocks.keys)
+
+ for((b, infos) <- callBlocks) {
+ registerCallBlocker(nextGeneration(0), b, infos)
+ }
+
+ for ((app, infos) <- appBlocks) {
+ registerAppBlocker(nextGeneration(0), app, infos)
}
// ...so we must force it to true!
- template.start +: (newClauses ++ lambdaManager.guards)
+ template.start +: (newClauses ++ blockClauses)
}
def nextGeneration(gen: Int) = gen + 3
def decreaseAllGenerations() = {
- for ((block, (gen, origGen, ast, finvs)) <- blockersInfo) {
+ for ((block, (gen, origGen, ast, infos)) <- callInfo) {
// We also decrease the original generation here
- blockersInfo += block -> (math.max(1,gen-1), math.max(1,origGen-1), ast, finvs)
+ callInfo += block -> (math.max(1,gen-1), math.max(1,origGen-1), ast, infos)
+ }
+
+ for ((app, (gen, origGen, b, notB, infos)) <- appInfo) {
+ appInfo += app -> (math.max(1,gen-1), math.max(1,origGen-1), b, notB, infos)
}
}
def promoteBlocker(b: T) = {
- if (blockersInfo contains b) {
- val (gen, origGen, ast, fis) = blockersInfo(b)
+ if (callInfo contains b) {
+ val (gen, origGen, ast, fis) = callInfo(b)
- blockersInfo += b -> (1, origGen, ast, fis)
+ callInfo += b -> (1, origGen, ast, fis)
+ }
+
+ if (blockerToApp contains b) {
+ val app = blockerToApp(b)
+ val (gen, origGen, _, notB, infos) = appInfo(app)
+
+ appInfo += app -> (1, origGen, b, notB, infos)
}
}
def unrollBehind(ids: Seq[T]): Seq[T] = {
- assert(ids.forall(id => blockersInfo contains id))
+ assert(ids.forall(id => (callInfo contains id) || (blockerToApp contains id)))
var newClauses : Seq[T] = Seq.empty
- for (id <- ids) {
- val (gen, _, _, fis) = blockersInfo(id)
+ val callInfos = ids.flatMap(id => callInfo.get(id).map(id -> _))
+ callInfo = callInfo -- ids
- blockersInfo = blockersInfo - id
+ val apps = ids.flatMap(id => blockerToApp.get(id))
+ val appInfos = apps.map(app => app -> appInfo(app))
+ blockerToApp = blockerToApp -- ids
+ appInfo = appInfo -- apps
- var reintroducedSelf = false
+ for ((app, (_, _, _, _, infos)) <- appInfos) {
+ newClauses :+= extendAppBlock(app, infos)
+ }
- for (fi <- fis) {
- var newCls = Seq[T]()
+ for ((id, (gen, _, _, infos)) <- callInfos; info @ TemplateCallInfo(tfd, args) <- infos) {
+ var newCls = Seq[T]()
- fi match {
- case TemplateCallInfo(tfd, args) =>
- val defBlocker = defBlockers.get(fi) match {
- case Some(defBlocker) =>
- // we already have defBlocker => f(args) = body
- defBlocker
+ val defBlocker = defBlockers.get(info) match {
+ case Some(defBlocker) =>
+ // we already have defBlocker => f(args) = body
+ defBlocker
- case None =>
- // we need to define this defBlocker and link it to definition
- val defBlocker = encoder.encodeId(FreshIdentifier("d").setType(BooleanType))
- defBlockers += fi -> defBlocker
+ case None =>
+ // we need to define this defBlocker and link it to definition
+ val defBlocker = encoder.encodeId(FreshIdentifier("d").setType(BooleanType))
+ defBlockers += info -> defBlocker
- val template = templateGenerator.mkTemplate(tfd)
- reporter.debug(template)
+ val template = templateGenerator.mkTemplate(tfd)
+ reporter.debug(template)
- val (newExprs, newBlocks) = template.instantiate(defBlocker, args)
+ val (newExprs, callBlocks, appBlocks) = template.instantiate(defBlocker, args)
+ val blockExprs = freshAppBlocks(appBlocks.keys)
- for((i, fis2) <- newBlocks) {
- registerBlocker(nextGeneration(gen), i, fis2)
- }
+ for((b, newInfos) <- callBlocks) {
+ registerCallBlocker(nextGeneration(gen), b, newInfos)
+ }
- newCls ++= newExprs
- defBlocker
- }
+ for ((app, newInfos) <- appBlocks) {
+ registerAppBlocker(nextGeneration(gen), app, newInfos)
+ }
- // We connect it to the defBlocker: blocker => defBlocker
- if (defBlocker != id) {
- newCls ++= List(encoder.mkImplies(id, defBlocker))
- }
+ newCls ++= newExprs
+ newCls ++= blockExprs
+ defBlocker
+ }
- case TemplateAppInfo(template, b, args) =>
- reporter.debug(template)
- val (newExprs, newBlocks) = template.instantiate(b, args)
+ // We connect it to the defBlocker: blocker => defBlocker
+ if (defBlocker != id) {
+ newCls ++= List(encoder.mkImplies(id, defBlocker))
+ }
- for((i, fis2) <- newBlocks) {
- registerBlocker(nextGeneration(gen), i, fis2)
- }
+ reporter.debug("Unrolling behind "+info+" ("+newCls.size+")")
+ for (cl <- newCls) {
+ reporter.debug(" . "+cl)
+ }
- newCls ++= newExprs
- newCls :+= id
- }
+ newClauses ++= newCls
+ }
- reporter.debug("Unrolling behind "+fi+" ("+newCls.size+")")
- for (cl <- newCls) {
- reporter.debug(" . "+cl)
- }
+ for ((app @ (b, _), (gen, _, _, _, infos)) <- appInfos; info @ TemplateAppInfo(template, equals, args) <- infos) {
+ var newCls = Seq.empty[T]
+
+ val nb = encoder.encodeId(FreshIdentifier("b", true).setType(BooleanType))
+ newCls :+= encoder.mkEquals(nb, encoder.mkAnd(equals, b))
+
+ val (newExprs, callBlocks, appBlocks) = template.instantiate(nb, args)
+ val blockExprs = freshAppBlocks(appBlocks.keys)
- newClauses ++= newCls
+ for ((b, newInfos) <- callBlocks) {
+ registerCallBlocker(nextGeneration(gen), b, newInfos)
}
- }
+ for ((newApp, newInfos) <- appBlocks) {
+ registerAppBlocker(nextGeneration(gen), newApp, newInfos)
+ }
+
+ newCls ++= newExprs
+ newCls ++= blockExprs
- newClauses ++= lambdaManager.guards
+ reporter.debug("Unrolling behind "+info+" ("+newCls.size+")")
+ for (cl <- newCls) {
+ reporter.debug(" . "+cl)
+ }
+
+ newClauses ++= newCls
+ }
reporter.debug(s" - ${newClauses.size} new clauses")
//context.reporter.ifDebug { debug =>
diff --git a/src/test/resources/regression/verification/purescala/valid/Lambdas.scala b/src/test/resources/regression/verification/purescala/valid/Lambdas.scala
new file mode 100644
index 0000000000000000000000000000000000000000..36ae0c7ad7f8a68e36358d9e5adb885e7bb108da
--- /dev/null
+++ b/src/test/resources/regression/verification/purescala/valid/Lambdas.scala
@@ -0,0 +1,15 @@
+import leon.lang._
+
+object Lambdas {
+ def gen(x: Int): (Int) => Int = {
+ val f = (x: Int) => x + 1
+ val g = (x: Int) => x + 2
+ if (x > 0) g else f
+ }
+
+ def test(x: Int): Boolean = {
+ require(x > 0)
+ val f = gen(x)
+ f(x) == x + 2
+ }.holds
+}