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(...)`.

diff --git a/src/theory/strings/sequences_rewriter.cpp b/src/theory/strings/sequences_rewriter.cpp
index aadca99043a6e78b04a0919ecdfd1cc08a07597b..1094bd14d4e1c75021c438d473d732cd5a9c7d4b 100644 (file)
--- 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 4d8a7a65ff4778dc65b856eff763667747c51207..568fec3ce93997da9a42c62a3810f87903a778e6 100644 (file)
--- 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 (file)
index 0000000..991aa59
--- /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)