From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Wed, 19 Sep 2018 01:54:13 +0000 (-0500)
Subject: Add two rewrites for string contains character (#2492)
X-Git-Tag: cvc5-1.0.0~4627
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=8ed4c0c135fcdd49a777fed1a03b378861af9757;p=cvc5.git

Add two rewrites for string contains character (#2492)
---

diff --git a/src/theory/strings/theory_strings_rewriter.cpp b/src/theory/strings/theory_strings_rewriter.cpp
index 7e5f7102d..dd280f52c 100644
--- a/src/theory/strings/theory_strings_rewriter.cpp
+++ b/src/theory/strings/theory_strings_rewriter.cpp
@@ -1495,6 +1495,45 @@ Node TheoryStringsRewriter::rewriteContains( Node node ) {
       Node ret = NodeManager::currentNM()->mkConst(true);
       return returnRewrite(node, ret, "ctn-rhs-emptystr");
     }
+    else if (t.size() == 1)
+    {
+      // The following rewrites are specific to a single character second
+      // argument of contains, where we can reason that this character is
+      // not split over multiple components in the first argument.
+      if (node[0].getKind() == STRING_CONCAT)
+      {
+        std::vector<Node> nc1;
+        getConcat(node[0], nc1);
+        NodeBuilder<> nb(OR);
+        for (const Node& ncc : nc1)
+        {
+          nb << nm->mkNode(STRING_STRCTN, ncc, node[1]);
+        }
+        Node ret = nb.constructNode();
+        // str.contains( x ++ y, "A" ) --->
+        //   str.contains( x, "A" ) OR str.contains( y, "A" )
+        return returnRewrite(node, ret, "ctn-concat-char");
+      }
+      else if (node[0].getKind() == STRING_STRREPL)
+      {
+        Node rplDomain = nm->mkNode(STRING_STRCTN, node[0][1], node[1]);
+        rplDomain = Rewriter::rewrite(rplDomain);
+        if (rplDomain.isConst() && !rplDomain.getConst<bool>())
+        {
+          Node d1 = nm->mkNode(STRING_STRCTN, node[0][0], node[1]);
+          Node d2 =
+              nm->mkNode(AND,
+                         nm->mkNode(STRING_STRCTN, node[0][0], node[0][1]),
+                         nm->mkNode(STRING_STRCTN, node[0][2], node[1]));
+          Node ret = nm->mkNode(OR, d1, d2);
+          // If str.contains( y, "A" ) ---> false, then:
+          // str.contains( str.replace( x, y, z ), "A" ) --->
+          //   str.contains( x, "A" ) OR
+          //   ( str.contains( x, y ) AND str.contains( z, "A" ) )
+          return returnRewrite(node, ret, "ctn-repl-char");
+        }
+      }
+    }
   }
   std::vector<Node> nc1;
   getConcat(node[0], nc1);