From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Mon, 22 Nov 2021 21:43:17 +0000 (-0600)
Subject: Add rewrite for repeated re.allchar (#7681)
X-Git-Tag: cvc5-1.0.0~787
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=3027ae937385e63582fc88247ea6b67976e72156;p=cvc5.git

Add rewrite for repeated re.allchar (#7681)

This solves 4 more challenge Amazon benchmarks.
---

diff --git a/src/theory/strings/rewrites.cpp b/src/theory/strings/rewrites.cpp
index f73f78c24..4da6e5600 100644
--- a/src/theory/strings/rewrites.cpp
+++ b/src/theory/strings/rewrites.cpp
@@ -89,6 +89,7 @@ const char* toString(Rewrite r)
     case Rewrite::RE_EMPTY_IN_STR_STAR: return "RE_EMPTY_IN_STR_STAR";
     case Rewrite::RE_IN_DIST_CHAR_STAR: return "RE_IN_DIST_CHAR_STAR";
     case Rewrite::RE_IN_SIGMA_STAR: return "RE_IN_SIGMA_STAR";
+    case Rewrite::RE_IN_CHAR_MODULUS_STAR: return "RE_IN_CHAR_MODULUS_STAR";
     case Rewrite::RE_LOOP: return "RE_LOOP";
     case Rewrite::RE_LOOP_STAR: return "RE_LOOP_STAR";
     case Rewrite::RE_OR_ALL: return "RE_OR_ALL";
diff --git a/src/theory/strings/rewrites.h b/src/theory/strings/rewrites.h
index 684ee0e8a..c96dffcde 100644
--- a/src/theory/strings/rewrites.h
+++ b/src/theory/strings/rewrites.h
@@ -92,6 +92,7 @@ enum class Rewrite : uint32_t
   RE_EMPTY_IN_STR_STAR,
   RE_IN_DIST_CHAR_STAR,
   RE_IN_SIGMA_STAR,
+  RE_IN_CHAR_MODULUS_STAR,
   RE_LOOP,
   RE_LOOP_STAR,
   RE_OR_ALL,
diff --git a/src/theory/strings/sequences_rewriter.cpp b/src/theory/strings/sequences_rewriter.cpp
index fbb40f212..69cd790e8 100644
--- a/src/theory/strings/sequences_rewriter.cpp
+++ b/src/theory/strings/sequences_rewriter.cpp
@@ -1362,6 +1362,29 @@ Node SequencesRewriter::rewriteMembership(TNode node)
       Node retNode = NodeManager::currentNM()->mkConst(true);
       return returnRewrite(node, retNode, Rewrite::RE_IN_SIGMA_STAR);
     }
+    else if (r[0].getKind() == REGEXP_CONCAT)
+    {
+      bool isAllchar = true;
+      for (const Node& rc : r[0])
+      {
+        if (rc.getKind() != REGEXP_ALLCHAR)
+        {
+          isAllchar = false;
+          break;
+        }
+      }
+      if (isAllchar)
+      {
+        // For example:
+        // (str.in_re x (re.* re.allchar re.allchar)) --->
+        // (= (mod (str.len x) 2) 0)
+        Node zero = nm->mkConstInt(Rational(0));
+        Node factor = nm->mkConstInt(Rational(r[0].getNumChildren()));
+        Node t = nm->mkNode(INTS_MODULUS, nm->mkNode(STRING_LENGTH, x), factor);
+        Node retNode = t.eqNode(zero);
+        return returnRewrite(node, retNode, Rewrite::RE_IN_CHAR_MODULUS_STAR);
+      }
+    }
   }
   else if (r.getKind() == kind::REGEXP_CONCAT)
   {