From acbea642cab4efc1973a6d6c36f9c022220261a9 Mon Sep 17 00:00:00 2001
From: Nicolas Voirol <voirol.nicolas@gmail.com>
Date: Mon, 31 Oct 2016 10:12:43 +0100
Subject: [PATCH] Lots of fixes for quantifier instantiation module
---
.../solvers/unrolling/FunctionTemplates.scala | 6 +-
.../solvers/unrolling/LambdaTemplates.scala | 9 +-
.../unrolling/QuantificationTemplates.scala | 132 +++++++++++++-----
.../solvers/unrolling/TemplateGenerator.scala | 42 +++---
.../inox/solvers/unrolling/Templates.scala | 67 ++++++---
.../solvers/unrolling/UnrollingSolver.scala | 14 +-
6 files changed, 186 insertions(+), 84 deletions(-)
diff --git a/src/main/scala/inox/solvers/unrolling/FunctionTemplates.scala b/src/main/scala/inox/solvers/unrolling/FunctionTemplates.scala
index eada1e7e8..5c0b037c0 100644
--- a/src/main/scala/inox/solvers/unrolling/FunctionTemplates.scala
+++ b/src/main/scala/inox/solvers/unrolling/FunctionTemplates.scala
@@ -23,13 +23,14 @@ trait FunctionTemplates { self: Templates =>
exprVars: Map[Variable, Encoded],
condTree: Map[Variable, Set[Variable]],
guardedExprs: Map[Variable, Seq[Expr]],
+ equations: Seq[Expr],
lambdas: Seq[LambdaTemplate],
quantifications: Seq[QuantificationTemplate]
) : FunctionTemplate = {
val (clauses, blockers, applications, matchers, templateString) =
- Template.encode(pathVar, arguments, condVars, exprVars, guardedExprs, lambdas, quantifications,
- optCall = Some(tfd))
+ Template.encode(pathVar, arguments, condVars, exprVars, guardedExprs, equations,
+ lambdas, quantifications, optCall = Some(tfd))
val funString : () => String = () => {
"Template for def " + tfd.signature +
@@ -153,6 +154,7 @@ trait FunctionTemplates { self: Templates =>
// We connect it to the defBlocker: blocker => defBlocker
if (defBlocker != blocker) {
+ registerImplication(blocker, defBlocker)
newCls += mkImplies(blocker, defBlocker)
}
diff --git a/src/main/scala/inox/solvers/unrolling/LambdaTemplates.scala b/src/main/scala/inox/solvers/unrolling/LambdaTemplates.scala
index ff0573a58..0455d0fc8 100644
--- a/src/main/scala/inox/solvers/unrolling/LambdaTemplates.scala
+++ b/src/main/scala/inox/solvers/unrolling/LambdaTemplates.scala
@@ -58,6 +58,7 @@ trait LambdaTemplates { self: Templates =>
exprVars: Map[Variable, Encoded],
condTree: Map[Variable, Set[Variable]],
guardedExprs: Map[Variable, Seq[Expr]],
+ equations: Seq[Expr],
lambdas: Seq[LambdaTemplate],
quantifications: Seq[QuantificationTemplate],
structure: LambdaStructure,
@@ -68,8 +69,8 @@ trait LambdaTemplates { self: Templates =>
val id = ids._2
val tpe = ids._1.getType.asInstanceOf[FunctionType]
val (clauses, blockers, applications, matchers, templateString) =
- Template.encode(pathVar, arguments, condVars, exprVars, guardedExprs, lambdas, quantifications,
- substMap = baseSubstMap + ids, optApp = Some(id -> tpe))
+ Template.encode(pathVar, arguments, condVars, exprVars, guardedExprs, equations,
+ lambdas, quantifications, substMap = baseSubstMap + ids, optApp = Some(id -> tpe))
val lambdaString : () => String = () => {
"Template for lambda " + ids._1 + ": " + lambda + " is :\n" + templateString()
@@ -375,6 +376,7 @@ trait LambdaTemplates { self: Templates =>
Seq.empty
} else typeBlockers.get(encoded) match {
case Some(typeBlocker) =>
+ registerImplication(blocker, typeBlocker)
Seq(mkImplies(blocker, typeBlocker))
case None =>
@@ -393,7 +395,7 @@ trait LambdaTemplates { self: Templates =>
val extClause = mkEquals(firstB, mkAnd(blocker, mkNot(mkOr(boundClauses.toSeq :+ nextB : _*))))
- registerParent(typeBlocker, firstB)
+ registerImplication(firstB, typeBlocker)
val symClauses = registerSymbol(typeBlocker, encoded, to)
symClauses :+ extClause :+ mkImplies(firstB, typeBlocker)
@@ -520,6 +522,7 @@ trait LambdaTemplates { self: Templates =>
}
val enabler = if (equals == trueT) b else mkAnd(equals, b)
+ registerImplication(b, lambdaBlocker)
newCls += mkImplies(enabler, lambdaBlocker)
ctx.reporter.debug("Unrolling behind "+info+" ("+newCls.size+")")
diff --git a/src/main/scala/inox/solvers/unrolling/QuantificationTemplates.scala b/src/main/scala/inox/solvers/unrolling/QuantificationTemplates.scala
index a6cc13624..5c1d651e8 100644
--- a/src/main/scala/inox/solvers/unrolling/QuantificationTemplates.scala
+++ b/src/main/scala/inox/solvers/unrolling/QuantificationTemplates.scala
@@ -76,11 +76,19 @@ trait QuantificationTemplates { self: Templates =>
case class Positive(guardVar: Encoded) extends Polarity
case class Negative(insts: (Variable, Encoded)) extends Polarity
- case class Unknown(
- qs: (Variable, Encoded),
- q2s: (Variable, Encoded),
- insts: (Variable, Encoded),
- guardVar: Encoded) extends Polarity
+
+ /** Unknown quantification polarity.
+ *
+ * Instantiations of unknown polarity quantification with body {{{p}}} follows the schema:
+ * {{{
+ * b ==> (q == (q2 && inst)
+ * b ==> (inst == (guard ==> p))
+ * }}}
+ * It is useful to keep the two clauses separate so that satisfying assignments can be
+ * 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
class QuantificationTemplate private[QuantificationTemplates] (
val pathVar: (Variable, Encoded),
@@ -138,52 +146,62 @@ trait QuantificationTemplates { self: Templates =>
exprVars: Map[Variable, Encoded],
condTree: Map[Variable, Set[Variable]],
guardedExprs: Map[Variable, Seq[Expr]],
+ equations: Seq[Expr],
lambdas: Seq[LambdaTemplate],
quantifications: Seq[QuantificationTemplate],
- baseSubstMap: Map[Variable, Encoded],
+ substMap: Map[Variable, Encoded],
proposition: Forall
): (Option[Variable], QuantificationTemplate) = {
- val (optVar, polarity, extraGuarded, extraSubst) = optPol match {
+ val pT = mkEncoder(
+ condVars ++ exprVars + pathVar ++ quantifiers ++
+ substMap ++ lambdas.map(_.ids) ++ quantifications.flatMap(_.mapping)
+ )(p)
+
+ val (optVar, polarity, extraClauses, extraSubst) = optPol match {
case Some(true) =>
- val guard: Variable = Variable(FreshIdentifier("guard", true), BooleanType)
- val guards = guard -> encodeSymbol(guard)
- (None, Positive(guards._2), Map(pathVar._1 -> Seq(Implies(guard, p))), Map(guards))
+ 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))
case Some(false) =>
val inst: Variable = Variable(FreshIdentifier("inst", true), BooleanType)
val insts = inst -> encodeSymbol(inst)
- (Some(inst), Negative(insts), Map(pathVar._1 -> Seq(Equals(inst, p))), Map(insts))
+ val extraClause = mkImplies(pathVar._2, mkEquals(insts._2, pT))
+ (Some(inst), Negative(insts), Seq(extraClause), Map.empty)
case None =>
val q: Variable = Variable(FreshIdentifier("q", true), BooleanType)
val q2: Variable = Variable(FreshIdentifier("qo", true), BooleanType)
val inst: Variable = Variable(FreshIdentifier("inst", true), BooleanType)
- val guard: Variable = Variable(FreshIdentifier("guard", true), BooleanType)
+ val guard = encodeSymbol(Variable(FreshIdentifier("guard", true), BooleanType))
val qs = q -> encodeSymbol(q)
val q2s = q2 -> encodeSymbol(q2)
val insts = inst -> encodeSymbol(inst)
- val guards = guard -> encodeSymbol(guard)
- val polarity = Unknown(qs, q2s, insts, guards._2)
- val extraGuarded = Map(pathVar._1 -> Seq(Equals(inst, Implies(guard, p)), Equals(q, And(q2, inst))))
- val extraSubst = Map(qs, q2s, insts, guards)
- (Some(q), polarity, extraGuarded, extraSubst)
+ 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 substMap = baseSubstMap ++ extraSubst
- val allGuarded = guardedExprs merge extraGuarded
-
+ // Note @nv: some hacky shit is going on here...
+ // We are overriding the mapping of `pathVar._1` for certain polarities so that
+ // the encoded clauses use the `guard` as blocker instead of `pathVar._2`. This only
+ // 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, allGuarded,
- lambdas, quantifications, substMap = substMap)
+ Template.encode(pathVar, quantifiers, condVars, exprVars, guardedExprs,
+ equations, lambdas, quantifications, substMap = substMap ++ extraSubst)
val key = templateKey(proposition.args, proposition.body, substMap)
(optVar, new QuantificationTemplate(
pathVar, polarity, quantifiers, condVars, exprVars, condTree,
- clauses, blockers, applications, matchers, lambdas, quantifications, key,
+ extraClauses ++ clauses, blockers, applications, matchers, lambdas, quantifications, key,
proposition.body, () => "Template for " + proposition + " is :\n" + templateString()))
}
}
@@ -203,8 +221,8 @@ trait QuantificationTemplates { self: Templates =>
val lambdaAxioms = new IncrementalSet[(LambdaStructure, Seq[(Variable, Encoded)])]
val templates = new IncrementalMap[(Seq[ValDef], Expr, Seq[Encoded]), Map[Encoded, Encoded]]
- val incrementals: Seq[IncrementalState] = Seq(
- quantifications, ignoredMatchers, handledMatchers, ignoredSubsts, handledSubsts, lambdaAxioms, templates)
+ val incrementals: Seq[IncrementalState] = Seq(quantifications, lambdaAxioms, templates,
+ ignoredMatchers, handledMatchers, ignoredSubsts, handledSubsts, ignoredGrounds)
override def push(): Unit = { super.push(); for (q <- quantifications) q.push() }
override def pop(): Unit = { super.pop(); for (q <- quantifications) q.pop() }
@@ -228,24 +246,35 @@ trait QuantificationTemplates { self: Templates =>
def promoteBlocker(b: Encoded): Boolean = false
def unroll: Clauses = {
- val clauses = new scala.collection.mutable.ListBuffer[Encoded]
-
+ val imClauses = new scala.collection.mutable.ListBuffer[Encoded]
for (e @ (gen, bs, m) <- ignoredMatchers.toSeq if gen <= currentGeneration) {
- clauses ++= instantiateMatcher(bs, m)
+ imClauses ++= instantiateMatcher(bs, m)
ignoredMatchers -= e
}
+ ctx.reporter.debug("Unrolling ignored matchers (" + imClauses.size + ")")
+ for (cl <- imClauses) {
+ ctx.reporter.debug(" . " + cl)
+ }
+
+ val suClauses = new scala.collection.mutable.ListBuffer[Encoded]
for (q <- quantifications.toSeq if ignoredSubsts.isDefinedAt(q)) {
val (release, keep) = ignoredSubsts(q).partition(_._1 <= currentGeneration)
ignoredSubsts += q -> keep
for ((_, bs, subst) <- release) {
- clauses ++= q.instantiateSubst(bs, subst)
+ suClauses ++= q.instantiateSubst(bs, subst)
}
}
+ ctx.reporter.debug("Unrolling ignored substitutions (" + suClauses.size + ")")
+ for (cl <- suClauses) {
+ ctx.reporter.debug(" . " + cl)
+ }
+
+ val grClauses = new scala.collection.mutable.ListBuffer[Encoded]
for ((gen, qs) <- ignoredGrounds.toSeq if gen <= currentGeneration; q <- qs) {
- clauses ++= q.ensureGrounds
+ grClauses ++= q.ensureGrounds
val remaining = ignoredGrounds.getOrElse(gen, Set.empty) - q
if (remaining.nonEmpty) {
ignoredGrounds += gen -> remaining
@@ -254,20 +283,28 @@ trait QuantificationTemplates { self: Templates =>
}
}
- clauses.toSeq
+ ctx.reporter.debug("Unrolling ignored grounds (" + grClauses.size + ")")
+ for (cl <- grClauses) {
+ ctx.reporter.debug(" . " + cl)
+ }
+
+ imClauses.toSeq ++ suClauses ++ grClauses
}
}
- def instantiateMatcher(blocker: Encoded, matcher: Matcher): Clauses =
+ def instantiateMatcher(blocker: Encoded, matcher: Matcher): Clauses = {
instantiateMatcher(Set(blocker), matcher)
+ }
@inline
private def instantiateMatcher(blockers: Set[Encoded], matcher: Matcher): Clauses = {
- if (handledMatchers(blockers -> matcher)) {
+ val relevantBlockers = blockerPath(blockers)
+
+ if (handledMatchers(relevantBlockers -> matcher)) {
Seq.empty
} else {
- handledMatchers += blockers -> matcher
- quantifications.flatMap(_.instantiate(blockers, matcher))
+ handledMatchers += relevantBlockers -> matcher
+ quantifications.flatMap(_.instantiate(relevantBlockers, matcher))
}
}
@@ -447,6 +484,7 @@ trait QuantificationTemplates { self: Templates =>
lazy val quantified: Set[Encoded] = quantifiers.map(_._2).toSet
lazy val start = pathVar._2
+ lazy val pathBlockers = blockerPath(start)
private val constraints: Seq[(Encoded, MatcherKey, Int)] = (for {
(_, ms) <- matchers
@@ -509,6 +547,8 @@ trait QuantificationTemplates { self: Templates =>
instantiateSubsts(mappings)
}
+ def hasAllGrounds: Boolean = quantified.forall(q => grounds(q).nonEmpty)
+
def ensureGrounds: Clauses = {
/* Build mappings from quantifiers to all potential ground values previously encountered
* AND the constants we're introducing to make sure grounds are non-empty. */
@@ -561,7 +601,7 @@ trait QuantificationTemplates { self: Templates =>
handledSubsts += this -> (handledSubsts.getOrElse(this, Set.empty) + (bs -> subst))
val instantiation = new scala.collection.mutable.ListBuffer[Encoded]
- val (enabler, enablerClauses) = encodeBlockers(bs)
+ val (enabler, enablerClauses) = encodeBlockers(bs ++ pathBlockers)
instantiation ++= enablerClauses
val baseSubst = subst ++ instanceSubst(enabler).mapValues(Left(_))
@@ -828,8 +868,12 @@ trait QuantificationTemplates { self: Templates =>
clauses ++= quantification.instantiate(bs, m)
}
+ val freshSubst = mkSubstituter(template.quantifiers.map(p => p._2 -> encodeSymbol(p._1)).toMap)
for ((b,ms) <- template.matchers; m <- ms) {
- clauses ++= instantiateMatcher(b, m)
+ clauses ++= instantiateMatcher(Set.empty[Encoded], m)
+ // 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
@@ -847,6 +891,13 @@ trait QuantificationTemplates { self: Templates =>
throw FatalError("Attempting to promote inexistent quantifiers")
val diff = (currentGeneration - optGen.get) max 0
+
+ val currentGrounds = ignoredGrounds.toSeq
+ ignoredGrounds.clear()
+ for ((gen, qs) <- currentGrounds) {
+ ignoredGrounds += (gen - diff) -> qs
+ }
+
val currentMatchers = ignoredMatchers.toSeq
ignoredMatchers.clear()
for ((gen, bs, m) <- currentMatchers) {
@@ -865,6 +916,13 @@ trait QuantificationTemplates { self: Templates =>
val clauses = new scala.collection.mutable.ListBuffer[Encoded]
val keyClause = MutableMap.empty[MatcherKey, (Clauses, Encoded)]
+ val currentGrounds = ignoredGrounds.toSeq
+ for ((gen, qs) <- currentGrounds if qs.exists(!_.hasAllGrounds)) {
+ ignoredGrounds -= gen
+ ignoredGrounds += currentGeneration -> qs
+ clauses += falseT
+ }
+
for ((_, bs, m) <- ignoredMatchers) {
val key = matcherKey(m)
val argTypes = key match {
diff --git a/src/main/scala/inox/solvers/unrolling/TemplateGenerator.scala b/src/main/scala/inox/solvers/unrolling/TemplateGenerator.scala
index 83acb6e04..9d4f63a07 100644
--- a/src/main/scala/inox/solvers/unrolling/TemplateGenerator.scala
+++ b/src/main/scala/inox/solvers/unrolling/TemplateGenerator.scala
@@ -17,19 +17,22 @@ trait TemplateGenerator { self: Templates =>
Map[Variable, Encoded],
Map[Variable, Set[Variable]],
Map[Variable, Seq[Expr]],
+ Seq[Expr],
Seq[LambdaTemplate],
Seq[QuantificationTemplate]
)
- private def emptyClauses: TemplateClauses = (Map.empty, Map.empty, Map.empty, Map.empty, Seq.empty, Seq.empty)
+ private def emptyClauses: TemplateClauses =
+ (Map.empty, Map.empty, Map.empty, Map.empty, Seq.empty, Seq.empty, Seq.empty)
private implicit class ClausesWrapper(clauses: TemplateClauses) {
def ++(that: TemplateClauses): TemplateClauses = {
- val (thisConds, thisExprs, thisTree, thisGuarded, thisLambdas, thisQuants) = clauses
- val (thatConds, thatExprs, thatTree, thatGuarded, thatLambdas, thatQuants) = that
+ val (thisConds, thisExprs, thisTree, thisGuarded, thisEqs, thisLambdas, thisQuants) = clauses
+ val (thatConds, thatExprs, thatTree, thatGuarded, thatEqs, thatLambdas, thatQuants) = that
- (thisConds ++ thatConds, thisExprs ++ thatExprs, thisTree merge thatTree,
- thisGuarded merge thatGuarded, thisLambdas ++ thatLambdas, thisQuants ++ thatQuants)
+ (thisConds ++ thatConds, thisExprs ++ thatExprs,
+ thisTree merge thatTree, thisGuarded merge thatGuarded,
+ thisEqs ++ thatEqs, thisLambdas ++ thatLambdas, thisQuants ++ thatQuants)
}
}
@@ -57,11 +60,11 @@ trait TemplateGenerator { self: Templates =>
val substMap : Map[Variable, Encoded] = arguments.toMap + pathVar
- val (condVars, exprVars, condTree, guardedExprs, lambdas, quantifications) =
+ val (condVars, exprVars, condTree, guardedExprs, eqs, lambdas, quantifications) =
invocationEqualsBody.foldLeft(emptyClauses)((clsSet, cls) => clsSet ++ mkClauses(start, cls, substMap))
val template = FunctionTemplate(tfd, pathVar, arguments,
- condVars, exprVars, condTree, guardedExprs, lambdas, quantifications)
+ condVars, exprVars, condTree, guardedExprs, eqs, lambdas, quantifications)
cache += tfd -> template
template
}
@@ -88,12 +91,13 @@ trait TemplateGenerator { self: Templates =>
}
def mkClauses(pathVar: Variable, expr: Expr, substMap: Map[Variable, Encoded], polarity: Option[Boolean] = None): TemplateClauses = {
- val (p, (condVars, exprVars, condTree, guardedExprs, lambdas, quantifications)) = mkExprClauses(pathVar, expr, substMap, polarity)
+ val (p, (condVars, exprVars, condTree, guardedExprs, eqs, lambdas, quantifications)) = mkExprClauses(pathVar, expr, substMap, polarity)
val allGuarded = guardedExprs + (pathVar -> (p +: guardedExprs.getOrElse(pathVar, Seq.empty)))
- (condVars, exprVars, condTree, allGuarded, lambdas, quantifications)
+ (condVars, exprVars, condTree, allGuarded, eqs, lambdas, quantifications)
}
private def mkExprClauses(pathVar: Variable, expr: Expr, substMap: Map[Variable, Encoded], polarity: Option[Boolean] = None): (Expr, TemplateClauses) = {
+ val initVar = pathVar
var condVars = Map[Variable, Encoded]()
var condTree = Map[Variable, Set[Variable]](pathVar -> Set.empty).withDefaultValue(Set.empty)
@@ -117,7 +121,9 @@ trait TemplateGenerator { self: Templates =>
guardedExprs += guardVar -> (expr +: prev)
}
- @inline def iff(e1: Expr, e2: Expr): Unit = storeGuarded(pathVar, Equals(e1, e2))
+ // Represents equations (simple formulas)
+ var eqs = Seq[Expr]()
+ @inline def iff(e1: Expr, e2: Expr): Unit = eqs :+= Equals(e1, e2)
var lambdaVars = Map[Variable, Encoded]()
@inline def storeLambda(id: Variable): Encoded = {
@@ -275,7 +281,7 @@ trait TemplateGenerator { self: Templates =>
val localSubst: Map[Variable, Encoded] = substMap ++ condVars ++ exprVars ++ lambdaVars
val clauseSubst: Map[Variable, Encoded] = localSubst ++ (idArgs zip trArgs)
- val (lambdaConds, lambdaExprs, lambdaTree, lambdaGuarded, lambdaTemplates, lambdaQuants) =
+ 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)
@@ -283,12 +289,12 @@ trait TemplateGenerator { self: Templates =>
val (struct, deps) = normalizeStructure(l)
val sortedDeps = deps.toSeq.sortBy(_._1.id.uniqueName)
- val (dependencies, (depConds, depExprs, depTree, depGuarded, depLambdas, depQuants)) =
+ val (dependencies, (depConds, depExprs, depTree, depGuarded, depEqs, depLambdas, depQuants)) =
sortedDeps.foldLeft[(Seq[Encoded], TemplateClauses)](Seq.empty -> emptyClauses) {
case ((dependencies, clsSet), (id, expr)) =>
if (!exprOps.isSimple(expr)) {
val encoded = encodeSymbol(id)
- val (e, cls @ (_, _, _, _, lmbds, quants)) = mkExprClauses(pathVar, expr, localSubst)
+ val (e, cls @ (_, _, _, _, _, lmbds, quants)) = mkExprClauses(pathVar, expr, localSubst)
val clauseSubst = localSubst ++ lmbds.map(_.ids) ++ quants.flatMap(_.mapping)
(dependencies :+ mkEncoder(clauseSubst)(e), clsSet ++ cls)
} else {
@@ -298,7 +304,7 @@ trait TemplateGenerator { self: Templates =>
val (depClauses, depCalls, depApps, depMatchers, _) = Template.encode(
pathVar -> encodedCond(pathVar), Seq.empty,
- depConds, depExprs, depGuarded, depLambdas, depQuants, localSubst)
+ depConds, depExprs, depGuarded, depEqs, depLambdas, depQuants, localSubst)
val depClosures: Seq[Encoded] = {
val vars = exprOps.variablesOf(l)
@@ -313,7 +319,7 @@ trait TemplateGenerator { self: Templates =>
val template = LambdaTemplate(ids, pathVar -> encodedCond(pathVar),
idArgs zip trArgs, lambdaConds, lambdaExprs, lambdaTree,
- lambdaGuarded, lambdaTemplates, lambdaQuants, structure, localSubst, l)
+ lambdaGuarded, lambdaEqs, lambdaTemplates, lambdaQuants, structure, localSubst, l)
registerLambda(template)
lid
@@ -329,10 +335,10 @@ trait TemplateGenerator { self: Templates =>
val localSubst: Map[Variable, Encoded] = substMap ++ condVars ++ exprVars ++ lambdaVars
val clauseSubst: Map[Variable, Encoded] = localSubst ++ (idQuantifiers zip trQuantifiers)
- val (p, (qConds, qExprs, qTree, qGuarded, qLambdas, qQuants)) = mkExprClauses(pathVar, conjunct, clauseSubst)
+ val (p, (qConds, qExprs, qTree, qGuarded, qEqs, qLambdas, qQuants)) = mkExprClauses(pathVar, conjunct, clauseSubst)
val (optVar, template) = QuantificationTemplate(pathVar -> encodedCond(pathVar),
- pol, p, idQuantifiers zip trQuantifiers, qConds, qExprs, qTree, qGuarded, qLambdas, qQuants,
+ pol, p, idQuantifiers zip trQuantifiers, qConds, qExprs, qTree, qGuarded, qEqs, qLambdas, qQuants,
localSubst, Forall(quantifiers.toSeq.sortBy(_.id.uniqueName).map(_.toVal), conjunct))
registerQuantification(template)
optVar.getOrElse(BooleanLiteral(true))
@@ -344,7 +350,7 @@ trait TemplateGenerator { self: Templates =>
}
val p = rec(pathVar, expr, polarity)
- (p, (condVars, exprVars, condTree, guardedExprs, lambdas, quantifications))
+ (p, (condVars, exprVars, condTree, guardedExprs, eqs, lambdas, quantifications))
}
}
diff --git a/src/main/scala/inox/solvers/unrolling/Templates.scala b/src/main/scala/inox/solvers/unrolling/Templates.scala
index bdd3a9b97..5b7466c51 100644
--- a/src/main/scala/inox/solvers/unrolling/Templates.scala
+++ b/src/main/scala/inox/solvers/unrolling/Templates.scala
@@ -35,10 +35,11 @@ trait Templates extends TemplateGenerator
def mkImplies(l: Encoded, r: Encoded): Encoded
private[unrolling] lazy val trueT = mkEncoder(Map.empty)(BooleanLiteral(true))
+ private[unrolling] lazy val falseT = mkEncoder(Map.empty)(BooleanLiteral(false))
private var currentGen: Int = 0
protected def currentGeneration: Int = currentGen
- protected def nextGeneration(gen: Int): Int = gen + 5
+ protected def nextGeneration(gen: Int): Int = gen + 3
trait Manager extends IncrementalStateWrapper {
def unrollGeneration: Option[Int]
@@ -59,22 +60,29 @@ trait Templates extends TemplateGenerator
def canUnroll: Boolean = managers.exists(_.unrollGeneration.isDefined)
def unroll: Clauses = {
assert(canUnroll, "Impossible to unroll further")
- val generation = managers.flatMap(_.unrollGeneration).min + 1
- if (generation > currentGen) {
- currentGen = generation
- }
-
+ currentGen = managers.flatMap(_.unrollGeneration).min + 1
+ ctx.reporter.debug("Unrolling generation [" + currentGen + "]")
managers.flatMap(_.unroll)
}
def satisfactionAssumptions = managers.flatMap(_.satisfactionAssumptions)
def refutationAssumptions = managers.flatMap(_.refutationAssumptions)
+ // implication tree that we're sure about: if (b1, b2) is in the tree, then
+ // we have the precise semantics of b1 ==> b2 in the resulting clause set
private val condImplies = new IncrementalMap[Encoded, Set[Encoded]].withDefaultValue(Set.empty)
private val condImplied = new IncrementalMap[Encoded, Set[Encoded]].withDefaultValue(Set.empty)
+
+ // implication tree that isn't quite ensured in the resulting clause set
+ // this can happen due to defBlocker caching in unrolling
+ private val potImplies = new IncrementalMap[Encoded, Set[Encoded]].withDefaultValue(Set.empty)
+ private val potImplied = new IncrementalMap[Encoded, Set[Encoded]].withDefaultValue(Set.empty)
+
private val condEquals = new IncrementalBijection[Encoded, Set[Encoded]]
- val incrementals: Seq[IncrementalState] = managers ++ Seq(condImplies, condImplied, condEquals)
+ val incrementals: Seq[IncrementalState] = managers ++ Seq(
+ condImplies, condImplied, potImplies, potImplied, condEquals
+ )
protected def freshConds(
pathVar: Encoded,
@@ -89,7 +97,8 @@ trait Templates extends TemplateGenerator
case None => // enabling condition, corresponds to pathVar
for (child <- children) {
val ec = mapping(child)
- condImplied += ec -> (condImplies(ec) + pathVar)
+ condImplies += pathVar -> (condImplies(pathVar) + ec)
+ condImplied += ec -> (condImplied(ec) + pathVar)
}
case Some(ep) =>
@@ -106,8 +115,11 @@ trait Templates extends TemplateGenerator
private val sym = Variable(FreshIdentifier("bs", true), BooleanType)
protected def encodeBlockers(bs: Set[Encoded]): (Encoded, Clauses) = bs.toSeq match {
- case Seq(b) if condImplies.isDefinedAt(b) || condImplied.isDefinedAt(b) || condEquals.containsA(b) =>
- (b, Seq.empty)
+ case Seq(b) if (
+ condImplies.isDefinedAt(b) || condImplied.isDefinedAt(b) ||
+ potImplies.isDefinedAt(b) || potImplied.isDefinedAt(b) ||
+ condEquals.containsA(b)
+ ) => (b, Seq.empty)
case _ =>
val flatBs = fixpoint((bs: Set[Encoded]) => bs.flatMap(b => condEquals.getBorElse(b, Set(b))))(bs)
@@ -120,12 +132,30 @@ trait Templates extends TemplateGenerator
}
}
- protected def registerParent(child: Encoded, parent: Encoded): Unit = {
- condImplied += child -> (condImplied(child) + parent)
+ protected def registerImplication(b1: Encoded, b2: Encoded): Unit = {
+ potImplies += b1 -> (potImplies(b1) + b2)
+ potImplied += b2 -> (potImplied(b2) + b1)
+ }
+
+ protected def blockerEquals(b: Encoded): Set[Encoded] = condEquals.getBorElse(b, Set.empty)
+
+ protected def blockerParents(b: Encoded, strict: Boolean = true): Set[Encoded] = {
+ condImplied(b) ++ (if (!strict) potImplied(b) else Set.empty)
+ }
+
+ protected def blockerChildren(b: Encoded, strict: Boolean = true): Set[Encoded] = {
+ condImplies(b) ++ (if (!strict) potImplies(b) else Set.empty)
}
- protected def blockerParents(b: Encoded): Set[Encoded] = condImplied(b)
- protected def blockerChildren(b: Encoded): Set[Encoded] = condImplies(b)
+ protected def blockerPath(b: Encoded): Set[Encoded] = blockerPath(Set(b))
+
+ /* This set is guaranteed finite and won't expand beyond the limit of a function's
+ * definition as aVar ==> defBlocker is NOT a strict implication (ie. won't be in
+ * the condImplied map) */
+ protected def blockerPath(bs: Set[Encoded]): Set[Encoded] = fixpoint((bs: Set[Encoded]) => bs.flatMap { b =>
+ val equal = condEquals.getBorElse(b, Set.empty)
+ if (equal.nonEmpty) equal else (condImplied(b) + b)
+ })(bs)
def promoteBlocker(b: Encoded, force: Boolean = false): Boolean = {
var seen: Set[Encoded] = Set.empty
@@ -145,7 +175,7 @@ trait Templates extends TemplateGenerator
}
if (force) {
- blockerChildren(b)
+ blockerChildren(b, strict = false)
} else {
Seq.empty[Encoded]
}
@@ -309,6 +339,7 @@ trait Templates extends TemplateGenerator
condVars: Map[Variable, Encoded],
exprVars: Map[Variable, Encoded],
guardedExprs: Map[Variable, Seq[Expr]],
+ equations: Seq[Expr],
lambdas: Seq[LambdaTemplate],
quantifications: Seq[QuantificationTemplate],
substMap: Map[Variable, Encoded] = Map.empty[Variable, Encoded],
@@ -395,6 +426,8 @@ trait Templates extends TemplateGenerator
if (matchs.nonEmpty) matchers += b -> matchs
}
+ clauses ++= equations.map(encoder)
+
(clauses, blockers, applications, matchers merge optIdMatcher.map(m => pathVar._1 -> Set(m)).toMap)
}
@@ -523,11 +556,11 @@ trait Templates extends TemplateGenerator
val tpeClauses = bindings.flatMap { case (v, s) => registerSymbol(encodedStart, s, v.getType) }.toSeq
val instExpr = simplifyHOFunctions(simplifyQuantifications(expr))
- val (condVars, exprVars, condTree, guardedExprs, lambdas, quants) =
+ val (condVars, exprVars, condTree, guardedExprs, eqs, lambdas, quants) =
mkClauses(start, instExpr, bindings + (start -> encodedStart), polarity = Some(true))
val (clauses, calls, apps, matchers, _) = Template.encode(
- start -> encodedStart, bindings.toSeq, condVars, exprVars, guardedExprs, lambdas, quants)
+ start -> encodedStart, bindings.toSeq, condVars, exprVars, guardedExprs, eqs, lambdas, quants)
val (substMap, substClauses) = Template.substitution(
condVars, exprVars, condTree, lambdas, quants, Map.empty, start, encodedStart)
diff --git a/src/main/scala/inox/solvers/unrolling/UnrollingSolver.scala b/src/main/scala/inox/solvers/unrolling/UnrollingSolver.scala
index e49d71bac..28081283e 100644
--- a/src/main/scala/inox/solvers/unrolling/UnrollingSolver.scala
+++ b/src/main/scala/inox/solvers/unrolling/UnrollingSolver.scala
@@ -544,8 +544,11 @@ trait AbstractUnrollingSolver extends Solver { self =>
}
val timer = ctx.timers.solvers.check.start()
+
+ // we always ask for a model here in order to give priority to blockers that
+ // are keeping quantified clause instantiations from being considered
val res: SolverResponse[underlying.Model, Set[underlying.Trees]] =
- underlying.checkAssumptions(config max Configuration(model = feelingLucky))(
+ underlying.checkAssumptions(config max Configuration(model = true))(
encodedAssumptions.toSet ++ templates.refutationAssumptions
)
timer.stop()
@@ -559,8 +562,8 @@ trait AbstractUnrollingSolver extends Solver { self =>
case _: Unsatisfiable =>
CheckResult.cast(res)
- case SatWithModel(model) if feelingLucky =>
- if (validateModel(extractSimpleModel(model), assumptionsSeq, silenceErrors = true)) {
+ case SatWithModel(model) =>
+ if (feelingLucky && validateModel(extractSimpleModel(model), assumptionsSeq, silenceErrors = true)) {
CheckResult.cast(res)
} else {
val wrapped = wrapModel(model)
@@ -572,9 +575,6 @@ trait AbstractUnrollingSolver extends Solver { self =>
Unroll
}
-
- case _ =>
- Unroll
}
case Unroll =>
@@ -582,7 +582,7 @@ trait AbstractUnrollingSolver extends Solver { self =>
val timer = ctx.timers.solvers.unroll.start()
// unfolling `unrollFactor` times
- for (i <- 1 to unrollFactor.toInt) {
+ for (i <- 1 to unrollFactor.toInt if templates.canUnroll) {
val newClauses = templates.unroll
for (ncl <- newClauses) {
underlying.assertCnstr(ncl)
--
GitLab