From b396d78982e109dc642611d32578bbca82b210cd Mon Sep 17 00:00:00 2001
From: Andres Noetzli <andres.noetzli@gmail.com>
Date: Sun, 3 Feb 2019 16:17:37 -0800
Subject: [PATCH] Add rewrite for contains + const strings replace (#2828)

---
 .../strings/theory_strings_rewriter.cpp       | 16 ++++++-
 src/util/regexp.h                             | 16 +++++++
 .../theory/theory_strings_rewriter_white.h    | 42 +++++++++++++++++++
 3 files changed, 72 insertions(+), 2 deletions(-)

diff --git a/src/theory/strings/theory_strings_rewriter.cpp b/src/theory/strings/theory_strings_rewriter.cpp
index f90d5bcfd..e8abc37a5 100644
--- a/src/theory/strings/theory_strings_rewriter.cpp
+++ b/src/theory/strings/theory_strings_rewriter.cpp
@@ -2041,8 +2041,7 @@ Node TheoryStringsRewriter::rewriteContains( Node node ) {
         if( node[0][i].isConst() ){
           CVC4::String s = node[0][i].getConst<String>();
           // if no overlap, we can split into disjunction
-          if (t.find(s) == std::string::npos && s.overlap(t) == 0
-              && t.overlap(s) == 0)
+          if (s.noOverlapWith(t))
           {
             std::vector<Node> nc0;
             getConcat(node[0], nc0);
@@ -2080,6 +2079,19 @@ Node TheoryStringsRewriter::rewriteContains( Node node ) {
   }
   else if (node[0].getKind() == kind::STRING_STRREPL)
   {
+    if (node[1].isConst() && node[0][1].isConst() && node[0][2].isConst())
+    {
+      String c = node[1].getConst<String>();
+      if (c.noOverlapWith(node[0][1].getConst<String>())
+          && c.noOverlapWith(node[0][2].getConst<String>()))
+      {
+        // (str.contains (str.replace x c1 c2) c3) ---> (str.contains x c3)
+        // if there is no overlap between c1 and c3 and none between c2 and c3
+        Node ret = nm->mkNode(STRING_STRCTN, node[0][0], node[1]);
+        return returnRewrite(node, ret, "ctn-repl-cnsts-to-ctn");
+      }
+    }
+
     if (node[0][0] == node[0][2])
     {
       // (str.contains (str.replace x y x) y) ---> (str.contains x y)
diff --git a/src/util/regexp.h b/src/util/regexp.h
index 2ab6b659c..1588b5174 100644
--- a/src/util/regexp.h
+++ b/src/util/regexp.h
@@ -149,6 +149,22 @@ class CVC4_PUBLIC String {
 
   String prefix(std::size_t i) const { return substr(0, i); }
   String suffix(std::size_t i) const { return substr(size() - i, i); }
+
+  /**
+   * Checks if there is any overlap between this string and another string. This
+   * corresponds to checking whether one string contains the other and wether a
+   * substring of one is a prefix of the other and vice-versa.
+   *
+   * @param y The other string
+   * @return True if there is an overlap, false otherwise
+   */
+  bool noOverlapWith(const String& y) const
+  {
+    return y.find(*this) == std::string::npos
+           && this->find(y) == std::string::npos && this->overlap(y) == 0
+           && y.overlap(*this) == 0;
+  }
+
   /** string overlap
   *
   * if overlap returns m>0,
diff --git a/test/unit/theory/theory_strings_rewriter_white.h b/test/unit/theory/theory_strings_rewriter_white.h
index bbaa4733f..191d0ba58 100644
--- a/test/unit/theory/theory_strings_rewriter_white.h
+++ b/test/unit/theory/theory_strings_rewriter_white.h
@@ -650,6 +650,9 @@ class TheoryStringsRewriterWhite : public CxxTest::TestSuite
     Node a = d_nm->mkConst(::CVC4::String("A"));
     Node b = d_nm->mkConst(::CVC4::String("B"));
     Node c = d_nm->mkConst(::CVC4::String("C"));
+    Node abc = d_nm->mkConst(::CVC4::String("ABC"));
+    Node def = d_nm->mkConst(::CVC4::String("DEF"));
+    Node ghi = d_nm->mkConst(::CVC4::String("GHI"));
     Node x = d_nm->mkVar("x", strType);
     Node y = d_nm->mkVar("y", strType);
     Node xy = d_nm->mkNode(kind::STRING_CONCAT, x, y);
@@ -888,6 +891,45 @@ class TheoryStringsRewriterWhite : public CxxTest::TestSuite
                               d_nm->mkNode(kind::STRING_CONCAT, b, x));
       sameNormalForm(ctn, f);
     }
+
+    {
+      // Same normal form for:
+      //
+      // (str.contains (str.replace x "ABC" "DEF") "GHI")
+      //
+      // (str.contains x "GHI")
+      lhs = d_nm->mkNode(kind::STRING_STRCTN,
+                         d_nm->mkNode(kind::STRING_STRREPL, x, abc, def),
+                         ghi);
+      rhs = d_nm->mkNode(kind::STRING_STRCTN, x, ghi);
+      sameNormalForm(lhs, rhs);
+    }
+
+    {
+      // Different normal forms for:
+      //
+      // (str.contains (str.replace x "ABC" "DEF") "B")
+      //
+      // (str.contains x "B")
+      lhs = d_nm->mkNode(kind::STRING_STRCTN,
+                         d_nm->mkNode(kind::STRING_STRREPL, x, abc, def),
+                         b);
+      rhs = d_nm->mkNode(kind::STRING_STRCTN, x, b);
+      differentNormalForms(lhs, rhs);
+    }
+
+    {
+      // Different normal forms for:
+      //
+      // (str.contains (str.replace x "B" "DEF") "ABC")
+      //
+      // (str.contains x "ABC")
+      lhs = d_nm->mkNode(kind::STRING_STRCTN,
+                         d_nm->mkNode(kind::STRING_STRREPL, x, b, def),
+                         abc);
+      rhs = d_nm->mkNode(kind::STRING_STRCTN, x, abc);
+      differentNormalForms(lhs, rhs);
+    }
   }
 
   void testInferEqsFromContains()
-- 
2.30.2