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 f73f78c24bc9656731038a69cca34c64661a7a30..4da6e5600d678d00a7065536fe7dff45212faa90 100644 (file)
--- 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 684ee0e8aacac35de0509807a63e91cfbf648ae5..c96dffcdebf47f25b600053202b2a6c63e44858b 100644 (file)
--- 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 fbb40f2123a540dd030832861074257d89401e7f..69cd790e876e9c8e21ee4dc52f775220e4284339 100644 (file)
--- 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)
   {