Add rewrite for allchar beneath union + star (#8299)

Addresses the issue on #8295.

The re elimination module was assuming that a trivial RE was rewritten when it was not.

diff --git a/src/theory/strings/rewrites.cpp b/src/theory/strings/rewrites.cpp
index 5ef742e9d294f2ed3945eef1e26044c65920c8a6..e57a1e8156bea83280714cd54097da8ba46a9f36 100644 (file)
--- a/src/theory/strings/rewrites.cpp
+++ b/src/theory/strings/rewrites.cpp
@@ -100,6 +100,7 @@ const char* toString(Rewrite r)
     case Rewrite::RE_STAR_EMPTY_STRING: return "RE_STAR_EMPTY_STRING";
     case Rewrite::RE_STAR_NESTED_STAR: return "RE_STAR_NESTED_STAR";
     case Rewrite::RE_STAR_UNION: return "RE_STAR_UNION";
+    case Rewrite::RE_STAR_UNION_CHAR: return "RE_STAR_UNION_CHAR";
     case Rewrite::REPL_CHAR_NCONTRIB_FIND: return "REPL_CHAR_NCONTRIB_FIND";
     case Rewrite::REPL_DUAL_REPL_ITE: return "REPL_DUAL_REPL_ITE";
     case Rewrite::REPL_REPL_SHORT_CIRCUIT: return "REPL_REPL_SHORT_CIRCUIT";

diff --git a/src/theory/strings/rewrites.h b/src/theory/strings/rewrites.h
index ea41450e9905348e38c58d192d91c6cb0d6b8b05..cd90ecaead2d5405aa3f9f0fb94c095724ae8167 100644 (file)
--- a/src/theory/strings/rewrites.h
+++ b/src/theory/strings/rewrites.h
@@ -103,6 +103,7 @@ enum class Rewrite : uint32_t
   RE_STAR_EMPTY_STRING,
   RE_STAR_NESTED_STAR,
   RE_STAR_UNION,
+  RE_STAR_UNION_CHAR,
   REPL_CHAR_NCONTRIB_FIND,
   REPL_DUAL_REPL_ITE,
   REPL_REPL_SHORT_CIRCUIT,

diff --git a/src/theory/strings/sequences_rewriter.cpp b/src/theory/strings/sequences_rewriter.cpp
index 606241c0ac9b1b106b25d357c9f416f450400b25..74b053cd24054eaf026fc20777b483e063d53fc9 100644 (file)
--- a/src/theory/strings/sequences_rewriter.cpp
+++ b/src/theory/strings/sequences_rewriter.cpp
@@ -957,6 +957,15 @@ Node SequencesRewriter::rewriteStarRegExp(TNode node)
   }
   else if (node[0].getKind() == REGEXP_UNION)
   {
+    for (const Node& nc : node[0])
+    {
+      if (nc.getKind() == REGEXP_ALLCHAR)
+      {
+        // (re.* (re.union ... re.allchar ...)) ---> (re.* re.allchar)
+        retNode = nm->mkNode(REGEXP_STAR, nc);
+        return returnRewrite(node, retNode, Rewrite::RE_STAR_UNION_CHAR);
+      }
+    }
     // simplification of unions under star
     if (RegExpEntail::hasEpsilonNode(node[0]))
     {

diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index ba1ebb1af5252f4fae725e86df1ae1605f8a3655..05b16abb474aec40a6ad8b4af1138c7d0c1d12d9 100644 (file)
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -1363,6 +1363,7 @@ set(regress_0_tests
   regress0/strings/issue6681-split-eq-strip-l.smt2
   regress0/strings/issue6834-str-eq-const-nhomog.smt2
   regress0/strings/issue7974-incomplete-neg-member.smt2
+  regress0/strings/issue8295-star-union-char.smt2
   regress0/strings/itos-entail.smt2
   regress0/strings/large-model.smt2
   regress0/strings/leadingzero001.smt2

diff --git a/test/regress/regress0/strings/issue8295-star-union-char.smt2 b/test/regress/regress0/strings/issue8295-star-union-char.smt2
new file mode 100644 (file)
index 0000000..a11e5ae
--- /dev/null
+++ b/test/regress/regress0/strings/issue8295-star-union-char.smt2
@@ -0,0 +1,7 @@
+(set-logic ALL)
+(set-info :status sat)
+(set-option :re-elim-agg true)
+(set-option :re-elim true)
+(declare-fun str9 () String)
+(assert (str.in_re str9 (re.* (re.union re.allchar (str.to_re "lE")))))
+(check-sat)