Add REGEXP_ALL kind to API (#8264)

Previously was immediately converted to (re.* re.allchar) upon construction.

diff --git a/src/api/cpp/cvc5.cpp b/src/api/cpp/cvc5.cpp
index 0dd86f8142ee211197129f353047fb425001f342..8f5fc6566f701a1a3d8e0ed0dfde012022eebfb1 100644 (file)
--- a/src/api/cpp/cvc5.cpp
+++ b/src/api/cpp/cvc5.cpp
@@ -355,6 +355,7 @@ const static std::unordered_map<Kind, cvc5::Kind> s_kinds{
     {REGEXP_REPEAT, cvc5::Kind::REGEXP_REPEAT},
     {REGEXP_LOOP, cvc5::Kind::REGEXP_LOOP},
     {REGEXP_NONE, cvc5::Kind::REGEXP_NONE},
+    {REGEXP_ALL, cvc5::Kind::REGEXP_ALL},
     {REGEXP_ALLCHAR, cvc5::Kind::REGEXP_ALLCHAR},
     {REGEXP_COMPLEMENT, cvc5::Kind::REGEXP_COMPLEMENT},
     // maps to the same kind as the string versions
@@ -670,6 +671,7 @@ const static std::unordered_map<cvc5::Kind, Kind, cvc5::kind::KindHashFunction>
         {cvc5::Kind::REGEXP_LOOP, REGEXP_LOOP},
         {cvc5::Kind::REGEXP_LOOP_OP, REGEXP_LOOP},
         {cvc5::Kind::REGEXP_NONE, REGEXP_NONE},
+        {cvc5::Kind::REGEXP_ALL, REGEXP_ALL},
         {cvc5::Kind::REGEXP_ALLCHAR, REGEXP_ALLCHAR},
         {cvc5::Kind::REGEXP_COMPLEMENT, REGEXP_COMPLEMENT},
         {cvc5::Kind::CONST_SEQUENCE, CONST_SEQUENCE},
@@ -5160,13 +5162,14 @@ Sort Solver::mkTupleSortHelper(const std::vector<Sort>& sorts) const
 Term Solver::mkTermFromKind(Kind kind) const
 {
   CVC5_API_KIND_CHECK_EXPECTED(kind == PI || kind == REGEXP_NONE
+                                   || kind == REGEXP_ALL
                                    || kind == REGEXP_ALLCHAR || kind == SEP_EMP,
                                kind)
-      << "PI, REGEXP_NONE, REGEXP_ALLCHAR or SEP_EMP";
+      << "PI, REGEXP_NONE, REGEXP_ALL, REGEXP_ALLCHAR or SEP_EMP";
   //////// all checks before this line
   Node res;
   cvc5::Kind k = extToIntKind(kind);
-  if (kind == REGEXP_NONE || kind == REGEXP_ALLCHAR)
+  if (kind == REGEXP_NONE || kind == REGEXP_ALL || kind == REGEXP_ALLCHAR)
   {
     Assert(isDefinedIntKind(k));
     res = d_nodeMgr->mkNode(k, std::vector<Node>());
@@ -5906,9 +5909,8 @@ Term Solver::mkRegexpAll() const
 {
   CVC5_API_TRY_CATCH_BEGIN;
   //////// all checks before this line
-  Node res = d_nodeMgr->mkNode(
-      cvc5::kind::REGEXP_STAR,
-      d_nodeMgr->mkNode(cvc5::kind::REGEXP_ALLCHAR, std::vector<cvc5::Node>()));
+  Node res =
+      d_nodeMgr->mkNode(cvc5::kind::REGEXP_ALL, std::vector<cvc5::Node>());
   (void)res.getType(true); /* kick off type checking */
   return Term(this, res);
   ////////

diff --git a/src/api/cpp/cvc5_kind.h b/src/api/cpp/cvc5_kind.h
index 89a7732a8e2d61f60649fcbc7561a4132e33f4c6..24b1b5ed75e13a289642d186f6618794fc45dc65 100644 (file)
--- a/src/api/cpp/cvc5_kind.h
+++ b/src/api/cpp/cvc5_kind.h
@@ -3087,6 +3087,16 @@ enum Kind : int32_t
    *   - `Solver::mkTerm(Kind kind) const`
    */
   REGEXP_NONE,
+  /**
+   * Regexp all.
+   *
+   * Parameters: none
+   *
+   * Create with:
+   *   - `Solver::mkRegexpAll() const`
+   *   - `Solver::mkTerm(Kind kind) const`
+   */
+  REGEXP_ALL,
   /**
    * Regexp all characters.
    *

diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp
index 1ca7893c02b601332f984c32bdc2b1e66b09ffe4..72d303be870e3a28f4e11210c5185c27cb84920c 100644 (file)
--- a/src/printer/smt2/smt2_printer.cpp
+++ b/src/printer/smt2/smt2_printer.cpp
@@ -1246,6 +1246,7 @@ std::string Smt2Printer::smtKindString(Kind k, Variant v)
   case kind::STRING_IN_REGEXP: return "str.in_re";
   case kind::STRING_TO_REGEXP: return "str.to_re";
   case kind::REGEXP_NONE: return "re.none";
+  case kind::REGEXP_ALL: return "re.all";
   case kind::REGEXP_ALLCHAR: return "re.allchar";
   case kind::REGEXP_CONCAT: return "re.++";
   case kind::REGEXP_UNION: return "re.union";

diff --git a/src/theory/strings/kinds b/src/theory/strings/kinds
index 0a17eed02853cb8248e91309e3b1425eb8871d34..ff226202bf8c346b52f93c5f565152579246ac4e 100644 (file)
--- a/src/theory/strings/kinds
+++ b/src/theory/strings/kinds
@@ -112,6 +112,7 @@ operator REGEXP_RANGE 2 "regexp range"
 operator REGEXP_COMPLEMENT 1 "regexp complement"
 
 operator REGEXP_NONE 0 "regexp empty"
+operator REGEXP_ALL 0 "regexp all"
 operator REGEXP_ALLCHAR 0 "regexp all characters"
 
 constant REGEXP_REPEAT_OP \
@@ -152,6 +153,7 @@ typerule REGEXP_COMPLEMENT "SimpleTypeRule<RRegExp, ARegExp>"
 typerule STRING_TO_REGEXP ::cvc5::theory::strings::StringToRegExpTypeRule
 typerule STRING_IN_REGEXP "SimpleTypeRule<RBool, AString, ARegExp>"
 typerule REGEXP_NONE "SimpleTypeRule<RRegExp>"
+typerule REGEXP_ALL "SimpleTypeRule<RRegExp>"
 typerule REGEXP_ALLCHAR "SimpleTypeRule<RRegExp>"
 
 # we return isConst for some regular expressions, including all that we enumerate

diff --git a/src/theory/strings/rewrites.cpp b/src/theory/strings/rewrites.cpp
index 98420faaac3b55d255ca3826d933dfe7e5e76df1..5ef742e9d294f2ed3945eef1e26044c65920c8a6 100644 (file)
--- a/src/theory/strings/rewrites.cpp
+++ b/src/theory/strings/rewrites.cpp
@@ -73,6 +73,7 @@ const char* toString(Rewrite r)
     case Rewrite::INDEXOF_RE_INVALID_INDEX: return "INDEXOF_RE_INVALID_INDEX";
     case Rewrite::INDEXOF_RE_MAX_INDEX: return "INDEXOF_RE_MAX_INDEX";
     case Rewrite::ITOS_EVAL: return "ITOS_EVAL";
+    case Rewrite::RE_ALL_ELIM: return "RE_ALL_ELIM";
     case Rewrite::RE_AND_EMPTY: return "RE_AND_EMPTY";
     case Rewrite::RE_ANDOR_FLATTEN: return "RE_ANDOR_FLATTEN";
     case Rewrite::RE_ANDOR_INC_CONFLICT: return "RE_ANDOR_INC_CONFLICT";

diff --git a/src/theory/strings/rewrites.h b/src/theory/strings/rewrites.h
index de8af0b4b7ddbc76fcc8c2088cadcc7cb9a6894a..ea41450e9905348e38c58d192d91c6cb0d6b8b05 100644 (file)
--- a/src/theory/strings/rewrites.h
+++ b/src/theory/strings/rewrites.h
@@ -78,6 +78,7 @@ enum class Rewrite : uint32_t
   INDEXOF_RE_INVALID_INDEX,
   INDEXOF_RE_MAX_INDEX,
   ITOS_EVAL,
+  RE_ALL_ELIM,
   RE_AND_EMPTY,
   RE_ANDOR_FLATTEN,
   RE_ANDOR_INC_CONFLICT,

diff --git a/src/theory/strings/sequences_rewriter.cpp b/src/theory/strings/sequences_rewriter.cpp
index cf2df47343b7efbcce87865bdaa910edab53b9c2..606241c0ac9b1b106b25d357c9f416f450400b25 100644 (file)
--- a/src/theory/strings/sequences_rewriter.cpp
+++ b/src/theory/strings/sequences_rewriter.cpp
@@ -757,6 +757,15 @@ Node SequencesRewriter::rewriteConcat(Node node)
   return node;
 }
 
+Node SequencesRewriter::rewriteAllRegExp(TNode node)
+{
+  Assert(node.getKind() == kind::REGEXP_ALL);
+  NodeManager* nm = NodeManager::currentNM();
+  // re.all ----> (re.* re.allchar)
+  Node ret = nm->mkNode(REGEXP_STAR, nm->mkNode(REGEXP_ALLCHAR));
+  return returnRewrite(node, ret, Rewrite::RE_ALL_ELIM);
+}
+
 Node SequencesRewriter::rewriteConcatRegExp(TNode node)
 {
   Assert(node.getKind() == kind::REGEXP_CONCAT);
@@ -1655,6 +1664,10 @@ RewriteResponse SequencesRewriter::postRewrite(TNode node)
   {
     retNode = rewriteMembership(node);
   }
+  else if (nk == REGEXP_ALL)
+  {
+    retNode = rewriteAllRegExp(node);
+  }
   else if (nk == REGEXP_CONCAT)
   {
     retNode = rewriteConcatRegExp(node);

diff --git a/src/theory/strings/sequences_rewriter.h b/src/theory/strings/sequences_rewriter.h
index 850acfb2a46c3327a277c90d294dc6aaddc2aa0c..f988a94609ee81c44088d47a477e1df6ffb49e4b 100644 (file)
--- a/src/theory/strings/sequences_rewriter.h
+++ b/src/theory/strings/sequences_rewriter.h
@@ -40,6 +40,12 @@ class SequencesRewriter : public TheoryRewriter
   StringsEntail& getStringsEntail();
 
  protected:
+  /** rewrite regular expression all
+   *
+   * This is the entry point for post-rewriting applications of re.all.
+   * Returns the rewritten form of node.
+   */
+  Node rewriteAllRegExp(TNode node);
   /** rewrite regular expression concatenation
    *
    * This is the entry point for post-rewriting applications of re.++.

diff --git a/src/theory/strings/theory_strings_utils.cpp b/src/theory/strings/theory_strings_utils.cpp
index 3c6562aae3a54e6d4aa7b67143f0522ef9d807e0..9deecc921639da0e01e0575130941cf178bbbbca 100644 (file)
--- a/src/theory/strings/theory_strings_utils.cpp
+++ b/src/theory/strings/theory_strings_utils.cpp
@@ -356,11 +356,11 @@ bool isStringKind(Kind k)
 
 bool isRegExpKind(Kind k)
 {
-  return k == REGEXP_NONE || k == REGEXP_ALLCHAR || k == STRING_TO_REGEXP
-         || k == REGEXP_CONCAT || k == REGEXP_UNION || k == REGEXP_INTER
-         || k == REGEXP_STAR || k == REGEXP_PLUS || k == REGEXP_OPT
-         || k == REGEXP_RANGE || k == REGEXP_LOOP || k == REGEXP_RV
-         || k == REGEXP_COMPLEMENT;
+  return k == REGEXP_NONE || k == REGEXP_ALL || k == REGEXP_ALLCHAR
+         || k == STRING_TO_REGEXP || k == REGEXP_CONCAT || k == REGEXP_UNION
+         || k == REGEXP_INTER || k == REGEXP_STAR || k == REGEXP_PLUS
+         || k == REGEXP_OPT || k == REGEXP_RANGE || k == REGEXP_LOOP
+         || k == REGEXP_RV || k == REGEXP_COMPLEMENT;
 }
 
 TypeNode getOwnerStringType(Node n)