Add rewrites for str.contains + str.replace/substr (#2496)

1 files changed, 64 insertions, 0 deletions

diff --git a/src/theory/strings/theory_strings_rewriter.cpp b/src/theory/strings/theory_strings_rewriter.cpp
index dd280f52c..7803224c6 100644
--- a/src/theory/strings/theory_strings_rewriter.cpp
+++ b/src/theory/strings/theory_strings_rewriter.cpp
@@ -1584,6 +1584,35 @@ Node TheoryStringsRewriter::rewriteContains( Node node ) {
           return returnRewrite(node, res, "ctn-rpl-non-ctn");
         }
       }
+
+      // (str.contains x (str.++ w (str.replace x y x) z)) --->
+      //   (and (= w "") (= x (str.replace x y x)) (= z ""))
+      if (node[0] == n[0] && node[0] == n[2])
+      {
+        Node ret;
+        if (nc2.size() > 1)
+        {
+          Node emp = nm->mkConst(CVC4::String(""));
+          NodeBuilder<> nb(kind::AND);
+          for (const Node& n2 : nc2)
+          {
+            if (n2 == n)
+            {
+              nb << nm->mkNode(kind::EQUAL, node[0], node[1]);
+            }
+            else
+            {
+              nb << nm->mkNode(kind::EQUAL, emp, n2);
+            }
+          }
+          ret = nb.constructNode();
+        }
+        else
+        {
+          ret = nm->mkNode(kind::EQUAL, node[0], node[1]);
+        }
+        return returnRewrite(node, ret, "ctn-repl-self");
+      }
     }
   }
 
@@ -1788,6 +1817,41 @@ Node TheoryStringsRewriter::rewriteContains( Node node ) {
     }
   }
 
+  if (node[0].getKind() == kind::STRING_SUBSTR)
+  {
+    // (str.contains (str.substr x n (str.len y)) y) --->
+    //   (= (str.substr x n (str.len y)) y)
+    //
+    // TODO: generalize with over-/underapproximation to:
+    //
+    // (str.contains x y) ---> (= x y) if (<= (str.len x) (str.len y))
+    if (node[0][2] == nm->mkNode(kind::STRING_LENGTH, node[1]))
+    {
+      Node ret = nm->mkNode(kind::EQUAL, node[0], node[1]);
+      return returnRewrite(node, ret, "ctn-substr");
+    }
+  }
+
+  if (node[1].getKind() == kind::STRING_STRREPL)
+  {
+    // (str.contains x (str.replace y x y)) --->
+    //   (str.contains x y)
+    if (node[0] == node[1][1] && node[1][0] == node[1][2])
+    {
+      Node ret = nm->mkNode(kind::STRING_STRCTN, node[0], node[1][0]);
+      return returnRewrite(node, ret, "ctn-repl");
+    }
+
+    // (str.contains x (str.replace "" x y)) --->
+    //   (= "" (str.replace "" x y))
+    Node emp = nm->mkConst(CVC4::String(""));
+    if (node[0] == node[1][1] && node[1][0] == emp)
+    {
+      Node ret = nm->mkNode(kind::EQUAL, emp, node[1]);
+      return returnRewrite(node, ret, "ctn-repl-empty");
+    }
+  }
+
   Trace("strings-rewrite-nf") << "No rewrites for : " << node << std::endl;
   return node;
 }