diff --git a/src/main/scala/inox/solvers/unrolling/LambdaTemplates.scala b/src/main/scala/inox/solvers/unrolling/LambdaTemplates.scala
index 0455d0fc8e1eeb1ff080a329584e71e630edadaf..d3f9e12cc78cea87bd77f638b44190c14b6bb4cd 100644
--- a/src/main/scala/inox/solvers/unrolling/LambdaTemplates.scala
+++ b/src/main/scala/inox/solvers/unrolling/LambdaTemplates.scala
@@ -170,7 +170,7 @@ trait LambdaTemplates { self: Templates =>
*/
lazy val (key, instantiation) = {
val (substMap, substInst) = Template.substitution(
- condVars, exprVars, condTree, lambdas, quantifications, Map.empty, pathVar._1, pathVar._2)
+ condVars, exprVars, condTree, lambdas, quantifications, Map.empty, pathVar._2)
val tmplInst = Template.instantiate(clauses, blockers, applications, matchers, substMap)
val substituter = mkSubstituter(substMap.mapValues(_.encoded))
diff --git a/src/main/scala/inox/solvers/unrolling/QuantificationTemplates.scala b/src/main/scala/inox/solvers/unrolling/QuantificationTemplates.scala
index fa43474eadd42e50c5463fe78e39e73494ba0a42..faa160dffcfa052badfc5ea63c1eeb61122314e1 100644
--- a/src/main/scala/inox/solvers/unrolling/QuantificationTemplates.scala
+++ b/src/main/scala/inox/solvers/unrolling/QuantificationTemplates.scala
@@ -68,13 +68,13 @@ trait QuantificationTemplates { self: Templates =>
*/
sealed abstract class Polarity {
def substitute(substituter: Encoded => Encoded): Polarity = this match {
- case Positive(guardVar) => Positive(guardVar)
+ case Positive(guard) => Positive(guard)
case Negative(insts) => Negative(insts._1 -> substituter(insts._2))
- case Unknown(qs, q2s, insts, guardVar) => Unknown(qs._1 -> substituter(qs._2), q2s, insts, guardVar)
+ case Unknown(qs, q2s, insts, guard) => Unknown(qs._1 -> substituter(qs._2), q2s, insts, guard)
}
}
- case class Positive(guardVar: Encoded) extends Polarity
+ case class Positive(guard: Encoded) extends Polarity
case class Negative(insts: (Variable, Encoded)) extends Polarity
/** Unknown quantification polarity.
@@ -88,7 +88,7 @@ trait QuantificationTemplates { self: Templates =>
* constructed where only certain `inst` variables are falsified. This is used to enable
* a powerful unrolling heuristic in the presence of both quantifiers and recursive functions.
*/
- case class Unknown(qs: (Variable, Encoded), q2s: (Variable, Encoded), insts: (Variable, Encoded), guardVar: Encoded) extends Polarity
+ case class Unknown(qs: (Variable, Encoded), q2s: (Variable, Encoded), insts: (Variable, Encoded), guard: Encoded) extends Polarity
class QuantificationTemplate private[QuantificationTemplates] (
val pathVar: (Variable, Encoded),
@@ -153,22 +153,24 @@ trait QuantificationTemplates { self: Templates =>
proposition: Forall
): (Option[Variable], QuantificationTemplate) = {
- val pT = mkEncoder(
- condVars ++ exprVars + pathVar ++ quantifiers ++
- substMap ++ lambdas.map(_.ids) ++ quantifications.flatMap(_.mapping)
- )(p)
-
- val (optVar, polarity, extraClauses, extraSubst) = optPol match {
+ val (optVar, polarity, extraGuarded, extraEqs, extraSubst): (
+ Option[Variable],
+ Polarity,
+ Map[Variable, Seq[Expr]],
+ Seq[Expr],
+ Map[Variable, Encoded]
+ ) = optPol match {
case Some(true) =>
val guard = encodeSymbol(Variable(FreshIdentifier("guard", true), BooleanType))
- val extraClause = mkImplies(mkAnd(pathVar._2, guard), pT)
- (None, Positive(guard), Seq(extraClause), Map(pathVar._1 -> guard))
+ val extraSubst = Map(pathVar._1 -> guard)
+ val extraGuarded = Map(pathVar._1 -> Seq(p))
+ (None, Positive(guard), extraGuarded, Seq.empty, extraSubst)
case Some(false) =>
val inst: Variable = Variable(FreshIdentifier("inst", true), BooleanType)
val insts = inst -> encodeSymbol(inst)
- val extraClause = mkImplies(pathVar._2, mkEquals(insts._2, pT))
- (Some(inst), Negative(insts), Seq(extraClause), Map.empty[Variable, Encoded])
+ val extraGuarded = Map(pathVar._1 -> Seq(Equals(inst, p)))
+ (Some(inst), Negative(insts), extraGuarded, Seq.empty, Map(insts))
case None =>
val q: Variable = Variable(FreshIdentifier("q", true), BooleanType)
@@ -181,11 +183,8 @@ trait QuantificationTemplates { self: Templates =>
val insts = inst -> encodeSymbol(inst)
val polarity = Unknown(qs, q2s, insts, guard)
- val extraClauses = Seq(
- mkImplies(pathVar._2, mkEquals(qs._2, mkAnd(q2s._2, insts._2))),
- mkImplies(pathVar._2, mkEquals(insts._2, mkImplies(guard, pT)))
- )
- (Some(q), polarity, extraClauses, Map(pathVar._1 -> guard))
+ val extraEqs = Seq(Equals(q, And(q2, inst)), Equals(inst, Implies(pathVar._1, p)))
+ (Some(q), polarity, Map.empty, extraEqs, Map(qs, q2s, insts) + (pathVar._1 -> guard))
}
// Note @nv: some hacky shit is going on here...
@@ -194,15 +193,16 @@ trait QuantificationTemplates { self: Templates =>
// works due to [[Template.encode]] injecting `pathVar` BEFORE `substMap` into the
// global encoding substitution.
val (clauses, blockers, applications, matchers, templateString) =
- Template.encode(pathVar, quantifiers, condVars, exprVars, guardedExprs,
- equations, lambdas, quantifications, substMap = substMap ++ extraSubst)
+ Template.encode(pathVar, quantifiers, condVars, exprVars,
+ extraGuarded merge guardedExprs, extraEqs ++ equations,
+ lambdas, quantifications, substMap = substMap ++ extraSubst)
val key = templateKey(proposition.args, proposition.body, substMap)
(optVar, new QuantificationTemplate(
- pathVar, polarity, quantifiers, condVars, exprVars, condTree,
- extraClauses ++ clauses, blockers, applications, matchers, lambdas, quantifications, key,
- proposition.body, () => "Template for " + proposition + " is :\n" + templateString()))
+ pathVar, polarity, quantifiers, condVars, exprVars, condTree, clauses,
+ blockers, applications, matchers, lambdas, quantifications, key, proposition.body,
+ () => "Template for " + proposition + " is :\n" + templateString()))
}
}
@@ -467,7 +467,8 @@ trait QuantificationTemplates { self: Templates =>
if (es.isEmpty) trueT else mkAnd(es.toSeq.sortBy(_.toString) : _*)
private[solvers] trait Quantification extends IncrementalState {
- val pathVar: (Variable, Encoded)
+ val blocker: Encoded
+ val guard: Encoded
val quantifiers: Seq[(Variable, Encoded)]
val condVars: Map[Variable, Encoded]
val exprVars: Map[Variable, Encoded]
@@ -483,8 +484,7 @@ trait QuantificationTemplates { self: Templates =>
val body: Expr
lazy val quantified: Set[Encoded] = quantifiers.map(_._2).toSet
- lazy val start = pathVar._2
- lazy val pathBlockers = blockerPath(start)
+ lazy val pathBlockers = blockerPath(blocker)
private val constraints: Seq[(Encoded, MatcherKey, Int)] = (for {
(_, ms) <- matchers
@@ -587,7 +587,7 @@ trait QuantificationTemplates { self: Templates =>
for (p @ (bs, subst, delay) <- substs if !handledSubsts.get(this).exists(_ contains (bs -> subst))) {
val totalDelay = delay + (3 * subst.values.collect { case Right(m) => totalDepth(m) }.sum)
if (totalDelay > 0) {
- val gen = currentGeneration + totalDelay
+ val gen = currentGeneration + totalDelay + (if (this.isInstanceOf[GeneralQuantification]) 2 else 0)
ignoredSubsts += this -> (ignoredSubsts.getOrElse(this, Set.empty) + ((gen, bs, subst)))
} else {
instantiation ++= instantiateSubst(bs, subst)
@@ -606,7 +606,7 @@ trait QuantificationTemplates { self: Templates =>
val baseSubst = subst ++ instanceSubst(enabler).mapValues(Left(_))
val (substMap, substClauses) = Template.substitution(
- condVars, exprVars, condTree, lambdas, quantifications, baseSubst, pathVar._1, enabler)
+ condVars, exprVars, condTree, lambdas, quantifications, baseSubst, enabler)
instantiation ++= substClauses
val msubst = substMap.collect { case (c, Right(m)) => c -> m }
@@ -617,17 +617,17 @@ trait QuantificationTemplates { self: Templates =>
instantiation ++= Template.instantiate(clauses, blockers, applications, Map.empty, substMap)
for ((b,ms) <- matchers; m <- ms) {
- val sb = bs ++ (if (b == start) Set.empty else Set(substituter(b)))
+ val sb = bs ++ (if (b == guard) Set.empty else Set(substituter(b)))
val sm = m.substitute(substituter, msubst)
def abs(i: Int): Int = if (i < 0) -i else i
- val nextGeneration: Int = currentGeneration +
- 2 * (abs(totalDepth(sm) - totalDepth(m)) + (if (b == start) 0 else 1))
+ val totalDelay = 2 * (abs(totalDepth(sm) - totalDepth(m)) + (if (b == guard) 0 else 1))
- if (nextGeneration == currentGeneration) {
- instantiation ++= instantiateMatcher(sb, sm)
+ if (totalDelay > 0) {
+ val gen = currentGeneration + totalDelay + (if (this.isInstanceOf[GeneralQuantification]) 2 else 0)
+ ignoredMatchers += ((gen, sb, sm))
} else {
- ignoredMatchers += ((nextGeneration, sb, sm))
+ instantiation ++= instantiateMatcher(sb, sm)
}
}
@@ -693,11 +693,11 @@ trait QuantificationTemplates { self: Templates =>
}
private class GeneralQuantification (
- val pathVar: (Variable, Encoded),
+ val blocker: Encoded,
val qs: (Variable, Encoded),
val q2s: (Variable, Encoded),
val insts: (Variable, Encoded),
- val guardVar: Encoded,
+ val guard: Encoded,
val quantifiers: Seq[(Variable, Encoded)],
val condVars: Map[Variable, Encoded],
val exprVars: Map[Variable, Encoded],
@@ -717,11 +717,10 @@ trait QuantificationTemplates { self: Templates =>
private var _insts: Map[Encoded, Set[Encoded]] = Map.empty
def instantiations = _insts
- private val blocker = Variable(FreshIdentifier("b_fresh", true), BooleanType)
protected def instanceSubst(enabler: Encoded): Map[Encoded, Encoded] = {
val nextQ2Var = encodeSymbol(q2s._1)
- val subst = Map(qs._2 -> currentQ2Var, guardVar -> enabler,
+ val subst = Map(qs._2 -> currentQ2Var, guard -> enabler,
q2s._2 -> nextQ2Var, insts._2 -> encodeSymbol(insts._1))
_currentQ2Var = nextQ2Var
@@ -736,8 +735,8 @@ trait QuantificationTemplates { self: Templates =>
}
private class Axiom (
- val pathVar: (Variable, Encoded),
- val guardVar: Encoded,
+ val blocker: Encoded,
+ val guard: Encoded,
val quantifiers: Seq[(Variable, Encoded)],
val condVars: Map[Variable, Encoded],
val exprVars: Map[Variable, Encoded],
@@ -753,7 +752,7 @@ trait QuantificationTemplates { self: Templates =>
val holds = trueT
protected def instanceSubst(enabler: Encoded): Map[Encoded, Encoded] = {
- Map(guardVar -> enabler)
+ Map(guard -> enabler)
}
}
@@ -820,8 +819,8 @@ trait QuantificationTemplates { self: Templates =>
case None =>
val clauses = new scala.collection.mutable.ListBuffer[Encoded]
val mapping: Map[Encoded, Encoded] = template.polarity match {
- case Positive(guardVar) =>
- val axiom = new Axiom(template.pathVar, guardVar,
+ case Positive(guard) =>
+ val axiom = new Axiom(template.pathVar._2, guard,
template.quantifiers, template.condVars, template.exprVars, template.condTree,
template.clauses, template.blockers, template.applications, template.matchers,
template.lambdas, template.quantifications, template.body)
@@ -841,7 +840,7 @@ trait QuantificationTemplates { self: Templates =>
val (substMap, substClauses) = Template.substitution(
template.condVars, template.exprVars, template.condTree,
template.lambdas, template.quantifications,
- Map(insts._2 -> Left(instT)), template.pathVar._1, template.pathVar._2)
+ Map(insts._2 -> Left(instT)), template.pathVar._2)
clauses ++= substClauses
// this will call `instantiateMatcher` on all matchers in `template.matchers`
@@ -851,12 +850,12 @@ trait QuantificationTemplates { self: Templates =>
Map(insts._2 -> instT)
- case Unknown(qs, q2s, insts, guardVar) =>
+ case Unknown(qs, q2s, insts, guard) =>
val qT = encodeSymbol(qs._1)
val substituter = mkSubstituter(Map(qs._2 -> qT))
- val quantification = new GeneralQuantification(template.pathVar,
- qs._1 -> qT, q2s, insts, guardVar,
+ val quantification = new GeneralQuantification(template.pathVar._2,
+ qs._1 -> qT, q2s, insts, guard,
template.quantifiers, template.condVars, template.exprVars, template.condTree,
template.clauses map substituter, // one clause depends on 'qs._2' (and therefore 'qT')
template.blockers, template.applications, template.matchers,
@@ -904,7 +903,7 @@ trait QuantificationTemplates { self: Templates =>
ignoredMatchers += ((gen - diff, bs, m))
}
- for (q <- quantifications) {
+ for (q <- quantifications if ignoredSubsts.isDefinedAt(q)) {
ignoredSubsts += q -> ignoredSubsts(q).map { case (gen, bs, subst) => (gen - diff, bs, subst) }
}
}
diff --git a/src/main/scala/inox/solvers/unrolling/Templates.scala b/src/main/scala/inox/solvers/unrolling/Templates.scala
index 5b7466c51db5d686298a8c45d86c742ca3a5b2d4..34406c5a6589c8df369f768c5b39bbc646ce1fa3 100644
--- a/src/main/scala/inox/solvers/unrolling/Templates.scala
+++ b/src/main/scala/inox/solvers/unrolling/Templates.scala
@@ -312,7 +312,7 @@ trait Templates extends TemplateGenerator
def instantiate(aVar: Encoded, args: Seq[Arg]): Clauses = {
val (substMap, clauses) = Template.substitution(
condVars, exprVars, condTree, lambdas, quantifications,
- (this.args zip args).toMap + (start -> Left(aVar)), pathVar._1, aVar)
+ (this.args zip args).toMap + (start -> Left(aVar)), aVar)
clauses ++ instantiate(substMap)
}
@@ -372,7 +372,8 @@ trait Templates extends TemplateGenerator
var applications : Map[Variable, Set[App]] = Map.empty
var matchers : Map[Variable, Set[Matcher]] = Map.empty
- for ((b,es) <- guardedExprs) {
+ val pv = pathVar._1
+ for ((b,es) <- guardedExprs + (pv -> (guardedExprs.getOrElse(pv, Set.empty) ++ equations))) {
var funInfos : Set[Call] = Set.empty
var appInfos : Set[App] = Set.empty
var matchInfos : Set[Matcher] = Set.empty
@@ -410,7 +411,6 @@ trait Templates extends TemplateGenerator
}
matchInfos ++= exprToMatcher.values
- clauses :+= encoder(Implies(b, e))
}
val calls = funInfos.filter(i => Some(i) != optIdCall)
@@ -426,6 +426,7 @@ trait Templates extends TemplateGenerator
if (matchs.nonEmpty) matchers += b -> matchs
}
+ clauses ++= (for ((b,es) <- guardedExprs; e <- es) yield encoder(Implies(b, e)))
clauses ++= equations.map(encoder)
(clauses, blockers, applications, matchers merge optIdMatcher.map(m => pathVar._1 -> Set(m)).toMap)
@@ -469,7 +470,6 @@ trait Templates extends TemplateGenerator
lambdas: Seq[LambdaTemplate],
quantifications: Seq[QuantificationTemplate],
baseSubst: Map[Encoded, Arg],
- pathVar: Variable,
aVar: Encoded
): (Map[Encoded, Arg], Clauses) = {
@@ -563,7 +563,7 @@ trait Templates extends TemplateGenerator
start -> encodedStart, bindings.toSeq, condVars, exprVars, guardedExprs, eqs, lambdas, quants)
val (substMap, substClauses) = Template.substitution(
- condVars, exprVars, condTree, lambdas, quants, Map.empty, start, encodedStart)
+ condVars, exprVars, condTree, lambdas, quants, Map.empty, encodedStart)
val templateClauses = Template.instantiate(clauses, calls, apps, matchers, substMap)
val allClauses = encodedStart +: (tpeClauses ++ substClauses ++ templateClauses)
diff --git a/src/main/scala/inox/utils/IncrementalMap.scala b/src/main/scala/inox/utils/IncrementalMap.scala
index c62104ae82e5a1b7462633c000d9fa7d093d6747..15cb2e6ab5aa03467ad6782a77d121f806fcbd53 100644
--- a/src/main/scala/inox/utils/IncrementalMap.scala
+++ b/src/main/scala/inox/utils/IncrementalMap.scala
@@ -20,6 +20,7 @@ class IncrementalMap[A, B] private(dflt: Option[B])
override def clear(): Unit = {
stack.clear()
+ push()
}
def reset(): Unit = {