diff options
| -rw-r--r-- | src/theory/strings/theory_strings_rewriter.cpp | 51 | ||||
| -rw-r--r-- | test/regress/Makefile.tests | 1 | ||||
| -rw-r--r-- | test/regress/regress2/strings/repl-repl.smt2 | 37 | ||||
| -rw-r--r-- | test/unit/theory/theory_strings_rewriter_white.h | 23 |
4 files changed, 108 insertions, 4 deletions
diff --git a/src/theory/strings/theory_strings_rewriter.cpp b/src/theory/strings/theory_strings_rewriter.cpp index e09eefddc..7e5f7102d 100644 --- a/src/theory/strings/theory_strings_rewriter.cpp +++ b/src/theory/strings/theory_strings_rewriter.cpp @@ -2203,6 +2203,57 @@ Node TheoryStringsRewriter::rewriteReplace( Node node ) { return returnRewrite(node, res, "repl-subst-idx"); } } + + if (node[0].getKind() == STRING_STRREPL) + { + Node x = node[0]; + Node y = node[1]; + Node z = node[2]; + if (x[0] == x[2] && x[0] == y) + { + // (str.replace (str.replace y w y) y z) --> + // (str.replace (str.replace y w z) y z) + // if (str.len w) >= (str.len z) and w != z + // + // Reasoning: There are two cases: (1) w does not appear in y and (2) w + // does appear in y. + // + // Case (1): In this case, the reasoning is trivial. The + // inner replace does not do anything, so we can just replace its third + // argument with any string. + // + // Case (2): After the inner replace, we are guaranteed to have a string + // that contains y at the index of w in the original string y. The outer + // replace then replaces that y with z, so we can short-circuit that + // replace by directly replacing w with z in the inner replace. We can + // only do that if the result of the new inner replace does not contain + // y, otherwise we end up doing two replaces that are different from the + // original expression. We enforce that by requiring that the length of w + // has to be greater or equal to the length of z and that w and z have to + // be different. This makes sure that an inner replace changes a string + // to a string that is shorter than y, making it impossible for the outer + // replace to match. + Node w = x[1]; + + // (str.len w) >= (str.len z) + Node wlen = nm->mkNode(kind::STRING_LENGTH, w); + Node zlen = nm->mkNode(kind::STRING_LENGTH, z); + if (checkEntailArith(wlen, zlen)) + { + // w != z + Node wEqZ = Rewriter::rewrite(nm->mkNode(kind::EQUAL, w, z)); + if (wEqZ.isConst() && !wEqZ.getConst<bool>()) + { + Node ret = nm->mkNode(kind::STRING_STRREPL, + nm->mkNode(kind::STRING_STRREPL, y, w, z), + y, + z); + return returnRewrite(node, ret, "repl-repl-short-circuit"); + } + } + } + } + if (node[1].getKind() == STRING_STRREPL) { if (node[1][0] == node[0]) diff --git a/test/regress/Makefile.tests b/test/regress/Makefile.tests index 7f33adac1..59a5b5f64 100644 --- a/test/regress/Makefile.tests +++ b/test/regress/Makefile.tests @@ -1686,6 +1686,7 @@ REG2_TESTS = \ regress2/strings/cmu-prereg-fmf.smt2 \ regress2/strings/cmu-repl-len-nterm.smt2 \ regress2/strings/norn-dis-0707-3.smt2 \ + regress2/strings/repl-repl.smt2 \ regress2/sygus/MPwL_d1s3.sy \ regress2/sygus/array_sum_dd.sy \ regress2/sygus/cegisunif-depth1-bv.sy \ diff --git a/test/regress/regress2/strings/repl-repl.smt2 b/test/regress/regress2/strings/repl-repl.smt2 new file mode 100644 index 000000000..baa4a31d7 --- /dev/null +++ b/test/regress/regress2/strings/repl-repl.smt2 @@ -0,0 +1,37 @@ +; COMMAND-LINE: --strings-exp --strings-fmf --incremental +; EXPECT: sat +; EXPECT: unsat +; EXPECT: sat +; EXPECT: sat +; EXPECT: sat +(set-logic SLIA) +(declare-const x String) +(declare-const y String) +(declare-const z String) + +(push 1) +(assert (not (= (str.replace (str.replace x "B" x) x "AB") (str.replace (str.replace x "B" "AB") x "AB")))) +(check-sat) +(pop 1) + +(push 1) +(assert (not (= (str.replace (str.replace x "B" x) x "A") (str.replace (str.replace x "B" "A") x "A")))) +(check-sat) +(pop 1) + +(push 1) +(assert (not (= (str.replace (str.replace x z x) x y) (str.replace (str.replace x z y) x y)))) +(check-sat) +(pop 1) + +(push 1) +(assert (not (= (str.replace (str.replace x z x) x y) (str.replace (str.replace x z y) x y)))) +(assert (<= (str.len y) (str.len z))) +(check-sat) +(pop 1) + +(push 1) +(assert (not (= (str.replace (str.replace x z x) x y) (str.replace (str.replace x z y) x y)))) +(assert (not (= y z))) +(check-sat) +(pop 1) diff --git a/test/unit/theory/theory_strings_rewriter_white.h b/test/unit/theory/theory_strings_rewriter_white.h index 67dc20541..2710a60fe 100644 --- a/test/unit/theory/theory_strings_rewriter_white.h +++ b/test/unit/theory/theory_strings_rewriter_white.h @@ -336,12 +336,27 @@ class TheoryStringsRewriterWhite : public CxxTest::TestSuite Node y = d_nm->mkVar("y", strType); Node z = d_nm->mkVar("z", strType); - // (str.replace "A" (str.replace "B", x, "C") "D") --> "A" + // (str.replace (str.replace x "B" x) x "A") --> + // (str.replace (str.replace x "B" "A") x "A") Node repl_repl = d_nm->mkNode(kind::STRING_STRREPL, - a, - d_nm->mkNode(kind::STRING_STRREPL, b, x, c), - d); + d_nm->mkNode(kind::STRING_STRREPL, x, b, x), + x, + a); + Node repl_repl_short = + d_nm->mkNode(kind::STRING_STRREPL, + d_nm->mkNode(kind::STRING_STRREPL, x, b, a), + x, + a); Node res_repl_repl = Rewriter::rewrite(repl_repl); + Node res_repl_repl_short = Rewriter::rewrite(repl_repl_short); + TS_ASSERT_EQUALS(res_repl_repl, res_repl_repl_short); + + // (str.replace "A" (str.replace "B", x, "C") "D") --> "A" + repl_repl = d_nm->mkNode(kind::STRING_STRREPL, + a, + d_nm->mkNode(kind::STRING_STRREPL, b, x, c), + d); + res_repl_repl = Rewriter::rewrite(repl_repl); TS_ASSERT_EQUALS(res_repl_repl, a); // (str.replace "A" (str.replace "B", x, "A") "D") -/-> "A" |