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

diff --git a/src/theory/strings/theory_strings_rewriter.cpp b/src/theory/strings/theory_strings_rewriter.cpp
index e09eefddc8a5e828d692329c4a09594f038b974a..7e5f7102d1eb421d537b15ae030b1bff51da33d1 100644 (file)
--- 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])

diff --git a/test/regress/Makefile.tests b/test/regress/Makefile.tests
index 7f33adac1d6d7e571d3c8d6ee51abda02a3f317b..59a5b5f64737b9464bd6bfac87c27dc1d385407e 100644 (file)
--- a/test/regress/Makefile.tests
+++ b/test/regress/Makefile.tests
@@ -1686,6 +1686,7 @@ REG2_TESTS = \
        regress2/strings/cmu-prereg-fmf.smt2 \
        regress2/strings/cmu-repl-len-nterm.smt2 \
        regress2/strings/norn-dis-0707-3.smt2 \
+       regress2/strings/repl-repl.smt2 \
        regress2/sygus/MPwL_d1s3.sy \
        regress2/sygus/array_sum_dd.sy \
        regress2/sygus/cegisunif-depth1-bv.sy \

diff --git a/test/regress/regress2/strings/repl-repl.smt2 b/test/regress/regress2/strings/repl-repl.smt2
new file mode 100644 (file)
index 0000000..baa4a31
--- /dev/null
+++ b/test/regress/regress2/strings/repl-repl.smt2
@@ -0,0 +1,37 @@
+; COMMAND-LINE: --strings-exp --strings-fmf --incremental
+; EXPECT: sat
+; EXPECT: unsat
+; EXPECT: sat
+; EXPECT: sat
+; EXPECT: sat
+(set-logic SLIA)
+(declare-const x String)
+(declare-const y String)
+(declare-const z String)
+
+(push 1)
+(assert (not (= (str.replace (str.replace x "B" x) x "AB") (str.replace (str.replace x "B" "AB") x "AB"))))
+(check-sat)
+(pop 1)
+
+(push 1)
+(assert (not (= (str.replace (str.replace x "B" x) x "A") (str.replace (str.replace x "B" "A") x "A"))))
+(check-sat)
+(pop 1)
+
+(push 1)
+(assert (not (= (str.replace (str.replace x z x) x y) (str.replace (str.replace x z y) x y))))
+(check-sat)
+(pop 1)
+
+(push 1)
+(assert (not (= (str.replace (str.replace x z x) x y) (str.replace (str.replace x z y) x y))))
+(assert (<= (str.len y) (str.len z)))
+(check-sat)
+(pop 1)
+
+(push 1)
+(assert (not (= (str.replace (str.replace x z x) x y) (str.replace (str.replace x z y) x y))))
+(assert (not (= y z)))
+(check-sat)
+(pop 1)

diff --git a/test/unit/theory/theory_strings_rewriter_white.h b/test/unit/theory/theory_strings_rewriter_white.h
index 67dc205419a8ad974399d37a21af4903a52fe545..2710a60fe45c2e9b04a1eee981c9779d8db939aa 100644 (file)
--- a/test/unit/theory/theory_strings_rewriter_white.h
+++ b/test/unit/theory/theory_strings_rewriter_white.h
@@ -336,12 +336,27 @@ class TheoryStringsRewriterWhite : public CxxTest::TestSuite
     Node y = d_nm->mkVar("y", strType);
     Node z = d_nm->mkVar("z", strType);
 
-    // (str.replace "A" (str.replace "B", x, "C") "D") --> "A"
+    // (str.replace (str.replace x "B" x) x "A") -->
+    //   (str.replace (str.replace x "B" "A") x "A")
     Node repl_repl = d_nm->mkNode(kind::STRING_STRREPL,
-                                  a,
-                                  d_nm->mkNode(kind::STRING_STRREPL, b, x, c),
-                                  d);
+                                  d_nm->mkNode(kind::STRING_STRREPL, x, b, x),
+                                  x,
+                                  a);
+    Node repl_repl_short =
+        d_nm->mkNode(kind::STRING_STRREPL,
+                     d_nm->mkNode(kind::STRING_STRREPL, x, b, a),
+                     x,
+                     a);
     Node res_repl_repl = Rewriter::rewrite(repl_repl);
+    Node res_repl_repl_short = Rewriter::rewrite(repl_repl_short);
+    TS_ASSERT_EQUALS(res_repl_repl, res_repl_repl_short);
+
+    // (str.replace "A" (str.replace "B", x, "C") "D") --> "A"
+    repl_repl = d_nm->mkNode(kind::STRING_STRREPL,
+                             a,
+                             d_nm->mkNode(kind::STRING_STRREPL, b, x, c),
+                             d);
+    res_repl_repl = Rewriter::rewrite(repl_repl);
     TS_ASSERT_EQUALS(res_repl_repl, a);
 
     // (str.replace "A" (str.replace "B", x, "A") "D") -/-> "A"