diff --git a/src/main/scala/inox/ast/SymbolOps.scala b/src/main/scala/inox/ast/SymbolOps.scala
index 82831049c87d9443a3fee78a3ff95487c93ef570..c966e166d0a7233b31e2163043ed744875532606 100644
--- a/src/main/scala/inox/ast/SymbolOps.scala
+++ b/src/main/scala/inox/ast/SymbolOps.scala
@@ -184,12 +184,16 @@ trait SymbolOps { self: TypeOps =>
val (es, recons) = extractMatcher(map)
(key +: es, { case key +: es => MapApply(recons(es), key) })
+ case FunctionInvocation(id, tps, args) =>
+ (args, es => FunctionInvocation(id, tps, es))
+
case _ => (Seq(e), es => es.head)
}
def outer(vars: Set[Variable], body: Expr): Expr = {
// this registers the argument images into subst
val tvars = vars map (v => v.copy(id = transformId(v.id, v.tpe)))
+ subst --= tvars
def isLocal(e: Expr, path: Path): Boolean = {
val vs = variablesOf(e)
@@ -263,7 +267,6 @@ trait SymbolOps { self: TypeOps =>
case Variable(id, tpe) =>
Variable(transformId(id, tpe), tpe)
- /*
case (_: Application) | (_: MultiplicityInBag) | (_: ElementOfSet) | (_: MapApply) if (
!isLocal(e, path) &&
preserveApps
@@ -271,7 +274,6 @@ trait SymbolOps { self: TypeOps =>
val (es, recons) = extractMatcher(e)
val newEs = es.map(rec(_, path))
recons(newEs)
- */
case Let(vd, e, b) if (
isLocal(e, path) &&
@@ -306,15 +308,7 @@ trait SymbolOps { self: TypeOps =>
val newExpr = outer(args.map(_.toVariable).toSet, expr)
val bindings = args.map(vd => vd.copy(id = varSubst(vd.id)))
-
- val bindingVars = bindings.map(_.toVariable).toSet
- val freeVars = fixpoint { (vs: Set[Variable]) =>
- vs ++ subst.filter(p => vs(p._1)).flatMap(p => variablesOf(p._2)) -- bindingVars
- } (variablesOf(newExpr) -- bindings.map(_.toVariable))
-
- val bodySubst = subst.filter(p => freeVars(p._1)).toMap
-
- (bindings, newExpr, bodySubst)
+ (bindings, newExpr, subst.toMap)
}
def normalizeStructure(e: Expr): (Expr, Map[Variable, Expr]) = e match {
diff --git a/src/main/scala/inox/solvers/unrolling/QuantificationTemplates.scala b/src/main/scala/inox/solvers/unrolling/QuantificationTemplates.scala
index fac5a2213075f8a7883f945bcd31f087f1629793..b71a2b78e185bbc702e42490747d7bd1a2e9006d 100644
--- a/src/main/scala/inox/solvers/unrolling/QuantificationTemplates.scala
+++ b/src/main/scala/inox/solvers/unrolling/QuantificationTemplates.scala
@@ -918,90 +918,95 @@ trait QuantificationTemplates { self: Templates =>
def instantiateQuantification(template: QuantificationTemplate): (Map[Encoded, Encoded], Clauses) = {
templates.get(template.structure).orElse {
templates.collectFirst { case (s, t) if s subsumes template.structure => t }
- } match {
- case Some((_, _, map)) =>
- (map, Seq.empty)
-
- case None =>
- val newTemplate = template.concretize
- val clauses = new scala.collection.mutable.ListBuffer[Encoded]
- clauses ++= newTemplate.structure.instantiation
-
- val (inst, mapping): (Encoded, Map[Encoded, Encoded]) = newTemplate.polarity match {
- case Positive(guard) =>
- val axiom = new Axiom(newTemplate.pathVar._2, guard,
- newTemplate.quantifiers, newTemplate.condVars, newTemplate.exprVars, newTemplate.condTree,
- newTemplate.clauses, newTemplate.blockers, newTemplate.applications, newTemplate.matchers,
- newTemplate.lambdas, newTemplate.quantifications, newTemplate.pointers, newTemplate.body)
-
- quantifications += axiom
-
- for ((bs,m) <- handledMatchers) {
- clauses ++= axiom.instantiate(bs, m)
- }
+ }.map { case (tmpl, inst, _) =>
+ template.polarity match {
+ case Positive(guard) =>
+ (Map.empty[Encoded, Encoded], Seq(mkImplies(template.pathVar._2, inst)))
+ case Negative(insts) =>
+ (Map(insts._2 -> inst), Seq.empty[Encoded])
+ case Unknown(qs, q2s, insts, guard) =>
+ (Map(qs._2 -> inst), Seq.empty[Encoded])
+ }
+ }.getOrElse {
+ val newTemplate = template.concretize
+ val clauses = new scala.collection.mutable.ListBuffer[Encoded]
+ clauses ++= newTemplate.structure.instantiation
- val groundGen = currentGeneration + 3
- ignoredGrounds += groundGen -> (ignoredGrounds.getOrElse(groundGen, Set.empty) + axiom)
- (trueT, Map.empty)
+ val (inst, mapping): (Encoded, Map[Encoded, Encoded]) = newTemplate.polarity match {
+ case Positive(guard) =>
+ val axiom = new Axiom(newTemplate.pathVar._2, guard,
+ newTemplate.quantifiers, newTemplate.condVars, newTemplate.exprVars, newTemplate.condTree,
+ newTemplate.clauses, newTemplate.blockers, newTemplate.applications, newTemplate.matchers,
+ newTemplate.lambdas, newTemplate.quantifications, newTemplate.pointers, newTemplate.body)
- case Negative(insts) =>
- val instT = encodeSymbol(insts._1)
- val (substMap, substClauses) = Template.substitution(
- newTemplate.condVars, newTemplate.exprVars, newTemplate.condTree,
- newTemplate.lambdas, newTemplate.quantifications, newTemplate.pointers,
- Map(insts._2 -> Left(instT)), newTemplate.pathVar._2)
- clauses ++= substClauses
+ quantifications += axiom
- // this will call `instantiateMatcher` on all matchers in `newTemplate.matchers`
- clauses ++= Template.instantiate(newTemplate.clauses,
- newTemplate.blockers, newTemplate.applications, newTemplate.matchers, substMap)
+ for ((bs,m) <- handledMatchers) {
+ clauses ++= axiom.instantiate(bs, m)
+ }
- (instT, Map(insts._2 -> instT))
+ val groundGen = currentGeneration + 3
+ ignoredGrounds += groundGen -> (ignoredGrounds.getOrElse(groundGen, Set.empty) + axiom)
+ (trueT, Map.empty)
- case Unknown(qs, q2s, insts, guard) =>
- val qT = encodeSymbol(qs._1)
- val substituter = mkSubstituter(Map(qs._2 -> qT))
+ case Negative(insts) =>
+ val instT = encodeSymbol(insts._1)
+ val (substMap, substClauses) = Template.substitution(
+ newTemplate.condVars, newTemplate.exprVars, newTemplate.condTree,
+ newTemplate.lambdas, newTemplate.quantifications, newTemplate.pointers,
+ Map(insts._2 -> Left(instT)), newTemplate.pathVar._2)
+ clauses ++= substClauses
- val quantification = new GeneralQuantification(newTemplate.pathVar._2,
- qs._1 -> qT, q2s, insts, guard,
- newTemplate.quantifiers, newTemplate.condVars, newTemplate.exprVars, newTemplate.condTree,
- newTemplate.clauses map substituter, // one clause depends on 'qs._2' (and therefore 'qT')
- newTemplate.blockers, newTemplate.applications, newTemplate.matchers,
- newTemplate.lambdas, newTemplate.quantifications, newTemplate.pointers, newTemplate.body)
+ // this will call `instantiateMatcher` on all matchers in `newTemplate.matchers`
+ clauses ++= Template.instantiate(newTemplate.clauses,
+ newTemplate.blockers, newTemplate.applications, newTemplate.matchers, substMap)
- quantifications += quantification
+ (instT, Map(insts._2 -> instT))
- for ((bs,m) <- handledMatchers) {
- clauses ++= quantification.instantiate(bs, m)
- }
+ case Unknown(qs, q2s, insts, guard) =>
+ val qT = encodeSymbol(qs._1)
+ val substituter = mkSubstituter(Map(qs._2 -> qT))
- val freshQuantifiers = newTemplate.quantifiers.map(p => encodeSymbol(p._1))
- val freshSubst = mkSubstituter((newTemplate.quantifiers.map(_._2) zip freshQuantifiers).toMap)
- for ((b,ms) <- newTemplate.matchers; m <- ms) {
- clauses ++= instantiateMatcher(Set.empty[Encoded], m, false)
- // it is very rare that such instantiations are actually required, so we defer them
- val gen = currentGeneration + 20
- ignoredMatchers += ((gen, Set(b), m.substitute(freshSubst, Map.empty)))
- }
+ val quantification = new GeneralQuantification(newTemplate.pathVar._2,
+ qs._1 -> qT, q2s, insts, guard,
+ newTemplate.quantifiers, newTemplate.condVars, newTemplate.exprVars, newTemplate.condTree,
+ newTemplate.clauses map substituter, // one clause depends on 'qs._2' (and therefore 'qT')
+ newTemplate.blockers, newTemplate.applications, newTemplate.matchers,
+ newTemplate.lambdas, newTemplate.quantifications, newTemplate.pointers, newTemplate.body)
- clauses ++= quantification.ensureGrounds
- (qT, Map(qs._2 -> qT))
- }
+ quantifications += quantification
- clauses ++= templates.flatMap { case (key, (tmpl, tinst, _)) =>
- if (newTemplate.structure.body == tmpl.structure.body) {
- val eqConds = (newTemplate.structure.locals zip tmpl.structure.locals)
- .filter(p => p._1 != p._2)
- .map(p => mkEquals(p._1._2, p._2._2))
- val cond = mkAnd(newTemplate.pathVar._2 +: tmpl.pathVar._2 +: eqConds : _*)
- Some(mkImplies(cond, mkEquals(inst, tinst)))
- } else {
- None
+ for ((bs,m) <- handledMatchers) {
+ clauses ++= quantification.instantiate(bs, m)
}
+
+ val freshQuantifiers = newTemplate.quantifiers.map(p => encodeSymbol(p._1))
+ val freshSubst = mkSubstituter((newTemplate.quantifiers.map(_._2) zip freshQuantifiers).toMap)
+ for ((b,ms) <- newTemplate.matchers; m <- ms) {
+ clauses ++= instantiateMatcher(Set.empty[Encoded], m, false)
+ // it is very rare that such instantiations are actually required, so we defer them
+ val gen = currentGeneration + 20
+ ignoredMatchers += ((gen, Set(b), m.substitute(freshSubst, Map.empty)))
+ }
+
+ clauses ++= quantification.ensureGrounds
+ (qT, Map(qs._2 -> qT))
+ }
+
+ clauses ++= templates.flatMap { case (key, (tmpl, tinst, _)) =>
+ if (newTemplate.structure.body == tmpl.structure.body) {
+ val eqConds = (newTemplate.structure.locals zip tmpl.structure.locals)
+ .filter(p => p._1 != p._2)
+ .map(p => mkEquals(p._1._2, p._2._2))
+ val cond = mkAnd(newTemplate.pathVar._2 +: tmpl.pathVar._2 +: eqConds : _*)
+ Some(mkImplies(cond, mkEquals(inst, tinst)))
+ } else {
+ None
}
+ }
- templates += newTemplate.structure -> ((newTemplate, inst, mapping))
- (mapping, clauses.toSeq)
+ templates += newTemplate.structure -> ((newTemplate, inst, mapping))
+ (mapping, clauses.toSeq)
}
}