diff --git a/src/main/scala/inox/ast/SymbolOps.scala b/src/main/scala/inox/ast/SymbolOps.scala index 515cc2c45d630b2418ae4f9fb5cec9adb4d7c0ad..19933077158ec14afd6810bff6184e67ac482029 100644 --- a/src/main/scala/inox/ast/SymbolOps.scala +++ b/src/main/scala/inox/ast/SymbolOps.scala @@ -132,7 +132,7 @@ trait SymbolOps { self: TypeOps => def transformId(id: Identifier, tpe: Type): Identifier = subst.get(Variable(id, tpe)) match { case Some(Variable(newId, _)) => newId - case Some(_) => scala.sys.error("Should never happen!") + case Some(_) => id case None => varSubst.get(id) match { case Some(newId) => newId case None => @@ -151,7 +151,7 @@ trait SymbolOps { self: TypeOps => case Variable(id, tpe) => Variable(transformId(id, tpe), tpe) - case Let(vd, e, b) if (!onlySimple || isSimple(e)) && (variablesOf(e) & vars).nonEmpty => + case Let(vd, e, b) if (!onlySimple || isSimple(e)) && (variablesOf(e) & vars).isEmpty => val newId = getId(e) transform(replaceFromSymbols(Map(vd.toVariable -> Variable(newId, vd.tpe)), b)) diff --git a/src/main/scala/inox/solvers/unrolling/LambdaTemplates.scala b/src/main/scala/inox/solvers/unrolling/LambdaTemplates.scala index 9ced30029faf11da39d2fb35019bfefce3b76426..0f61233639b4d1f6b5318ad63a601f2fc320c1a6 100644 --- a/src/main/scala/inox/solvers/unrolling/LambdaTemplates.scala +++ b/src/main/scala/inox/solvers/unrolling/LambdaTemplates.scala @@ -169,7 +169,7 @@ trait LambdaTemplates { self: Templates => * already been found, then the associated instantiations must already appear * in those handled by the solver. */ - lazy val (key, instantiation, locals) = { + lazy val (key, instantiation, locals, instantiationSubst) = { val (substMap, substInst) = Template.substitution( condVars, exprVars, condTree, lambdas, quantifications, Map.empty, pathVar._2) val tmplInst = Template.instantiate(clauses, blockers, applications, matchers, substMap) @@ -181,7 +181,7 @@ trait LambdaTemplates { self: Templates => val sortedDeps = exprOps.variablesOf(lambda).toSeq.sortBy(_.id.uniqueName) val locals = sortedDeps zip deps - (key, instantiation, locals) + (key, instantiation, locals, substMap.mapValues(_.encoded)) } override def equals(that: Any): Boolean = that match { @@ -233,7 +233,7 @@ 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)) + val substituter = mkSubstituter(Map(ids._2 -> idT) ++ structure.instantiationSubst) new LambdaTemplate( ids._1 -> idT, pathVar, arguments, condVars, exprVars, condTree, diff --git a/src/main/scala/inox/solvers/unrolling/TemplateGenerator.scala b/src/main/scala/inox/solvers/unrolling/TemplateGenerator.scala index 0bd78b8a124511c692ff3af4382f33026ae3b3a0..12e758e6acad3555cb207e8e01d3e8115fd88c19 100644 --- a/src/main/scala/inox/solvers/unrolling/TemplateGenerator.scala +++ b/src/main/scala/inox/solvers/unrolling/TemplateGenerator.scala @@ -279,9 +279,27 @@ trait TemplateGenerator { self: Templates => val (struct, deps) = normalizeStructure(l) val sortedDeps = deps.toSeq.sortBy(_._1.id.uniqueName) + 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 depsByScope: Seq[(Variable, Expr)] = { def rec(v: Variable): Seq[Variable] = - (exprOps.variablesOf(deps(v)) & deps.keySet).toSeq.flatMap(rec) :+ v + (exprOps.variablesOf(deps(v)) & deps.keySet - v).toSeq.flatMap(rec) :+ v deps.keys.toSeq.flatMap(rec).distinct.map(v => v -> deps(v)) } @@ -290,7 +308,8 @@ trait TemplateGenerator { self: Templates => 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) + val normalExpr = if (!isNormalForm) simplifyHOFunctions(expr) else expr + val (e, cls @ (_, _, _, _, _, lmbds, quants)) = mkExprClauses(pathVar, normalExpr, depSubst) val clauseSubst = depSubst ++ lmbds.map(_.ids) ++ quants.flatMap(_.mapping) (depSubst + (v -> mkEncoder(clauseSubst)(e)), clsSet ++ cls) } else { @@ -317,24 +336,6 @@ 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)