diff --git a/src/main/scala/inox/ast/SymbolOps.scala b/src/main/scala/inox/ast/SymbolOps.scala
index deadd9826ab8dd9aadb434d52bd23492ecccca41..515cc2c45d630b2418ae4f9fb5cec9adb4d7c0ad 100644
--- a/src/main/scala/inox/ast/SymbolOps.scala
+++ b/src/main/scala/inox/ast/SymbolOps.scala
@@ -116,7 +116,7 @@ trait SymbolOps { self: TypeOps =>
val remainingIds: MutableMap[Type, List[Identifier]] = MutableMap.empty ++ typedIds.toMap
def getId(e: Expr): Identifier = {
- val tpe = bestRealType(e.getType)
+ val tpe = e.getType
val newId = remainingIds.get(tpe) match {
case Some(x :: xs) =>
remainingIds += tpe -> xs
diff --git a/src/main/scala/inox/solvers/unrolling/LambdaTemplates.scala b/src/main/scala/inox/solvers/unrolling/LambdaTemplates.scala
index 16510afc7fe73c9c88d31b674bb3ccbb259a6e45..9ced30029faf11da39d2fb35019bfefce3b76426 100644
--- a/src/main/scala/inox/solvers/unrolling/LambdaTemplates.scala
+++ b/src/main/scala/inox/solvers/unrolling/LambdaTemplates.scala
@@ -55,7 +55,6 @@ trait LambdaTemplates { self: Templates =>
ids: (Variable, Encoded),
pathVar: (Variable, Encoded),
arguments: Seq[(Variable, Encoded)],
- closures: Seq[(Variable, Encoded)],
condVars: Map[Variable, Encoded],
exprVars: Map[Variable, Encoded],
condTree: Map[Variable, Set[Variable]],
@@ -72,14 +71,14 @@ trait LambdaTemplates { self: Templates =>
val tpe = ids._1.getType.asInstanceOf[FunctionType]
val (clauses, blockers, applications, matchers, templateString) =
Template.encode(pathVar, arguments, condVars, exprVars, guardedExprs, equations,
- lambdas, quantifications, substMap = baseSubstMap + ids ++ closures, optApp = Some(id -> tpe))
+ lambdas, quantifications, substMap = baseSubstMap + ids, optApp = Some(id -> tpe))
val lambdaString : () => String = () => {
"Template for lambda " + ids._1 + ": " + lambda + " is :\n" + templateString()
}
new LambdaTemplate(
- ids, pathVar, arguments, closures,
+ ids, pathVar, arguments,
condVars, exprVars, condTree,
clauses, blockers, applications, matchers,
lambdas, quantifications,
@@ -201,7 +200,6 @@ trait LambdaTemplates { self: Templates =>
val ids: (Variable, Encoded),
val pathVar: (Variable, Encoded),
val arguments: Seq[(Variable, Encoded)],
- val closures: Seq[(Variable, Encoded)],
val condVars: Map[Variable, Encoded],
val exprVars: Map[Variable, Encoded],
val condTree: Map[Variable, Set[Variable]],
@@ -222,7 +220,7 @@ trait LambdaTemplates { self: Templates =>
def substitute(substituter: Encoded => Encoded, msubst: Map[Encoded, Matcher]): LambdaTemplate = new LambdaTemplate(
ids._1 -> substituter(ids._2),
pathVar._1 -> substituter(pathVar._2),
- arguments, closures, condVars, exprVars, condTree,
+ arguments, condVars, exprVars, condTree,
clauses.map(substituter),
blockers.map { case (b, fis) => substituter(b) -> fis.map(_.substitute(substituter, msubst)) },
applications.map { case (b, apps) => substituter(b) -> apps.map(_.substitute(substituter, msubst)) },
@@ -235,10 +233,10 @@ trait LambdaTemplates { self: Templates =>
/** This must be called right before returning the clauses in [[structure.instantiation]]! */
def concretize(idT: Encoded): LambdaTemplate = {
assert(!isConcrete, "Can't concretize concrete lambda template")
- val substituter = mkSubstituter(Map(ids._2 -> idT) ++ (closures.map(_._2) zip structure.locals.map(_._2)))
+ val substituter = mkSubstituter(Map(ids._2 -> idT))
new LambdaTemplate(
ids._1 -> idT,
- pathVar, arguments, closures, condVars, exprVars, condTree,
+ pathVar, arguments, condVars, exprVars, condTree,
clauses map substituter,
blockers.map { case (b, fis) => b -> fis.map(_.substitute(substituter, Map.empty)) },
applications.map { case (b, apps) => b -> apps.map(_.substitute(substituter, Map.empty)) },
diff --git a/src/main/scala/inox/solvers/unrolling/TemplateGenerator.scala b/src/main/scala/inox/solvers/unrolling/TemplateGenerator.scala
index dc519c71903f51543629a96e516c8b555ead4b1a..0bd78b8a124511c692ff3af4382f33026ae3b3a0 100644
--- a/src/main/scala/inox/solvers/unrolling/TemplateGenerator.scala
+++ b/src/main/scala/inox/solvers/unrolling/TemplateGenerator.scala
@@ -278,21 +278,16 @@ trait TemplateGenerator { self: Templates =>
val (struct, deps) = normalizeStructure(l)
val sortedDeps = deps.toSeq.sortBy(_._1.id.uniqueName)
- val idDeps = sortedDeps.map(_._1)
- val trDeps = idDeps.map(id => encodeSymbol(id))
- val lid = Variable(FreshIdentifier("lambda", true), bestRealType(l.getType))
- val clauses = liftedEquals(lid, struct, idArgs, inlineFirst = true)
+ val depsByScope: Seq[(Variable, Expr)] = {
+ def rec(v: Variable): Seq[Variable] =
+ (exprOps.variablesOf(deps(v)) & deps.keySet).toSeq.flatMap(rec) :+ v
+ deps.keys.toSeq.flatMap(rec).distinct.map(v => v -> deps(v))
+ }
val localSubst: Map[Variable, Encoded] = substMap ++ condVars ++ exprVars ++ lambdaVars
- val clauseSubst: Map[Variable, Encoded] = localSubst ++ (idArgs zip trArgs) ++ (idDeps zip trDeps)
- val (lambdaConds, lambdaExprs, lambdaTree, lambdaGuarded, lambdaEqs, lambdaTemplates, lambdaQuants) =
- clauses.foldLeft(emptyClauses)((clsSet, cls) => clsSet ++ mkClauses(pathVar, cls, clauseSubst))
-
- val ids: (Variable, Encoded) = lid -> storeLambda(lid)
-
val (depSubst, (depConds, depExprs, depTree, depGuarded, depEqs, depLambdas, depQuants)) =
- sortedDeps.foldLeft[(Map[Variable, Encoded], TemplateClauses)](localSubst -> emptyClauses) {
+ depsByScope.foldLeft[(Map[Variable, Encoded], TemplateClauses)](localSubst -> emptyClauses) {
case ((depSubst, clsSet), (v, expr)) =>
if (!exprOps.isSimple(expr)) {
val (e, cls @ (_, _, _, _, _, lmbds, quants)) = mkExprClauses(pathVar, expr, depSubst)
@@ -322,8 +317,36 @@ trait TemplateGenerator { self: Templates =>
struct, dependencies, pathVar -> encodedCond(pathVar), depClosures,
depConds, depExprs, depTree, depClauses, depCalls, depApps, depMatchers, depLambdas, depQuants)
+ val isNormalForm: Boolean = {
+ def extractBody(e: Expr): (Seq[ValDef], Expr) = e match {
+ case Lambda(args, body) =>
+ val (nextArgs, nextBody) = extractBody(body)
+ (args ++ nextArgs, nextBody)
+ case _ => (Seq.empty, e)
+ }
+
+ extractBody(struct) match {
+ case (params, ApplicationExtractor(caller: Variable, args)) =>
+ (params.map(_.toVariable) == args) && (deps.get(caller) match {
+ case Some(_: Application | _: FunctionInvocation) => true
+ case _ => false
+ })
+ case _ => false
+ }
+ }
+
+ val realLambda = if (isNormalForm) l else struct
+ val lid = Variable(FreshIdentifier("lambda", true), bestRealType(l.getType))
+ val clauses = liftedEquals(lid, realLambda, idArgs, inlineFirst = true)
+
+ val clauseSubst: Map[Variable, Encoded] = depSubst ++ (idArgs zip trArgs)
+ val (lambdaConds, lambdaExprs, lambdaTree, lambdaGuarded, lambdaEqs, lambdaTemplates, lambdaQuants) =
+ clauses.foldLeft(emptyClauses)((clsSet, cls) => clsSet ++ mkClauses(pathVar, cls, clauseSubst))
+
+ val ids: (Variable, Encoded) = lid -> storeLambda(lid)
+
val template = LambdaTemplate(ids, pathVar -> encodedCond(pathVar),
- idArgs zip trArgs, idDeps zip trDeps, lambdaConds, lambdaExprs, lambdaTree,
+ idArgs zip trArgs, lambdaConds, lambdaExprs, lambdaTree,
lambdaGuarded, lambdaEqs, lambdaTemplates, lambdaQuants, structure, depSubst, l)
registerLambda(template)
lid