Rewrite simple regexp pattern to str.contains

2 files changed, 54 insertions, 4 deletions

diff --git a/src/theory/strings/theory_strings_rewriter.cpp b/src/theory/strings/theory_strings_rewriter.cpp
index f90d5bcfd..919c56f54 100644
--- a/src/theory/strings/theory_strings_rewriter.cpp
+++ b/src/theory/strings/theory_strings_rewriter.cpp
@@ -1244,6 +1244,7 @@ Node TheoryStringsRewriter::rewriteMembership(TNode node) {
     bool allSigma = true;
     bool allSigmaStrict = true;
     unsigned allSigmaMinSize = 0;
+    Node constStr;
     for (const Node& rc : r)
     {
       Assert(rc.getKind() != kind::REGEXP_EMPTY);
@@ -1255,6 +1256,18 @@ Node TheoryStringsRewriter::rewriteMembership(TNode node) {
       {
         allSigmaStrict = false;
       }
+      else if (rc.getKind() == STRING_TO_REGEXP)
+      {
+        if (constStr.isNull())
+        {
+          constStr = rc[0];
+        }
+        else
+        {
+          allSigma = false;
+          break;
+        }
+      }
       else
       {
         allSigma = false;
@@ -1263,10 +1276,20 @@ Node TheoryStringsRewriter::rewriteMembership(TNode node) {
     }
     if (allSigma)
     {
-      Node num = nm->mkConst(Rational(allSigmaMinSize));
-      Node lenx = nm->mkNode(STRING_LENGTH, x);
-      retNode = nm->mkNode(allSigmaStrict ? EQUAL : GEQ, lenx, num);
-      return returnRewrite(node, retNode, "re-concat-pure-allchar");
+      if (constStr.isNull())
+      {
+        // x in re.++(_*, _, _) ---> str.len(x) >= 2
+        Node num = nm->mkConst(Rational(allSigmaMinSize));
+        Node lenx = nm->mkNode(STRING_LENGTH, x);
+        retNode = nm->mkNode(allSigmaStrict ? EQUAL : GEQ, lenx, num);
+        return returnRewrite(node, retNode, "re-concat-pure-allchar");
+      }
+      else if (allSigmaMinSize == 0)
+      {
+        // x in re.++(_*, "abc", _*) ---> str.contains(x, "abc")
+        retNode = nm->mkNode(STRING_STRCTN, x, constStr);
+        return returnRewrite(node, retNode, "re-concat-to-contains");
+      }
     }
   }else if( r.getKind()==kind::REGEXP_INTER || r.getKind()==kind::REGEXP_UNION ){
     std::vector< Node > mvec;
diff --git a/test/unit/theory/theory_strings_rewriter_white.h b/test/unit/theory/theory_strings_rewriter_white.h
index bbaa4733f..0ca5e5c15 100644
--- a/test/unit/theory/theory_strings_rewriter_white.h
+++ b/test/unit/theory/theory_strings_rewriter_white.h
@@ -1197,6 +1197,33 @@ class TheoryStringsRewriterWhite : public CxxTest::TestSuite
     }
   }
 
+  void testRewriteMembership()
+  {
+    TypeNode strType = d_nm->stringType();
+
+    std::vector<Node> vec_empty;
+    Node abc = d_nm->mkConst(::CVC4::String("ABC"));
+    Node re_abc = d_nm->mkNode(kind::STRING_TO_REGEXP, abc);
+    Node x = d_nm->mkVar("x", strType);
+
+    {
+      // Same normal form for:
+      //
+      // (str.in.re x (re.++ (re.* re.allchar) (str.to.re "ABC") (re.*
+      // re.allchar)))
+      //
+      // (str.contains x "ABC")
+      Node sig_star = d_nm->mkNode(kind::REGEXP_STAR,
+                                   d_nm->mkNode(kind::REGEXP_SIGMA, vec_empty));
+      Node lhs = d_nm->mkNode(
+          kind::STRING_IN_REGEXP,
+          x,
+          d_nm->mkNode(kind::REGEXP_CONCAT, sig_star, re_abc, sig_star));
+      Node rhs = d_nm->mkNode(kind::STRING_STRCTN, x, abc);
+      sameNormalForm(lhs, rhs);
+    }
+  }
+
  private:
   ExprManager* d_em;
   SmtEngine* d_smt;