Add (str.replace (str.replace y w y) y z) rewrite (#2441)

1 files changed, 51 insertions, 0 deletions

diff --git a/src/theory/strings/theory_strings_rewriter.cpp b/src/theory/strings/theory_strings_rewriter.cpp
index e09eefddc..7e5f7102d 100644
--- a/src/theory/strings/theory_strings_rewriter.cpp
+++ b/src/theory/strings/theory_strings_rewriter.cpp
@@ -2203,6 +2203,57 @@ Node TheoryStringsRewriter::rewriteReplace( Node node ) {
       return returnRewrite(node, res, "repl-subst-idx");
     }
   }
+
+  if (node[0].getKind() == STRING_STRREPL)
+  {
+    Node x = node[0];
+    Node y = node[1];
+    Node z = node[2];
+    if (x[0] == x[2] && x[0] == y)
+    {
+      // (str.replace (str.replace y w y) y z) -->
+      //   (str.replace (str.replace y w z) y z)
+      // if (str.len w) >= (str.len z) and w != z
+      //
+      // Reasoning: There are two cases: (1) w does not appear in y and (2) w
+      // does appear in y.
+      //
+      // Case (1): In this case, the reasoning is trivial. The
+      // inner replace does not do anything, so we can just replace its third
+      // argument with any string.
+      //
+      // Case (2): After the inner replace, we are guaranteed to have a string
+      // that contains y at the index of w in the original string y. The outer
+      // replace then replaces that y with z, so we can short-circuit that
+      // replace by directly replacing w with z in the inner replace. We can
+      // only do that if the result of the new inner replace does not contain
+      // y, otherwise we end up doing two replaces that are different from the
+      // original expression. We enforce that by requiring that the length of w
+      // has to be greater or equal to the length of z and that w and z have to
+      // be different. This makes sure that an inner replace changes a string
+      // to a string that is shorter than y, making it impossible for the outer
+      // replace to match.
+      Node w = x[1];
+
+      // (str.len w) >= (str.len z)
+      Node wlen = nm->mkNode(kind::STRING_LENGTH, w);
+      Node zlen = nm->mkNode(kind::STRING_LENGTH, z);
+      if (checkEntailArith(wlen, zlen))
+      {
+        // w != z
+        Node wEqZ = Rewriter::rewrite(nm->mkNode(kind::EQUAL, w, z));
+        if (wEqZ.isConst() && !wEqZ.getConst<bool>())
+        {
+          Node ret = nm->mkNode(kind::STRING_STRREPL,
+                                nm->mkNode(kind::STRING_STRREPL, y, w, z),
+                                y,
+                                z);
+          return returnRewrite(node, ret, "repl-repl-short-circuit");
+        }
+      }
+    }
+  }
+
   if (node[1].getKind() == STRING_STRREPL)
   {
     if (node[1][0] == node[0])