From 2df0cc4257391daf6daf175826d69a735517ad19 Mon Sep 17 00:00:00 2001 From: Andres Noetzli Date: Fri, 17 Dec 2021 13:46:14 -0800 Subject: [PATCH] Fix rewrite for `str.update(str.rev(s), n, t))` (#7838) Fixes https://github.com/cvc5/cvc5-projects/issues/390. This commit fixes two issues with the rewrite: (1) the rewrite should only apply if the update is of size 1 and (2) the `str.rev(...)` should be removed inside the `str.update(...)`. --- src/theory/strings/sequences_rewriter.cpp | 6 ++++-- test/regress/CMakeLists.txt | 1 + .../strings/proj-issue390-update-rev-rewrite.smt2 | 10 ++++++++++ 3 files changed, 15 insertions(+), 2 deletions(-) create mode 100644 test/regress/regress0/strings/proj-issue390-update-rev-rewrite.smt2 diff --git a/src/theory/strings/sequences_rewriter.cpp b/src/theory/strings/sequences_rewriter.cpp index aadca9904..1094bd14d 100644 --- a/src/theory/strings/sequences_rewriter.cpp +++ b/src/theory/strings/sequences_rewriter.cpp @@ -2085,13 +2085,15 @@ Node SequencesRewriter::rewriteUpdate(Node node) } } - if (s.getKind() == STRING_REV) + if (s.getKind() == STRING_REV && d_stringsEntail.checkLengthOne(x)) { + // str.update(str.rev(s), n, t) ---> + // str.rev(str.update(s, len(s) - (n + 1), t)) NodeManager* nm = NodeManager::currentNM(); Node idx = nm->mkNode(MINUS, nm->mkNode(STRING_LENGTH, s), nm->mkNode(PLUS, i, nm->mkConstInt(Rational(1)))); - Node ret = nm->mkNode(STRING_REV, nm->mkNode(STRING_UPDATE, s, idx, x)); + Node ret = nm->mkNode(STRING_REV, nm->mkNode(STRING_UPDATE, s[0], idx, x)); return returnRewrite(node, ret, Rewrite::UPD_REV); } diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index 4d8a7a65f..568fec3ce 100644 --- a/test/regress/CMakeLists.txt +++ b/test/regress/CMakeLists.txt @@ -1273,6 +1273,7 @@ set(regress_0_tests regress0/strings/norn-simp-rew.smt2 regress0/strings/parser-syms.cvc.smt2 regress0/strings/proj-issue316-regexp-ite.smt2 + regress0/strings/proj-issue390-update-rev-rewrite.smt2 regress0/strings/re_diff.smt2 regress0/strings/re-in-rewrite.smt2 regress0/strings/re-syntax.smt2 diff --git a/test/regress/regress0/strings/proj-issue390-update-rev-rewrite.smt2 b/test/regress/regress0/strings/proj-issue390-update-rev-rewrite.smt2 new file mode 100644 index 000000000..991aa594a --- /dev/null +++ b/test/regress/regress0/strings/proj-issue390-update-rev-rewrite.smt2 @@ -0,0 +1,10 @@ +(set-logic QF_BVSLIRA) +(declare-const _x3 String) +(declare-const _x5 Real) +(assert (= + (str.rev _x3) + (str.at + (str.update (str.rev _x3) (bv2nat #b000000000000000000000000000000000001) (str.rev _x3)) + (bv2nat #b000000000000000000000000000000000001)))) +(set-info :status sat) +(check-sat) -- 2.30.2