From 4877909b806329e5e0e14dcfc3c404b8e4f6c0af Mon Sep 17 00:00:00 2001
From: Aina Niemetz <aina.niemetz@gmail.com>
Date: Wed, 10 Nov 2021 13:10:16 -0800
Subject: api: Add Solver::mkRegexpAll(). (#7614)

---
 src/api/cpp/cvc5.cpp | 13 +++++++++++++
 1 file changed, 13 insertions(+)

(limited to 'src/api/cpp/cvc5.cpp')

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;
-- 
cgit v1.2.3