diff options
| -rw-r--r-- | src/theory/strings/sequences_rewriter.cpp | 42 | ||||
| -rw-r--r-- | test/regress/CMakeLists.txt | 1 | ||||
| -rw-r--r-- | test/regress/regress0/strings/issue6520.smt2 | 8 |
3 files changed, 37 insertions, 14 deletions
diff --git a/src/theory/strings/sequences_rewriter.cpp b/src/theory/strings/sequences_rewriter.cpp index 84127e8e3..d3c750185 100644 --- a/src/theory/strings/sequences_rewriter.cpp +++ b/src/theory/strings/sequences_rewriter.cpp @@ -468,13 +468,20 @@ Node SequencesRewriter::rewriteStrEqualityExt(Node node) if (StringsEntail::stripSymbolicLength( pfxv1, rpfxv1, 1, lenPfx0, true)) { - std::vector<Node> sfxv0(v0.begin() + i, v0.end()); - pfxv1.insert(pfxv1.end(), v1.begin() + j, v1.end()); - Node ret = nm->mkNode(kind::AND, - pfx0.eqNode(utils::mkConcat(rpfxv1, stype)), - utils::mkConcat(sfxv0, stype) - .eqNode(utils::mkConcat(pfxv1, stype))); - return returnRewrite(node, ret, Rewrite::SPLIT_EQ_STRIP_R); + // The rewrite requires the full left-hand prefix length to be + // stripped (otherwise we would have to keep parts of the + // left-hand prefix). + if (lenPfx0.isConst() && lenPfx0.getConst<Rational>().isZero()) + { + std::vector<Node> sfxv0(v0.begin() + i, v0.end()); + pfxv1.insert(pfxv1.end(), v1.begin() + j, v1.end()); + Node ret = + nm->mkNode(kind::AND, + pfx0.eqNode(utils::mkConcat(rpfxv1, stype)), + utils::mkConcat(sfxv0, stype) + .eqNode(utils::mkConcat(pfxv1, stype))); + return returnRewrite(node, ret, Rewrite::SPLIT_EQ_STRIP_R); + } } // If the prefix of the right-hand side is (strictly) longer than @@ -496,13 +503,20 @@ Node SequencesRewriter::rewriteStrEqualityExt(Node node) if (StringsEntail::stripSymbolicLength( pfxv0, rpfxv0, 1, lenPfx1, true)) { - pfxv0.insert(pfxv0.end(), v0.begin() + i, v0.end()); - std::vector<Node> sfxv1(v1.begin() + j, v1.end()); - Node ret = nm->mkNode(kind::AND, - utils::mkConcat(rpfxv0, stype).eqNode(pfx1), - utils::mkConcat(pfxv0, stype) - .eqNode(utils::mkConcat(sfxv1, stype))); - return returnRewrite(node, ret, Rewrite::SPLIT_EQ_STRIP_L); + // 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<Rational>().isZero()) + { + pfxv0.insert(pfxv0.end(), v0.begin() + i, v0.end()); + std::vector<Node> sfxv1(v1.begin() + j, v1.end()); + Node ret = + nm->mkNode(kind::AND, + utils::mkConcat(rpfxv0, stype).eqNode(pfx1), + utils::mkConcat(pfxv0, stype) + .eqNode(utils::mkConcat(sfxv1, stype))); + return returnRewrite(node, ret, Rewrite::SPLIT_EQ_STRIP_L); + } } // If the prefix of the left-hand side is (strictly) longer than diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index 8ed170da9..5e9b38e8d 100644 --- a/test/regress/CMakeLists.txt +++ b/test/regress/CMakeLists.txt @@ -1128,6 +1128,7 @@ set(regress_0_tests regress0/strings/issue5915-repl-ctn-rewrite.smt2 regress0/strings/issue6203-3-unfold-trivial-true.smt2 regress0/strings/issue6510-seq-bool.smt2 + regress0/strings/issue6520.smt2 regress0/strings/itos-entail.smt2 regress0/strings/large-model.smt2 regress0/strings/leadingzero001.smt2 diff --git a/test/regress/regress0/strings/issue6520.smt2 b/test/regress/regress0/strings/issue6520.smt2 new file mode 100644 index 000000000..23a938365 --- /dev/null +++ b/test/regress/regress0/strings/issue6520.smt2 @@ -0,0 +1,8 @@ +; COMMAND-LINE: --ext-rew-prep +(set-logic QF_SLIA) +(declare-fun a () String) +(declare-fun b () String) +(declare-fun c () String) +(assert (= (str.++ "AB" b c) (str.++ c "B" a))) +(set-info :status sat) +(check-sat) |