Add `isNull` to cpp api tests, python api, and python api tests (#7059)

While working on API documentation for python, I noticed that isNull is not wrapped
by the python API. It is also not tested in the cpp API tests. This PR fixes both issues,
and also updates the python api tests accordingly.

3 files changed, 20 insertions, 1 deletions

diff --git a/src/api/cpp/cvc5.cpp b/src/api/cpp/cvc5.cpp
index 12c59c0de..f85286acb 100644
--- a/src/api/cpp/cvc5.cpp
+++ b/src/api/cpp/cvc5.cpp
@@ -4169,7 +4169,6 @@ bool Datatype::hasNestedRecursion() const
 bool Datatype::isNull() const
 {
   CVC5_API_TRY_CATCH_BEGIN;
-  CVC5_API_CHECK_NOT_NULL;
   //////// all checks before this line
   return isNullHelper();
   ////////
diff --git a/src/api/python/cvc5.pxd b/src/api/python/cvc5.pxd
index ee73187ff..2665706c0 100644
--- a/src/api/python/cvc5.pxd
+++ b/src/api/python/cvc5.pxd
@@ -58,6 +58,7 @@ cdef extern from "api/cpp/cvc5.h" namespace "cvc5::api":
         bint isFinite() except +
         bint isWellFounded() except +
         bint hasNestedRecursion() except +
+        bint isNull() except +
         string toString() except +
         cppclass const_iterator:
             const_iterator() except +
@@ -80,6 +81,7 @@ cdef extern from "api/cpp/cvc5.h" namespace "cvc5::api":
         size_t getNumSelectors() except +
         DatatypeSelector getSelector(const string& name) except +
         Term getSelectorTerm(const string& name) except +
+        bint isNull() except +
         string toString() except +
         cppclass const_iterator:
             const_iterator() except +
@@ -94,6 +96,7 @@ cdef extern from "api/cpp/cvc5.h" namespace "cvc5::api":
     cdef cppclass DatatypeConstructorDecl:
         void addSelector(const string& name, Sort sort) except +
         void addSelectorSelf(const string& name) except +
+        bint isNull() except +
         string toString() except +
 
 
@@ -103,6 +106,7 @@ cdef extern from "api/cpp/cvc5.h" namespace "cvc5::api":
         bint isParametric() except +
         string toString() except +
         string getName() except +
+        bint isNull() except +
 
 
     cdef cppclass DatatypeSelector:
@@ -111,6 +115,7 @@ cdef extern from "api/cpp/cvc5.h" namespace "cvc5::api":
         Term getSelectorTerm() except +
         Term getUpdaterTerm() except +
         Sort getRangeSort() except +
+        bint isNull() except +
         string toString() except +
 
 
diff --git a/src/api/python/cvc5.pxi b/src/api/python/cvc5.pxi
index f5dca55c7..36dcc066e 100644
--- a/src/api/python/cvc5.pxi
+++ b/src/api/python/cvc5.pxi
@@ -176,6 +176,9 @@ cdef class Datatype:
         """:return: whether this datatype has nested recursion (see :cpp:func:`Datatype::hasNestedRecursion() <cvc5::api::Datatype::hasNestedRecursion>`)."""
         return self.cd.hasNestedRecursion()
 
+    def isNull(self):
+        return self.cd.isNull()
+
     def __str__(self):
         return self.cd.toString().decode()
 
@@ -237,6 +240,9 @@ cdef class DatatypeConstructor:
         term.cterm = self.cdc.getSelectorTerm(name.encode())
         return term
 
+    def isNull(self):
+        return self.cdc.isNull()
+
     def __str__(self):
         return self.cdc.toString().decode()
 
@@ -263,6 +269,9 @@ cdef class DatatypeConstructorDecl:
     def addSelectorSelf(self, str name):
         self.cddc.addSelectorSelf(name.encode())
 
+    def isNull(self):
+        return self.cddc.isNull()
+
     def __str__(self):
         return self.cddc.toString().decode()
 
@@ -288,6 +297,9 @@ cdef class DatatypeDecl:
     def getName(self):
         return self.cdd.getName().decode()
 
+    def isNull(self):
+        return self.cdd.isNull()
+
     def __str__(self):
         return self.cdd.toString().decode()
 
@@ -320,6 +332,9 @@ cdef class DatatypeSelector:
         sort.csort = self.cds.getRangeSort()
         return sort
 
+    def isNull(self):
+        return self.cds.isNull()
+
     def __str__(self):
         return self.cds.toString().decode()