From 59d935b0210fe20cdddf5de2be91bb26a66d05fb Mon Sep 17 00:00:00 2001 From: Andres Noetzli Date: Mon, 17 May 2021 11:33:01 -0700 Subject: [PATCH] Fix `SPLIT_EQ_STRIP_R`/`SPLIT_EQ_STRIP_L` rewrites (#6550) Fixes #6520. The `SPLIT_EQ_STRIP_R`/`SPLIT_EQ_STRIP_L` rewrites were applied too aggressively. Those rewrites attempt to rewrite string equalities between concatenations where the prefix on one side is provably shorter than the prefix on the other side. The length of the shorter prefix is then stripped from the longer prefix. However, cvc5 was not checking whether it was able to strip the length of the full prefix. If cvc5 cannot strip the full length of the shorter prefix, then the rewrite does not apply because parts of the shorter prefix would have to be kept. This commit adds an additional condition that checks whether the length of the full prefix was stripped. --- src/theory/strings/sequences_rewriter.cpp | 42 +++++++++++++------- test/regress/CMakeLists.txt | 1 + test/regress/regress0/strings/issue6520.smt2 | 8 ++++ 3 files changed, 37 insertions(+), 14 deletions(-) create mode 100644 test/regress/regress0/strings/issue6520.smt2 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 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().isZero()) + { + std::vector 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 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().isZero()) + { + pfxv0.insert(pfxv0.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) + .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) -- 2.30.2