From 3027ae937385e63582fc88247ea6b67976e72156 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Mon, 22 Nov 2021 15:43:17 -0600 Subject: [PATCH] Add rewrite for repeated re.allchar (#7681) This solves 4 more challenge Amazon benchmarks. --- src/theory/strings/rewrites.cpp | 1 + src/theory/strings/rewrites.h | 1 + src/theory/strings/sequences_rewriter.cpp | 23 +++++++++++++++++++++++ 3 files changed, 25 insertions(+) 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) { -- 2.30.2