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

10 files changed, 97 insertions, 23 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
diff --git a/src/api/java/io/github/cvc5/api/Solver.java b/src/api/java/io/github/cvc5/api/Solver.java
index 09ad66f5b..16220228c 100644
--- a/src/api/java/io/github/cvc5/api/Solver.java
+++ b/src/api/java/io/github/cvc5/api/Solver.java
@@ -851,8 +851,8 @@ public class Solver implements IPointer, AutoCloseable
   private native long mkReal(long pointer, long num, long den);
 
   /**
-   * Create a regular expression empty term.
-   * @return the empty term
+   * Create a regular expression none (re.none) term.
+   * @return the none term
    */
   public Term mkRegexpNone()
   {
@@ -863,8 +863,20 @@ public class Solver implements IPointer, AutoCloseable
   private native long mkRegexpNone(long pointer);
 
   /**
-   * Create a regular expression sigma term.
-   * @return the sigma term
+   * Create a regular expression all (re.all) term.
+   * @return the all term
+   */
+  public Term mkRegexpAll()
+  {
+    long termPointer = mkRegexpAll(pointer);
+    return new Term(this, termPointer);
+  }
+
+  private native long mkRegexpAll(long pointer);
+
+  /**
+   * Create a regular expression allchar (re.allchar) term.
+   * @return the allchar term
    */
   public Term mkRegexpAllchar()
   {
diff --git a/src/api/java/jni/solver.cpp b/src/api/java/jni/solver.cpp
index a3ce49f4e..2e4404362 100644
--- a/src/api/java/jni/solver.cpp
+++ b/src/api/java/jni/solver.cpp
@@ -992,6 +992,21 @@ JNIEXPORT jlong JNICALL Java_io_github_cvc5_api_Solver_mkRegexpNone(
 
 /*
  * Class:     io_github_cvc5_api_Solver
+ * Method:    mkRegexpAll
+ * Signature: (J)J
+ */
+JNIEXPORT jlong JNICALL
+Java_io_github_cvc5_api_Solver_mkRegexpAll(JNIEnv* env, jobject, jlong pointer)
+{
+  CVC5_JAVA_API_TRY_CATCH_BEGIN;
+  Solver* solver = reinterpret_cast<Solver*>(pointer);
+  Term* retPointer = new Term(solver->mkRegexpAll());
+  return reinterpret_cast<jlong>(retPointer);
+  CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, 0);
+}
+
+/*
+ * Class:     io_github_cvc5_api_Solver
  * Method:    mkRegexpAllchar
  * Signature: (J)J
  */
diff --git a/src/api/python/cvc5.pxd b/src/api/python/cvc5.pxd
index baee5899e..9dae7da96 100644
--- a/src/api/python/cvc5.pxd
+++ b/src/api/python/cvc5.pxd
@@ -215,8 +215,9 @@ cdef extern from "api/cpp/cvc5.h" namespace "cvc5::api":
         Term mkInteger(const uint64_t i) except +
         Term mkInteger(const string& s) except +
         Term mkReal(const string& s) except +
-        Term mkRegexpNone() except +
+        Term mkRegexpAll() except +
         Term mkRegexpAllchar() except +
+        Term mkRegexpNone() except +
         Term mkEmptySet(Sort s) except +
         Term mkEmptyBag(Sort s) except +
         Term mkSepEmp() except +
diff --git a/src/api/python/cvc5.pxi b/src/api/python/cvc5.pxi
index 9e1aeaca1..1df252e86 100644
--- a/src/api/python/cvc5.pxi
+++ b/src/api/python/cvc5.pxi
@@ -1130,24 +1130,33 @@ cdef class Solver:
             term.cterm = self.csolver.mkReal("{}/{}".format(val, den).encode())
         return term
 
-    def mkRegexpNone(self):
-        """Create a regular expression empty term.
+    def mkRegexpAll(self):
+        """Create a regular expression all (re.all) term.
 
-        :return: the empty term
+        :return: the all term
         """
         cdef Term term = Term(self)
-        term.cterm = self.csolver.mkRegexpNone()
+        term.cterm = self.csolver.mkRegexpAll()
         return term
 
     def mkRegexpAllchar(self):
-        """Create a regular expression sigma term.
+        """Create a regular expression allchar (re.allchar) term.
 
-        :return: the sigma term
+        :return: the allchar term
         """
         cdef Term term = Term(self)
         term.cterm = self.csolver.mkRegexpAllchar()
         return term
 
+    def mkRegexpNone(self):
+        """Create a regular expression none (re.none) term.
+
+        :return: the none term
+        """
+        cdef Term term = Term(self)
+        term.cterm = self.csolver.mkRegexpNone()
+        return term
+
     def mkEmptySet(self, Sort s):
         """Create a constant representing an empty set of the given sort.
 
diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp
index 1fc7a637f..b4f39a315 100644
--- a/src/parser/smt2/smt2.cpp
+++ b/src/parser/smt2/smt2.cpp
@@ -145,9 +145,7 @@ void Smt2::addDatatypesOperators()
 }
 
 void Smt2::addStringOperators() {
-  defineVar(
-      "re.all",
-      getSolver()->mkTerm(api::REGEXP_STAR, getSolver()->mkRegexpAllchar()));
+  defineVar("re.all", getSolver()->mkRegexpAll());
   addOperator(api::STRING_CONCAT, "str.++");
   addOperator(api::STRING_LENGTH, "str.len");
   addOperator(api::STRING_SUBSTR, "str.substr");
diff --git a/test/unit/api/cpp/solver_black.cpp b/test/unit/api/cpp/solver_black.cpp
index 37aed63be..51a0f38b5 100644
--- a/test/unit/api/cpp/solver_black.cpp
+++ b/test/unit/api/cpp/solver_black.cpp
@@ -595,12 +595,11 @@ TEST_F(TestApiBlackSolver, mkReal)
   ASSERT_NO_THROW(d_solver.mkReal(val4, val4));
 }
 
-TEST_F(TestApiBlackSolver, mkRegexpNone)
+TEST_F(TestApiBlackSolver, mkRegexpAll)
 {
   Sort strSort = d_solver.getStringSort();
   Term s = d_solver.mkConst(strSort, "s");
-  ASSERT_NO_THROW(
-      d_solver.mkTerm(STRING_IN_REGEXP, s, d_solver.mkRegexpNone()));
+  ASSERT_NO_THROW(d_solver.mkTerm(STRING_IN_REGEXP, s, d_solver.mkRegexpAll()));
 }
 
 TEST_F(TestApiBlackSolver, mkRegexpAllchar)
@@ -611,6 +610,14 @@ TEST_F(TestApiBlackSolver, mkRegexpAllchar)
       d_solver.mkTerm(STRING_IN_REGEXP, s, d_solver.mkRegexpAllchar()));
 }
 
+TEST_F(TestApiBlackSolver, mkRegexpNone)
+{
+  Sort strSort = d_solver.getStringSort();
+  Term s = d_solver.mkConst(strSort, "s");
+  ASSERT_NO_THROW(
+      d_solver.mkTerm(STRING_IN_REGEXP, s, d_solver.mkRegexpNone()));
+}
+
 TEST_F(TestApiBlackSolver, mkSepEmp) { ASSERT_NO_THROW(d_solver.mkSepEmp()); }
 
 TEST_F(TestApiBlackSolver, mkSepNil)
diff --git a/test/unit/api/java/SolverTest.java b/test/unit/api/java/SolverTest.java
index 161854421..6a08d79c6 100644
--- a/test/unit/api/java/SolverTest.java
+++ b/test/unit/api/java/SolverTest.java
@@ -639,6 +639,13 @@ class SolverTest
     assertDoesNotThrow(() -> d_solver.mkTerm(STRING_IN_REGEXP, s, d_solver.mkRegexpNone()));
   }
 
+  @Test void mkRegexpAll()
+  {
+    Sort strSort = d_solver.getStringSort();
+    Term s = d_solver.mkConst(strSort, "s");
+    assertDoesNotThrow(() -> d_solver.mkTerm(STRING_IN_REGEXP, s, d_solver.mkRegexpAll()));
+  }
+
   @Test void mkRegexpAllchar()
   {
     Sort strSort = d_solver.getStringSort();
diff --git a/test/unit/api/python/test_solver.py b/test/unit/api/python/test_solver.py
index 71ab17465..89e99bd9e 100644
--- a/test/unit/api/python/test_solver.py
+++ b/test/unit/api/python/test_solver.py
@@ -643,13 +643,19 @@ def test_mk_real(solver):
     solver.mkReal(val4, val4)
 
 
-def test_mk_regexp_empty(solver):
+def test_mk_regexp_none(solver):
     strSort = solver.getStringSort()
     s = solver.mkConst(strSort, "s")
     solver.mkTerm(kinds.StringInRegexp, s, solver.mkRegexpNone())
 
 
-def test_mk_regexp_sigma(solver):
+def test_mk_regexp_all(solver):
+    strSort = solver.getStringSort()
+    s = solver.mkConst(strSort, "s")
+    solver.mkTerm(kinds.StringInRegexp, s, solver.mkRegexpAll())
+
+
+def test_mk_regexp_allchar(solver):
     strSort = solver.getStringSort()
     s = solver.mkConst(strSort, "s")
     solver.mkTerm(kinds.StringInRegexp, s, solver.mkRegexpAllchar())