Use str.indexof in str.replace reductionstringReplaceUsingIndexOf

1 files changed, 8 insertions, 18 deletions

diff --git a/src/theory/strings/theory_strings_preprocess.cpp b/src/theory/strings/theory_strings_preprocess.cpp
index 1cc0736fb..70320ab83 100644
--- a/src/theory/strings/theory_strings_preprocess.cpp
+++ b/src/theory/strings/theory_strings_preprocess.cpp
@@ -482,24 +482,14 @@ Node StringsPreprocess::reduce(Node t,
 
     // contains( x, y )
     Node cond2 = nm->mkNode(kind::STRING_STRCTN, x, y);
-    // x = str.++( rp1, y, rp2 )
-    Node c21 = x.eqNode(nm->mkNode(kind::STRING_CONCAT, rp1, y, rp2));
+
+    Node idx = nm->mkNode(kind::STRING_STRIDOF, x, y, zero);
+    Node pfx = nm->mkNode(kind::STRING_SUBSTR, x, zero, idx);
+    Node end = nm->mkNode(kind::PLUS, idx, nm->mkNode(kind::STRING_LENGTH, y));
+    Node sfxLen = nm->mkNode(kind::MINUS, nm->mkNode(kind::STRING_LENGTH, x), end);
+    Node sfx = nm->mkNode(kind::STRING_SUBSTR, x, end, sfxLen);
     // rpw = str.++( rp1, z, rp2 )
-    Node c22 = rpw.eqNode(nm->mkNode(kind::STRING_CONCAT, rp1, z, rp2));
-    // ~contains( str.++( rp1, substr( y, 0, len(y)-1 ) ), y )
-    Node c23 =
-        nm->mkNode(kind::STRING_STRCTN,
-                   nm->mkNode(
-                       kind::STRING_CONCAT,
-                       rp1,
-                       nm->mkNode(kind::STRING_SUBSTR,
-                                  y,
-                                  zero,
-                                  nm->mkNode(kind::MINUS,
-                                             nm->mkNode(kind::STRING_LENGTH, y),
-                                             one))),
-                   y)
-            .negate();
+    Node eq = rpw.eqNode(nm->mkNode(kind::STRING_CONCAT, pfx, z, sfx));
 
     // assert:
     //   IF    y=""
@@ -515,7 +505,7 @@ Node StringsPreprocess::reduce(Node t,
                          c1,
                          nm->mkNode(kind::ITE,
                                     cond2,
-                                    nm->mkNode(kind::AND, c21, c22, c23),
+                                    eq,
                                     rpw.eqNode(x)));
     asserts.push_back(rr);