summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--src/theory/strings/term_registry.cpp12
-rw-r--r--src/theory/strings/theory_strings_preprocess.cpp17
-rw-r--r--test/regress/CMakeLists.txt3
-rw-r--r--test/regress/regress0/strings/indexof_re-start-index.smt28
-rw-r--r--test/regress/regress2/strings/issue6636-replace-re-all.smt26
-rw-r--r--test/regress/regress2/strings/issue6637-replace-re-all.smt27
6 files changed, 40 insertions, 13 deletions
diff --git a/src/theory/strings/term_registry.cpp b/src/theory/strings/term_registry.cpp
index c7b3b5300..aac9e9313 100644
--- a/src/theory/strings/term_registry.cpp
+++ b/src/theory/strings/term_registry.cpp
@@ -90,13 +90,17 @@ Node TermRegistry::eagerReduce(Node t, SkolemCache* sc)
}
else if (tk == STRING_STRIDOF || tk == STRING_INDEXOF_RE)
{
- // (and (>= (f x y n) (- 1)) (<= (f x y n) (str.len x)))
+ // (and
+ // (or (= (f x y n) (- 1)) (>= (f x y n) n))
+ // (<= (f x y n) (str.len x)))
//
// where f in { str.indexof, str.indexof_re }
Node l = nm->mkNode(STRING_LENGTH, t[0]);
- lemma = nm->mkNode(AND,
- nm->mkNode(GEQ, t, nm->mkConst(Rational(-1))),
- nm->mkNode(LEQ, t, l));
+ lemma = nm->mkNode(
+ AND,
+ nm->mkNode(
+ OR, nm->mkConst(Rational(-1)).eqNode(t), nm->mkNode(GEQ, t, t[2])),
+ nm->mkNode(LEQ, t, l));
}
else if (tk == STRING_STOI)
{
diff --git a/src/theory/strings/theory_strings_preprocess.cpp b/src/theory/strings/theory_strings_preprocess.cpp
index 83a4fa04a..152a3e180 100644
--- a/src/theory/strings/theory_strings_preprocess.cpp
+++ b/src/theory/strings/theory_strings_preprocess.cpp
@@ -301,14 +301,14 @@ Node StringsPreprocess::reduce(Node t,
Node bvll = nm->mkNode(BOUND_VAR_LIST, l);
Node validLen =
nm->mkNode(AND,
- nm->mkNode(GEQ, l, n),
+ nm->mkNode(GEQ, l, zero),
nm->mkNode(LEQ, l, nm->mkNode(MINUS, sLen, skk)));
Node matchBody = nm->mkNode(
AND,
validLen,
nm->mkNode(STRING_IN_REGEXP, nm->mkNode(STRING_SUBSTR, s, skk, l), r));
// skk != -1 =>
- // exists l. n <= l < len(s) - skk ^ in_re(substr(s, skk, l), r))
+ // 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());
@@ -321,7 +321,7 @@ Node StringsPreprocess::reduce(Node t,
// n <= i < ite(skk = -1, len(s), skk) ^ 0 < l <= len(s) - i =>
// ~in_re(substr(s, i, l), r)) ^
// (skk != -1 =>
- // exists l. n <= l < len(s) - skk ^ in_re(substr(s, skk, l), r))
+ // exists l. 0 <= l < len(s) - skk ^ in_re(substr(s, skk, l), r))
//
// Note that this reduction relies on eager reduction lemmas being sent to
// properly limit the range of skk.
@@ -758,9 +758,8 @@ Node StringsPreprocess::reduce(Node t,
Node emp = Word::mkEmptyWord(t.getType());
Node yp = nm->mkNode(REGEXP_DIFF, y, nm->mkNode(STRING_TO_REGEXP, emp));
- Node idx = nm->mkNode(STRING_INDEXOF_RE, x, yp, zero);
// indexof_re(x, y', 0) = -1
- Node noMatch = idx.eqNode(negOne);
+ Node noMatch = nm->mkNode(STRING_INDEXOF_RE, x, yp, zero).eqNode(negOne);
Node ufno = nm->mkNode(APPLY_UF, uf, numOcc);
Node usno = nm->mkNode(APPLY_UF, us, numOcc);
@@ -791,7 +790,7 @@ Node StringsPreprocess::reduce(Node t,
Node ii = nm->mkNode(MINUS, ufip1, ulip1);
std::vector<Node> flem;
- // Ul(i) > 0
+ // Ul(i + 1) > 0
flem.push_back(nm->mkNode(GT, ulip1, zero));
// Uf(i + 1) = indexof_re(x, yp, Uf(i)) + Ul(i + 1)
flem.push_back(ufip1.eqNode(
@@ -829,13 +828,13 @@ Node StringsPreprocess::reduce(Node t,
// k = Us(0) ^ Us(numOcc) = substr(x, Uf(numOcc)) ^
// Uf(0) = 0 ^ indexof_re(substr(x, Uf(numOcc)), y', 0) = -1 ^
// forall i. 0 <= i < nummOcc =>
- // Ul(i) > 0 ^
+ // Ul(i + 1) > 0 ^
// Uf(i + 1) = indexof_re(x, yp, Uf(i)) + Ul(i + 1) ^
// in_re(substr(x, ii, Ul(i + 1)), y') ^
// forall l. 0 < l < Ul(i + 1) =>
- // ~in_re(substr(x, Uf(i + 1) - Ul(i + 1), l), y')
+ // ~in_re(substr(x, ii, l), y')
// Us(i) = substr(x, Uf(i), ii - Uf(i)) ++ z ++ Us(i + 1)
- // where ii = Uf(i + 1) - Ul(i)
+ // where ii = Uf(i + 1) - Ul(i + 1)
// where y' = re.diff(y, "")
//
// Conceptually, y' is the regex y but excluding the empty string (because
diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index 860d1854a..6036b021b 100644
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -1120,6 +1120,7 @@ set(regress_0_tests
regress0/strings/ilc-like.smt2
regress0/strings/indexof-sym-simp.smt2
regress0/strings/indexof_re.smt2
+ regress0/strings/indexof_re-start-index.smt2
regress0/strings/is_digit_simple.smt2
regress0/strings/issue1189.smt2
regress0/strings/issue2958.smt2
@@ -2456,6 +2457,8 @@ set(regress_2_tests
regress2/strings/issue6483.smt2
regress2/strings/issue6057-replace-re-all.smt2
regress2/strings/issue6057-replace-re-all-simplified.smt2
+ regress2/strings/issue6636-replace-re-all.smt2
+ regress2/strings/issue6637-replace-re-all.smt2
regress2/strings/issue918.smt2
regress2/strings/non_termination_regular_expression6.smt2
regress2/strings/range-perf.smt2
diff --git a/test/regress/regress0/strings/indexof_re-start-index.smt2 b/test/regress/regress0/strings/indexof_re-start-index.smt2
new file mode 100644
index 000000000..9f17c5bef
--- /dev/null
+++ b/test/regress/regress0/strings/indexof_re-start-index.smt2
@@ -0,0 +1,8 @@
+; COMMAND-LINE: --strings-exp
+(set-logic QF_SLIA)
+(declare-fun i () Int)
+(declare-fun a () String)
+(assert (= i (str.indexof_re a (str.to_re "abc") 3)))
+(assert (and (>= i 0) (< i 3)))
+(set-info :status unsat)
+(check-sat)
diff --git a/test/regress/regress2/strings/issue6636-replace-re-all.smt2 b/test/regress/regress2/strings/issue6636-replace-re-all.smt2
new file mode 100644
index 000000000..779ef3af6
--- /dev/null
+++ b/test/regress/regress2/strings/issue6636-replace-re-all.smt2
@@ -0,0 +1,6 @@
+; COMMAND-LINE: --strings-exp
+(set-logic QF_SLIA)
+(declare-fun a () String)
+(assert (not (= a (str.replace_re_all a (re.++ (re.* re.allchar) (str.to_re a) (re.* re.allchar)) a))))
+(set-info :status unsat)
+(check-sat)
diff --git a/test/regress/regress2/strings/issue6637-replace-re-all.smt2 b/test/regress/regress2/strings/issue6637-replace-re-all.smt2
new file mode 100644
index 000000000..df4e0bd0e
--- /dev/null
+++ b/test/regress/regress2/strings/issue6637-replace-re-all.smt2
@@ -0,0 +1,7 @@
+; COMMAND-LINE: --strings-exp
+(set-logic QF_SLIA)
+(declare-fun a () String)
+(assert (= (str.len a) 2))
+(assert (= (str.len (str.replace_re_all a (str.to_re "A") "B")) 3))
+(set-info :status unsat)
+(check-sat)
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback