From f7b60f68bb6a7945eebb7f97a5f63302ad0ddc67 Mon Sep 17 00:00:00 2001 From: Andres Noetzli Date: Fri, 4 Jun 2021 20:22:57 -0700 Subject: [PATCH] Remove unwanted side effects in `SPLIT_EQ_STRIP_L` (#6689) Fixes #6681. When checking whether SPLIT_EQ_STRIP_L applies, we were using sripSymbolicLength, which changes its inputs depending on how many elements of the concatenation it could strip. However, one of the arguments, pfxv0, was reused across multiple checks if the strip did not result in a rewrite. Later invocations were wrong as a result. This commit changes the call to stripSymbolicLength() to use a new copy of the vector instead. --- src/theory/strings/sequences_rewriter.cpp | 9 +++++---- test/regress/CMakeLists.txt | 1 + .../regress0/strings/issue6681-split-eq-strip-l.smt2 | 8 ++++++++ 3 files changed, 14 insertions(+), 4 deletions(-) create mode 100644 test/regress/regress0/strings/issue6681-split-eq-strip-l.smt2 diff --git a/src/theory/strings/sequences_rewriter.cpp b/src/theory/strings/sequences_rewriter.cpp index 7ef1242c6..f63b416ff 100644 --- a/src/theory/strings/sequences_rewriter.cpp +++ b/src/theory/strings/sequences_rewriter.cpp @@ -437,7 +437,7 @@ Node SequencesRewriter::rewriteStrEqualityExt(Node node) size_t startRhs = 0; for (size_t i = 0, size0 = v0.size(); i <= size0; i++) { - std::vector pfxv0(v0.begin(), v0.begin() + i); + const std::vector pfxv0(v0.begin(), v0.begin() + i); Node pfx0 = utils::mkConcat(pfxv0, stype); for (size_t j = startRhs, size1 = v1.size(); j <= size1; j++) { @@ -502,21 +502,22 @@ Node SequencesRewriter::rewriteStrEqualityExt(Node node) // Example: // (= (str.++ x "AB" z) (str.++ "A" x y)) ---> // (and (= (str.++ x "A") (str.++ "A" x)) (= (str.++ "B" z) y)) + std::vector sfxv0 = pfxv0; std::vector rpfxv0; if (StringsEntail::stripSymbolicLength( - pfxv0, rpfxv0, 1, lenPfx1, true)) + sfxv0, rpfxv0, 1, lenPfx1, true)) { // The rewrite requires the full right-hand prefix length to be // stripped (otherwise we would have to keep parts of the // right-hand prefix). if (lenPfx1.isConst() && lenPfx1.getConst().isZero()) { - pfxv0.insert(pfxv0.end(), v0.begin() + i, v0.end()); + sfxv0.insert(sfxv0.end(), v0.begin() + i, v0.end()); std::vector sfxv1(v1.begin() + j, v1.end()); Node ret = nm->mkNode(kind::AND, utils::mkConcat(rpfxv0, stype).eqNode(pfx1), - utils::mkConcat(pfxv0, stype) + utils::mkConcat(sfxv0, stype) .eqNode(utils::mkConcat(sfxv1, stype))); return returnRewrite(node, ret, Rewrite::SPLIT_EQ_STRIP_L); } diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index 707e5e43d..237ca77dd 100644 --- a/test/regress/CMakeLists.txt +++ b/test/regress/CMakeLists.txt @@ -1156,6 +1156,7 @@ set(regress_0_tests regress0/strings/issue6560-indexof-reduction.smt2 regress0/strings/issue6604-re-elim.smt2 regress0/strings/issue6643-ctn-decompose-conflict.smt2 + regress0/strings/issue6681-split-eq-strip-l.smt2 regress0/strings/itos-entail.smt2 regress0/strings/large-model.smt2 regress0/strings/leadingzero001.smt2 diff --git a/test/regress/regress0/strings/issue6681-split-eq-strip-l.smt2 b/test/regress/regress0/strings/issue6681-split-eq-strip-l.smt2 new file mode 100644 index 000000000..213d9737b --- /dev/null +++ b/test/regress/regress0/strings/issue6681-split-eq-strip-l.smt2 @@ -0,0 +1,8 @@ +(set-logic QF_SLIA) +(declare-fun a () String) +(declare-fun b () String) +(declare-fun c () String) +(declare-fun d () String) +(assert (= (str.++ "A" a "CBA" b "BA" d) (str.++ b "BA" d a "CBA" c))) +(set-info :status sat) +(check-sat) -- 2.30.2