From: Andres Noetzli <andres.noetzli@gmail.com>
Date: Fri, 17 Dec 2021 21:46:14 +0000 (-0800)
Subject: Fix rewrite for `str.update(str.rev(s), n, t))` (#7838)
X-Git-Tag: cvc5-1.0.0~637
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=2df0cc4257391daf6daf175826d69a735517ad19;p=cvc5.git

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 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)