From 434596534ef68bcc7c7162f16687f8827c8d8c50 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Mon, 14 Mar 2022 13:02:09 -0500 Subject: [PATCH] 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. --- src/theory/strings/rewrites.cpp | 1 + src/theory/strings/rewrites.h | 1 + src/theory/strings/sequences_rewriter.cpp | 9 +++++++++ test/regress/CMakeLists.txt | 1 + .../regress0/strings/issue8295-star-union-char.smt2 | 7 +++++++ 5 files changed, 19 insertions(+) create mode 100644 test/regress/regress0/strings/issue8295-star-union-char.smt2 diff --git a/src/theory/strings/rewrites.cpp b/src/theory/strings/rewrites.cpp index 5ef742e9d..e57a1e815 100644 --- 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 ea41450e9..cd90ecaea 100644 --- 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 606241c0a..74b053cd2 100644 --- 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 ba1ebb1af..05b16abb4 100644 --- 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 index 000000000..a11e5ae64 --- /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) -- 2.30.2