summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--src/smt/set_defaults.cpp11
-rw-r--r--src/theory/quantifiers/fmf/bounded_integers.cpp13
-rw-r--r--src/theory/quantifiers/quantifiers_modules.cpp8
-rw-r--r--src/theory/strings/regexp_elim.cpp8
-rw-r--r--src/theory/strings/regexp_operation.cpp6
-rw-r--r--src/theory/strings/theory_strings_preprocess.cpp65
-rw-r--r--src/theory/strings/theory_strings_preprocess.h8
-rw-r--r--src/theory/strings/theory_strings_utils.cpp37
-rw-r--r--src/theory/strings/theory_strings_utils.h9
-rw-r--r--test/regress/CMakeLists.txt1
-rw-r--r--test/regress/regress1/fmf/bug651.smt22
-rw-r--r--test/regress/regress1/quantifiers/issue3537.smt22
-rw-r--r--test/regress/regress1/strings/seq-quant-infinite-branch.smt218
13 files changed, 115 insertions, 73 deletions
diff --git a/src/smt/set_defaults.cpp b/src/smt/set_defaults.cpp
index 7ae07d196..ee3701d51 100644
--- a/src/smt/set_defaults.cpp
+++ b/src/smt/set_defaults.cpp
@@ -292,14 +292,11 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver)
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;
diff --git a/src/theory/quantifiers/fmf/bounded_integers.cpp b/src/theory/quantifiers/fmf/bounded_integers.cpp
index 5ecc33778..3fd478c31 100644
--- a/src/theory/quantifiers/fmf/bounded_integers.cpp
+++ b/src/theory/quantifiers/fmf/bounded_integers.cpp
@@ -317,6 +317,19 @@ void BoundedIntegers::checkOwnership(Node f)
{
//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();
diff --git a/src/theory/quantifiers/quantifiers_modules.cpp b/src/theory/quantifiers/quantifiers_modules.cpp
index f6b8f30f4..27ec187a9 100644
--- a/src/theory/quantifiers/quantifiers_modules.cpp
+++ b/src/theory/quantifiers/quantifiers_modules.cpp
@@ -16,6 +16,7 @@
#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"
@@ -74,14 +75,15 @@ void QuantifiersModules::initialize(QuantifiersState& qs,
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());
diff --git a/src/theory/strings/regexp_elim.cpp b/src/theory/strings/regexp_elim.cpp
index 18a5b049a..dfe006a86 100644
--- a/src/theory/strings/regexp_elim.cpp
+++ b/src/theory/strings/regexp_elim.cpp
@@ -347,7 +347,7 @@ Node RegExpElimination::eliminateConcat(Node atom, bool isAgg)
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));
@@ -486,7 +486,7 @@ Node RegExpElimination::eliminateConcat(Node atom, bool isAgg)
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.
@@ -575,7 +575,7 @@ Node RegExpElimination::eliminateStar(Node atom, bool isAgg)
: 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")
@@ -605,7 +605,7 @@ Node RegExpElimination::eliminateStar(Node atom, bool isAgg)
.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.
diff --git a/src/theory/strings/regexp_operation.cpp b/src/theory/strings/regexp_operation.cpp
index 106ce09d0..268368e7f 100644
--- a/src/theory/strings/regexp_operation.cpp
+++ b/src/theory/strings/regexp_operation.cpp
@@ -928,7 +928,8 @@ Node RegExpOpr::reduceRegExpNeg(Node mem)
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
@@ -999,7 +1000,8 @@ Node RegExpOpr::reduceRegExpNegConcatFixed(Node mem, Node reLen, size_t index)
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;
}
diff --git a/src/theory/strings/theory_strings_preprocess.cpp b/src/theory/strings/theory_strings_preprocess.cpp
index 5f21d6e65..550a9af8b 100644
--- a/src/theory/strings/theory_strings_preprocess.cpp
+++ b/src/theory/strings/theory_strings_preprocess.cpp
@@ -20,9 +20,9 @@
#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"
@@ -35,13 +35,6 @@ namespace cvc5 {
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)
@@ -299,7 +292,7 @@ Node StringsPreprocess::reduce(Node t,
// 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,
@@ -311,8 +304,10 @@ Node StringsPreprocess::reduce(Node t,
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
@@ -382,7 +377,7 @@ Node StringsPreprocess::reduce(Node t,
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);
@@ -470,7 +465,7 @@ Node StringsPreprocess::reduce(Node t,
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);
@@ -651,7 +646,7 @@ Node StringsPreprocess::reduce(Node t,
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:
@@ -717,7 +712,7 @@ Node StringsPreprocess::reduce(Node t,
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
@@ -811,7 +806,7 @@ Node StringsPreprocess::reduce(Node t,
.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)
@@ -820,7 +815,7 @@ Node StringsPreprocess::reduce(Node t,
.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
@@ -886,7 +881,7 @@ Node StringsPreprocess::reduce(Node t,
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
@@ -921,7 +916,7 @@ Node StringsPreprocess::reduce(Node t,
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) =>
@@ -952,7 +947,7 @@ Node StringsPreprocess::reduce(Node t,
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)
{
@@ -982,8 +977,9 @@ Node StringsPreprocess::reduce(Node t,
}
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
@@ -1095,31 +1091,6 @@ Node StringsPreprocess::processAssertion(Node n, std::vector<Node>& asserts)
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
diff --git a/src/theory/strings/theory_strings_preprocess.h b/src/theory/strings/theory_strings_preprocess.h
index 7f0efe50f..01e6fa856 100644
--- a/src/theory/strings/theory_strings_preprocess.h
+++ b/src/theory/strings/theory_strings_preprocess.h
@@ -91,14 +91,6 @@ class StringsPreprocess {
* 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
diff --git a/src/theory/strings/theory_strings_utils.cpp b/src/theory/strings/theory_strings_utils.cpp
index cfe126ef3..27bf090ca 100644
--- a/src/theory/strings/theory_strings_utils.cpp
+++ b/src/theory/strings/theory_strings_utils.cpp
@@ -17,7 +17,10 @@
#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"
@@ -421,6 +424,40 @@ unsigned getLoopMinOccurrences(TNode node)
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
diff --git a/src/theory/strings/theory_strings_utils.h b/src/theory/strings/theory_strings_utils.h
index ec093031e..58162ac1b 100644
--- a/src/theory/strings/theory_strings_utils.h
+++ b/src/theory/strings/theory_strings_utils.h
@@ -216,6 +216,15 @@ unsigned getLoopMaxOccurrences(TNode node);
/* 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
diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index da67705f5..5312e70a3 100644
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -2198,6 +2198,7 @@ set(regress_1_tests
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
diff --git a/test/regress/regress1/fmf/bug651.smt2 b/test/regress/regress1/fmf/bug651.smt2
index d243e0ce7..956a55cd3 100644
--- a/test/regress/regress1/fmf/bug651.smt2
+++ b/test/regress/regress1/fmf/bug651.smt2
@@ -1,4 +1,4 @@
-; 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)
diff --git a/test/regress/regress1/quantifiers/issue3537.smt2 b/test/regress/regress1/quantifiers/issue3537.smt2
index 7f0ab060f..442eb65ac 100644
--- a/test/regress/regress1/quantifiers/issue3537.smt2
+++ b/test/regress/regress1/quantifiers/issue3537.smt2
@@ -1,4 +1,4 @@
-; 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))
diff --git a/test/regress/regress1/strings/seq-quant-infinite-branch.smt2 b/test/regress/regress1/strings/seq-quant-infinite-branch.smt2
new file mode 100644
index 000000000..9816301d4
--- /dev/null
+++ b/test/regress/regress1/strings/seq-quant-infinite-branch.smt2
@@ -0,0 +1,18 @@
+(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)
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback