Add `isNull` and `isUpdater` to `Sort` class of python API (#7423)

This adds two missing functions to the python API, along with tests for them. It also adds a missing test for the cpp API.

4 files changed, 27 insertions, 0 deletions

diff --git a/src/api/python/cvc5.pxd b/src/api/python/cvc5.pxd
index 08bcc956a..e458b635d 100644
--- a/src/api/python/cvc5.pxd
+++ b/src/api/python/cvc5.pxd
@@ -308,6 +308,7 @@ cdef extern from "api/cpp/cvc5.h" namespace "cvc5::api":
         bint operator>(const Sort&) except +
         bint operator<=(const Sort&) except +
         bint operator>=(const Sort&) except +
+        bint isNull() except +
         bint isBoolean() except +
         bint isInteger() except +
         bint isReal() except +
@@ -321,6 +322,7 @@ cdef extern from "api/cpp/cvc5.h" namespace "cvc5::api":
         bint isConstructor() except +
         bint isSelector() except +
         bint isTester() except +
+        bint isUpdater() except +
         bint isFunction() except +
         bint isPredicate() except +
         bint isTuple() except +
diff --git a/src/api/python/cvc5.pxi b/src/api/python/cvc5.pxi
index 6b6d391e6..2ce8efb08 100644
--- a/src/api/python/cvc5.pxi
+++ b/src/api/python/cvc5.pxi
@@ -2205,6 +2205,9 @@ cdef class Sort:
     def __hash__(self):
         return csorthash(self.csort)
 
+    def isNull(self):
+        return self.csort.isNull()
+
     def isBoolean(self):
         return self.csort.isBoolean()
 
@@ -2244,6 +2247,9 @@ cdef class Sort:
     def isTester(self):
         return self.csort.isTester()
 
+    def isUpdater(self):
+        return self.csort.isUpdater()
+
     def isFunction(self):
         return self.csort.isFunction()
 
diff --git a/test/python/unit/api/test_sort.py b/test/python/unit/api/test_sort.py
index db8cbff25..98cf76d76 100644
--- a/test/python/unit/api/test_sort.py
+++ b/test/python/unit/api/test_sort.py
@@ -60,6 +60,11 @@ def test_operators_comparison(solver):
     solver.getIntegerSort() > Sort(solver)
     solver.getIntegerSort() >= Sort(solver)
 
+def test_is_null(solver):
+   x = Sort(solver)
+   assert x.isNull()
+   x = solver.getBooleanSort()
+   assert not x.isNull()
 
 def test_is_boolean(solver):
     assert solver.getBooleanSort().isBoolean()
@@ -140,6 +145,12 @@ def test_is_tester(solver):
     assert cons_sort.isTester()
     Sort(solver).isTester()
 
+def test_is_updater(solver):
+  dt_sort = create_datatype_sort(solver)
+  dt = dt_sort.getDatatype()
+  updater_sort = dt[0][0].getUpdaterTerm().getSort()
+  assert updater_sort.isUpdater()
+  Sort(solver).isUpdater()
 
 def test_is_function(solver):
     fun_sort = solver.mkFunctionSort(solver.getRealSort(),
diff --git a/test/unit/api/sort_black.cpp b/test/unit/api/sort_black.cpp
index 1e9505ee1..d0c755cf7 100644
--- a/test/unit/api/sort_black.cpp
+++ b/test/unit/api/sort_black.cpp
@@ -61,6 +61,14 @@ TEST_F(TestApiBlackSort, operators_comparison)
   ASSERT_NO_THROW(d_solver.getIntegerSort() >= Sort());
 }
 
+TEST_F(TestApiBlackSort, isNull)
+{
+  Sort x;
+  ASSERT_TRUE(x.isNull());
+  x = d_solver.getBooleanSort();
+  ASSERT_FALSE(x.isNull());
+}
+
 TEST_F(TestApiBlackSort, isBoolean)
 {
   ASSERT_TRUE(d_solver.getBooleanSort().isBoolean());