From: Andres Noetzli <andres.noetzli@gmail.com>
Date: Wed, 19 Sep 2018 15:16:46 +0000 (-0700)
Subject: Add rewrites for str.contains + str.replace/substr (#2496)
X-Git-Tag: cvc5-1.0.0~4625
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=d7f70ffac0731b7ce5a9d9115e5a5a9717d9174f;p=cvc5.git

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

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;
 }
diff --git a/test/unit/theory/theory_strings_rewriter_white.h b/test/unit/theory/theory_strings_rewriter_white.h
index 2710a60fe..99abdb5a4 100644
--- a/test/unit/theory/theory_strings_rewriter_white.h
+++ b/test/unit/theory/theory_strings_rewriter_white.h
@@ -413,6 +413,7 @@ class TheoryStringsRewriterWhite : public CxxTest::TestSuite
 
   void testRewriteContains()
   {
+    TypeNode intType = d_nm->integerType();
     TypeNode strType = d_nm->stringType();
 
     Node empty = d_nm->mkConst(::CVC4::String(""));
@@ -422,6 +423,7 @@ class TheoryStringsRewriterWhite : public CxxTest::TestSuite
     Node x = d_nm->mkVar("x", strType);
     Node y = d_nm->mkVar("y", strType);
     Node z = d_nm->mkVar("z", strType);
+    Node n = d_nm->mkVar("n", intType);
     Node one = d_nm->mkConst(Rational(2));
     Node three = d_nm->mkConst(Rational(3));
     Node four = d_nm->mkConst(Rational(4));
@@ -502,5 +504,74 @@ class TheoryStringsRewriterWhite : public CxxTest::TestSuite
                                    d_nm->mkNode(kind::EQUAL, z, empty));
     Node res_yx_cnts_xy = Rewriter::rewrite(yx_cnts_xy);
     TS_ASSERT_EQUALS(res_yx_cnts_xzy, res_yx_cnts_xy);
+
+    // Same normal form for:
+    //
+    // (str.contains (str.substr x n (str.len y)) y)
+    //
+    // (= (str.substr x n (str.len y)) y)
+    Node ctn_substr = d_nm->mkNode(
+        kind::STRING_STRCTN,
+        d_nm->mkNode(
+            kind::STRING_SUBSTR, x, n, d_nm->mkNode(kind::STRING_LENGTH, y)),
+        y);
+    Node substr_eq = d_nm->mkNode(
+        kind::EQUAL,
+        d_nm->mkNode(
+            kind::STRING_SUBSTR, x, n, d_nm->mkNode(kind::STRING_LENGTH, y)),
+        y);
+    Node res_ctn_substr = Rewriter::rewrite(ctn_substr);
+    Node res_substr_eq = Rewriter::rewrite(substr_eq);
+    TS_ASSERT_EQUALS(res_ctn_substr, res_substr_eq);
+
+    // Same normal form for:
+    //
+    // (str.contains x (str.replace y x y))
+    //
+    // (str.contains x y)
+    Node ctn_repl_y_x_y = d_nm->mkNode(
+        kind::STRING_STRCTN, x, d_nm->mkNode(kind::STRING_STRREPL, y, x, y));
+    Node ctn_x_y = d_nm->mkNode(kind::STRING_STRCTN, x, y);
+    Node res_ctn_repl_y_x_y = Rewriter::rewrite(ctn_repl_y_x_y);
+    Node res_ctn_x_y = Rewriter::rewrite(ctn_x_y);
+    TS_ASSERT_EQUALS(res_ctn_repl_y_x_y, res_ctn_x_y);
+
+    // Same normal form for:
+    //
+    // (str.contains x (str.replace x y x))
+    //
+    // (= x (str.replace x y x))
+    Node ctn_repl_self = d_nm->mkNode(
+        kind::STRING_STRCTN, x, d_nm->mkNode(kind::STRING_STRREPL, x, y, x));
+    Node eq_repl = d_nm->mkNode(
+        kind::EQUAL, x, d_nm->mkNode(kind::STRING_STRREPL, x, y, x));
+    Node res_ctn_repl_self = Rewriter::rewrite(ctn_repl_self);
+    Node res_eq_repl = Rewriter::rewrite(eq_repl);
+    TS_ASSERT_EQUALS(res_ctn_repl_self, res_eq_repl);
+
+    // (str.contains x (str.++ "A" (str.replace x y x))) ---> false
+    Node ctn_repl_self_f =
+        d_nm->mkNode(kind::STRING_STRCTN,
+                     x,
+                     d_nm->mkNode(kind::STRING_CONCAT,
+                                  a,
+                                  d_nm->mkNode(kind::STRING_STRREPL, x, y, x)));
+    Node res_ctn_repl_self_f = Rewriter::rewrite(ctn_repl_self_f);
+    TS_ASSERT_EQUALS(res_ctn_repl_self_f, f);
+
+    // Same normal form for:
+    //
+    // (str.contains x (str.replace "" x y))
+    //
+    // (= "" (str.replace "" x y))
+    Node ctn_repl_empty =
+        d_nm->mkNode(kind::STRING_STRCTN,
+                     x,
+                     d_nm->mkNode(kind::STRING_STRREPL, empty, x, y));
+    Node eq_repl_empty = d_nm->mkNode(
+        kind::EQUAL, empty, d_nm->mkNode(kind::STRING_STRREPL, empty, x, y));
+    Node res_ctn_repl_empty = Rewriter::rewrite(ctn_repl_empty);
+    Node res_eq_repl_empty = Rewriter::rewrite(eq_repl_empty);
+    TS_ASSERT_EQUALS(res_ctn_repl_empty, res_eq_repl_empty);
   }
 };