There are compelling use cases that combine strings/sequences and quantifiers. Prior to this PR, strings enabled "bounded integer" quantifier instantiation so that internally generated quantifiers for strings reductions are handled in a complete manner. However, this enabled bounded integer quantifier instantiation globally. This degrades performance for "unsat" on quantified formulas in general.
After this PR, we do not enable bounded integer quantifier globally. Instead, we ensure that bounded integer quantification is applied to at least the internally generated quantified formulas; all other quantified formulas are handled as usual.
Notice this required ensuring that all quantified formulas generated by strings are marked properly. It also required adding --fmf-bound to a few regressions that explicitly require it.
Trace("smt") << "turning on quantifier logic, for strings-exp"
<< std::endl;
}
- // We require bounded quantifier handling.
- if (!opts.quantifiers.fmfBoundWasSetByUser)
- {
- opts.quantifiers.fmfBound = true;
- Trace("smt") << "turning on fmf-bound, for strings-exp" << std::endl;
- }
// Note we allow E-matching by default to support combinations of sequences
- // and quantifiers.
+ // and quantifiers. We also do not enable fmfBound here, which would
+ // enable bounded integer instantiation for *all* quantifiers. Instead,
+ // the bounded integers module will always process internally generated
+ // quantifiers (those marked with InternalQuantAttribute).
}
// whether we must disable proofs
bool disableProofs = false;
{
//this needs to be done at preregister since it affects e.g. QuantDSplit's preregister
Trace("bound-int") << "check ownership quantifier " << f << std::endl;
+
+ // determine if we should look at the quantified formula at all
+ if (!options::fmfBound())
+ {
+ // only applying it to internal quantifiers
+ QuantAttributes& qattr = d_qreg.getQuantAttributes();
+ if (!qattr.isInternal(f))
+ {
+ Trace("bound-int") << "...not internal, skip" << std::endl;
+ return;
+ }
+ }
+
NodeManager* nm = NodeManager::currentNM();
SkolemManager* sm = nm->getSkolemManager();
#include "theory/quantifiers/quantifiers_modules.h"
#include "options/quantifiers_options.h"
+#include "options/strings_options.h"
#include "theory/quantifiers/relevant_domain.h"
#include "theory/quantifiers/term_registry.h"
d_synth_e.reset(new SynthEngine(qs, qim, qr, tr));
modules.push_back(d_synth_e.get());
}
- // finite model finding
- if (options::fmfBound())
+ // bounded integer instantiation is used when the user requests it via
+ // fmfBound, or if strings are enabled.
+ if (options::fmfBound() || options::stringExp())
{
d_bint.reset(new BoundedIntegers(qs, qim, qr, tr));
modules.push_back(d_bint.get());
}
- if (options::finiteModelFind() || options::fmfBound())
+ if (options::finiteModelFind() || options::fmfBound() || options::stringExp())
{
d_model_engine.reset(new ModelEngine(qs, qim, qr, tr, builder));
modules.push_back(d_model_engine.get());
children2.push_back(res);
Node body = nm->mkNode(AND, children2);
Node bvl = nm->mkNode(BOUND_VAR_LIST, non_greedy_find_vars);
- res = nm->mkNode(EXISTS, bvl, body);
+ res = utils::mkForallInternal(bvl, body.negate()).negate();
}
// must also give a minimum length requirement
res = nm->mkNode(AND, res, nm->mkNode(GEQ, lenx, lenSum));
if (k.getKind() == BOUND_VARIABLE)
{
Node bvl = nm->mkNode(BOUND_VAR_LIST, k);
- body = nm->mkNode(EXISTS, bvl, body);
+ body = utils::mkForallInternal(bvl, body.negate()).negate();
}
// e.g. x in re.++( R1, "AB", R2 ) --->
// exists k.
: nm->mkNode(OR, char_constraints);
Node body = nm->mkNode(OR, bound.negate(), conc);
Node bvl = nm->mkNode(BOUND_VAR_LIST, index);
- Node res = nm->mkNode(FORALL, bvl, body);
+ Node res = utils::mkForallInternal(bvl, body);
// e.g.
// x in (re.* (re.union "A" "B" )) --->
// forall k. 0<=k<len(x) => (substr(x,k,1) in "A" OR substr(x,k,1) in "B")
.eqNode(s);
Node body = nm->mkNode(OR, bound.negate(), conc);
Node bvl = nm->mkNode(BOUND_VAR_LIST, index);
- Node res = nm->mkNode(FORALL, bvl, body);
+ Node res = utils::mkForallInternal(bvl, body);
res = nm->mkNode(
AND, nm->mkNode(INTS_MODULUS_TOTAL, lenx, lens).eqNode(zero), res);
// e.g.
conc = nm->mkNode(OR, s1r1, s2r2);
conc = nm->mkNode(IMPLIES, g1, conc);
- conc = nm->mkNode(FORALL, b1v, conc);
+ // must mark as an internal quantifier
+ conc = utils::mkForallInternal(b1v, conc);
conc = nm->mkNode(AND, sne, conc);
}
else
if (!b1v.isNull())
{
conc = nm->mkNode(OR, guard.negate(), conc);
- conc = nm->mkNode(FORALL, b1v, conc);
+ // must mark as an internal quantifier
+ conc = utils::mkForallInternal(b1v, conc);
}
return conc;
}
#include "options/smt_options.h"
#include "options/strings_options.h"
#include "smt/logic_exception.h"
-#include "theory/quantifiers/quantifiers_attributes.h"
#include "theory/strings/arith_entail.h"
#include "theory/strings/sequences_rewriter.h"
+#include "theory/strings/theory_strings_utils.h"
#include "theory/strings/word.h"
#include "util/rational.h"
#include "util/statistics_registry.h"
namespace theory {
namespace strings {
-/** Mapping to a dummy node for marking an attribute on internal quantified
- * formulas */
-struct QInternalVarAttributeId
-{
-};
-typedef expr::Attribute<QInternalVarAttributeId, Node> QInternalVarAttribute;
-
StringsPreprocess::StringsPreprocess(SkolemCache* sc,
HistogramStat<Kind>* statReductions)
: d_sc(sc), d_statReductions(statReductions)
// forall il.
// n <= i < ite(skk = -1, len(s), skk) ^ 0 < l <= len(s) - i =>
// ~in_re(substr(s, i, l), r)
- Node firstMatch = mkForallInternal(bvl, body);
+ Node firstMatch = utils::mkForallInternal(bvl, body);
Node bvll = nm->mkNode(BOUND_VAR_LIST, l);
Node validLen =
nm->mkNode(AND,
nm->mkNode(STRING_IN_REGEXP, nm->mkNode(STRING_SUBSTR, s, skk, l), r));
// skk != -1 =>
// exists l. (0 <= l < len(s) - skk) ^ in_re(substr(s, skk, l), r))
- Node match = nm->mkNode(
- OR, retNegOne, mkForallInternal(bvll, matchBody.negate()).negate());
+ Node match =
+ nm->mkNode(OR,
+ retNegOne,
+ utils::mkForallInternal(bvll, matchBody.negate()).negate());
// assert:
// IF: n > len(s) OR 0 > n
Node ux1lem = nm->mkNode(GEQ, n, ux1);
lem = nm->mkNode(OR, g.negate(), nm->mkNode(AND, eq, cb, ux1lem));
- lem = mkForallInternal(xbv, lem);
+ lem = utils::mkForallInternal(xbv, lem);
conc.push_back(lem);
Node nonneg = nm->mkNode(GEQ, n, zero);
Node ux1lem = nm->mkNode(GEQ, stoit, ux1);
lem = nm->mkNode(OR, g.negate(), nm->mkNode(AND, eq, cb, ux1lem));
- lem = mkForallInternal(xbv, lem);
+ lem = utils::mkForallInternal(xbv, lem);
conc2.push_back(lem);
Node sneg = nm->mkNode(LT, stoit, zero);
ufip1.eqNode(nm->mkNode(PLUS, ii, nm->mkNode(STRING_LENGTH, y))));
Node body = nm->mkNode(OR, bound.negate(), nm->mkNode(AND, flem));
- Node q = mkForallInternal(bvli, body);
+ Node q = utils::mkForallInternal(bvli, body);
lem.push_back(q);
// assert:
nm->mkNode(STRING_IN_REGEXP, nm->mkNode(STRING_SUBSTR, k2, zero, l), y)
.negate());
// forall l. 0 <= l < len(k2) => ~in_re(substr(k2, 0, l), r)
- Node shortestMatch = mkForallInternal(bvll, body);
+ Node shortestMatch = utils::mkForallInternal(bvll, body);
// in_re(k2, y)
Node match = nm->mkNode(STRING_IN_REGEXP, k2, y);
// k = k1 ++ z ++ k3
.negate());
// forall l. 0 < l < Ul(i + 1) =>
// ~in_re(substr(x, Uf(i + 1) - Ul(i + 1), l), y')
- flem.push_back(mkForallInternal(bvll, shortestMatchBody));
+ flem.push_back(utils::mkForallInternal(bvll, shortestMatchBody));
Node pfxMatch =
nm->mkNode(STRING_SUBSTR, x, ufi, nm->mkNode(MINUS, ii, ufi));
// Us(i) = substr(x, Uf(i), ii - Uf(i)) ++ z ++ Us(i + 1)
.eqNode(nm->mkNode(
STRING_CONCAT, pfxMatch, z, nm->mkNode(APPLY_UF, us, ip1))));
Node body = nm->mkNode(OR, bound.negate(), nm->mkNode(AND, flem));
- Node forall = mkForallInternal(bvli, body);
+ Node forall = utils::mkForallInternal(bvli, body);
lemmas.push_back(forall);
// IF indexof(x, y', 0) = -1
Node bound =
nm->mkNode(AND, nm->mkNode(LEQ, zero, i), nm->mkNode(LT, i, lenr));
Node body = nm->mkNode(OR, bound.negate(), ri.eqNode(res));
- Node rangeA = mkForallInternal(bvi, body);
+ Node rangeA = utils::mkForallInternal(bvi, body);
// upper 65 ... 90
// lower 97 ... 122
Node bound =
nm->mkNode(AND, nm->mkNode(LEQ, zero, i), nm->mkNode(LT, i, lenr));
Node body = nm->mkNode(OR, bound.negate(), ssr.eqNode(ssx));
- Node rangeA = mkForallInternal(bvi, body);
+ Node rangeA = utils::mkForallInternal(bvi, body);
// assert:
// len(r) = len(x) ^
// forall i. 0 <= i < len(r) =>
kind::EQUAL,
NodeManager::currentNM()->mkNode(kind::STRING_SUBSTR, x, b1, lens),
s));
- retNode = NodeManager::currentNM()->mkNode( kind::EXISTS, b1v, body );
+ retNode = utils::mkForallInternal(b1v, body.negate()).negate();
}
else if (t.getKind() == kind::STRING_LEQ)
{
}
conj.push_back(nm->mkNode(ITE, ite_ch));
- Node conjn = nm->mkNode(
- EXISTS, nm->mkNode(BOUND_VAR_LIST, k), nm->mkNode(AND, conj));
+ Node conjn = utils::mkForallInternal(nm->mkNode(BOUND_VAR_LIST, k),
+ nm->mkNode(AND, conj).negate())
+ .negate();
// Intuitively, the reduction says either x and y are equal, or they have
// some (maximal) common prefix after which their characters at position k
// are distinct, and the comparison of their code matches the return value
return ret;
}
-Node StringsPreprocess::mkForallInternal(Node bvl, Node body)
-{
- NodeManager* nm = NodeManager::currentNM();
- QInternalVarAttribute qiva;
- Node qvar;
- if (bvl.hasAttribute(qiva))
- {
- qvar = bvl.getAttribute(qiva);
- }
- else
- {
- SkolemManager* sm = nm->getSkolemManager();
- qvar = sm->mkDummySkolem("qinternal", nm->booleanType());
- // this dummy variable marks that the quantified formula is internal
- qvar.setAttribute(InternalQuantAttribute(), true);
- // remember the dummy variable
- bvl.setAttribute(qiva, qvar);
- }
- // make the internal attribute, and put it in a singleton list
- Node ip = nm->mkNode(INST_ATTRIBUTE, qvar);
- Node ipl = nm->mkNode(INST_PATTERN_LIST, ip);
- // make the overall formula
- return nm->mkNode(FORALL, bvl, body, ipl);
-}
-
} // namespace strings
} // namespace theory
} // namespace cvc5
* visited stores a cache of previous results.
*/
Node simplifyRec(Node t, std::vector<Node>& asserts);
- /**
- * Make internal quantified formula with bound variable list bvl and body.
- * Internally, we get a node corresponding to marking a quantified formula as
- * an "internal" one. This node is provided as the third argument of the
- * FORALL returned by this method. This ensures that E-matching is not applied
- * to the quantified formula.
- */
- static Node mkForallInternal(Node bvl, Node body);
};
} // namespace strings
#include <sstream>
+#include "expr/attribute.h"
+#include "expr/skolem_manager.h"
#include "options/strings_options.h"
+#include "theory/quantifiers/quantifiers_attributes.h"
#include "theory/rewriter.h"
#include "theory/strings/arith_entail.h"
#include "theory/strings/strings_entail.h"
return node.getOperator().getConst<RegExpLoop>().d_loopMinOcc;
}
+/**
+ * Mapping to a dummy node for marking an attribute on internal quantified
+ * formulas. This ensures that reductions are deterministic.
+ */
+struct QInternalVarAttributeId
+{
+};
+typedef expr::Attribute<QInternalVarAttributeId, Node> QInternalVarAttribute;
+
+Node mkForallInternal(Node bvl, Node body)
+{
+ NodeManager* nm = NodeManager::currentNM();
+ QInternalVarAttribute qiva;
+ Node qvar;
+ if (bvl.hasAttribute(qiva))
+ {
+ qvar = bvl.getAttribute(qiva);
+ }
+ else
+ {
+ SkolemManager* sm = nm->getSkolemManager();
+ qvar = sm->mkDummySkolem("qinternal", nm->booleanType());
+ // this dummy variable marks that the quantified formula is internal
+ qvar.setAttribute(InternalQuantAttribute(), true);
+ // remember the dummy variable
+ bvl.setAttribute(qiva, qvar);
+ }
+ // make the internal attribute, and put it in a singleton list
+ Node ip = nm->mkNode(INST_ATTRIBUTE, qvar);
+ Node ipl = nm->mkNode(INST_PATTERN_LIST, ip);
+ // make the overall formula
+ return nm->mkNode(FORALL, bvl, body, ipl);
+}
+
} // namespace utils
} // namespace strings
} // namespace theory
/* Get the minimum occurrences of given regexp loop node. */
unsigned getLoopMinOccurrences(TNode node);
+/**
+ * Make internal quantified formula with bound variable list bvl and body.
+ * Internally, we get a node corresponding to marking a quantified formula as
+ * an "internal" one. This node is provided as the third argument of the
+ * FORALL returned by this method. This ensures that E-matching is not applied
+ * to the quantified formula.
+ */
+Node mkForallInternal(Node bvl, Node body);
+
} // namespace utils
} // namespace strings
} // namespace theory
regress1/strings/rev-ex5.smt2
regress1/strings/rew-020618.smt2
regress1/strings/rew-check1.smt2
+ regress1/strings/seq-quant-infinite-branch.smt2
regress1/strings/simple-re-consume.smt2
regress1/strings/stoi-400million.smt2
regress1/strings/stoi-solve.smt2
-; COMMAND-LINE: --fmf-fun --no-check-models
+; COMMAND-LINE: --fmf-fun --no-check-models --fmf-bound
; EXPECT: sat
(set-logic UFDTSLIA)
(set-option :produce-models true)
-; COMMAND-LINE: --strings-exp --finite-model-find
+; COMMAND-LINE: --strings-exp --finite-model-find --fmf-bound
; EXPECT: sat
(set-logic ALL)
(declare-datatypes ((UNIT 0)) (((Unit))
--- /dev/null
+(set-logic ALL)
+(set-info :status unsat)
+(declare-const x8 Bool)
+(set-option :strings-exp true)
+(declare-fun s () (Seq Int))
+(declare-fun x () Int)
+(declare-fun i () Int)
+(declare-fun i@ () Int)
+(assert (and (forall ((u Int)) (or (> 0 u) (>= u i) (distinct x (seq.nth s u))))
+ (or (and x8 (not x8))
+ (and (= i@ (+ i 1))
+ (distinct x (seq.nth s i))
+ (exists ((u Int)) (and (<= 0 u)
+ (< u i@)
+ (= x (seq.nth s u))))
+ )
+ )))
+(check-sat)
projects / cvc5.git / commitdiff