api: Add Solver::mkRegexpAll(). (#7614)

2 files changed, 23 insertions, 4 deletions

diff --git a/src/api/cpp/cvc5.cpp b/src/api/cpp/cvc5.cpp
index ae0ee2ceb..4dcfb466e 100644
--- a/src/api/cpp/cvc5.cpp
+++ b/src/api/cpp/cvc5.cpp
@@ -5796,6 +5796,19 @@ Term Solver::mkReal(int64_t num, int64_t den) const
   CVC5_API_TRY_CATCH_END;
 }
 
+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>()));
+  (void)res.getType(true); /* kick off type checking */
+  return Term(this, res);
+  ////////
+  CVC5_API_TRY_CATCH_END;
+}
+
 Term Solver::mkRegexpNone() const
 {
   CVC5_API_TRY_CATCH_BEGIN;
diff --git a/src/api/cpp/cvc5.h b/src/api/cpp/cvc5.h
index 91a6ae447..ab9a4de25 100644
--- a/src/api/cpp/cvc5.h
+++ b/src/api/cpp/cvc5.h
@@ -3443,18 +3443,24 @@ class CVC5_EXPORT Solver
   Term mkReal(int64_t num, int64_t den) const;
 
   /**
-   * Create a regular expression none (re.none) term.
-   * @return the empty term
+   * Create a regular expression all (re.all) term.
+   * @return the all term
    */
-  Term mkRegexpNone() const;
+  Term mkRegexpAll() const;
 
   /**
    * Create a regular expression allchar (re.allchar) term.
-   * @return the sigma term
+   * @return the allchar term
    */
   Term mkRegexpAllchar() const;
 
   /**
+   * Create a regular expression none (re.none) term.
+   * @return the none term
+   */
+  Term mkRegexpNone() const;
+
+  /**
    * Create a constant representing an empty set of the given sort.
    * @param sort the sort of the set elements.
    * @return the empty set constant