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.

diff --git a/src/api/python/cvc5.pxd b/src/api/python/cvc5.pxd
index 08bcc956a135802b2a4609afb615e9c13d60ed5c..e458b635df1a65f8a11e5d1974127f325d9072c5 100644 (file)
--- 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 6b6d391e6e62d1fa8c61c74580b90b85a915302f..2ce8efb087503dc69081195dea9a5e35081086a9 100644 (file)
--- 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 db8cbff25771575bf57c633ad9fbfa8678a4c60c..98cf76d762f3c7a2899e29ccf2ba9b1ef2764363 100644 (file)
--- 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 1e9505ee18b4b6438f17b2b50bb83d71428f82f7..d0c755cf76c7ff520fa14acb9c8b82f1d3476881 100644 (file)
--- 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());