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.

diff --git a/src/api/cpp/cvc5.cpp b/src/api/cpp/cvc5.cpp
index 12c59c0debd133b701438692ac893c21ea7aac08..f85286acbe202a2362d0ab38e0ab30122d3f7acf 100644 (file)
--- 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 ee73187ff03b65f12dc64722dddfeb0d41365ab9..2665706c0f3d1dd45ac7c2e86c8230ec3c6a2c27 100644 (file)
--- 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 f5dca55c7fe8ca0eb6d92d7c9434ef805df28e07..36dcc066e62139310c5e80c7eeb1ac7280d97e9e 100644 (file)
--- 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()
 

diff --git a/test/python/unit/api/test_datatype_api.py b/test/python/unit/api/test_datatype_api.py
index 24a47bd761883e738fb292290bd3cddaa06b743a..d8a4c26f76c9b1025e581295a262beeb3b7a8e2f 100644 (file)
--- a/test/python/unit/api/test_datatype_api.py
+++ b/test/python/unit/api/test_datatype_api.py
@@ -14,7 +14,12 @@
 import pytest
 import pycvc5
 from pycvc5 import kinds
-from pycvc5 import Sort, Term, DatatypeDecl
+from pycvc5 import Sort, Term 
+from pycvc5 import DatatypeDecl
+from pycvc5 import Datatype
+from pycvc5 import DatatypeConstructorDecl
+from pycvc5 import DatatypeConstructor
+from pycvc5 import DatatypeSelector
 
 
 @pytest.fixture
@@ -38,6 +43,37 @@ def test_mk_datatype_sort(solver):
     consConstr.getConstructorTerm()
     nilConstr.getConstructorTerm()
 
+def test_is_null(solver):
+  # creating empty (null) objects.
+  dtypeSpec = DatatypeDecl(solver)
+  cons = DatatypeConstructorDecl(solver)
+  d = Datatype(solver)
+  consConstr = DatatypeConstructor(solver)
+  sel = DatatypeSelector(solver)
+
+  # verifying that the objects are considered null.
+  assert dtypeSpec.isNull()
+  assert cons.isNull()
+  assert d.isNull()
+  assert consConstr.isNull()
+  assert sel.isNull()
+
+  # changing the objects to be non-null
+  dtypeSpec = solver.mkDatatypeDecl("list");
+  cons = solver.mkDatatypeConstructorDecl("cons");
+  cons.addSelector("head", solver.getIntegerSort());
+  dtypeSpec.addConstructor(cons);
+  listSort = solver.mkDatatypeSort(dtypeSpec)
+  d = listSort.getDatatype();
+  consConstr = d[0];
+  sel = consConstr[0];
+
+  # verifying that the new objects are non-null
+  assert not dtypeSpec.isNull()
+  assert not cons.isNull()
+  assert not d.isNull()
+  assert not consConstr.isNull()
+  assert not sel.isNull()
 
 def test_mk_datatype_sorts(solver):
     # Create two mutual datatypes corresponding to this definition

diff --git a/test/unit/api/datatype_api_black.cpp b/test/unit/api/datatype_api_black.cpp
index f82e722d3c26cf7ccf9ab6949e2ebabc98ca7626..745abc17ca9f073c5956d4dc93a0a8440b792d27 100644 (file)
--- a/test/unit/api/datatype_api_black.cpp
+++ b/test/unit/api/datatype_api_black.cpp
@@ -42,6 +42,40 @@ TEST_F(TestApiBlackDatatype, mkDatatypeSort)
   ASSERT_NO_THROW(nilConstr.getConstructorTerm());
 }
 
+TEST_F(TestApiBlackDatatype, isNull)
+{
+  // creating empty (null) objects.
+  DatatypeDecl dtypeSpec;
+  DatatypeConstructorDecl cons;
+  Datatype d;
+  DatatypeConstructor consConstr;
+  DatatypeSelector sel;
+
+  // verifying that the objects are considered null.
+  ASSERT_TRUE(dtypeSpec.isNull());
+  ASSERT_TRUE(cons.isNull());
+  ASSERT_TRUE(d.isNull());
+  ASSERT_TRUE(consConstr.isNull());
+  ASSERT_TRUE(sel.isNull());
+
+  // changing the objects to be non-null
+  dtypeSpec = d_solver.mkDatatypeDecl("list");
+  cons = d_solver.mkDatatypeConstructorDecl("cons");
+  cons.addSelector("head", d_solver.getIntegerSort());
+  dtypeSpec.addConstructor(cons);
+  Sort listSort = d_solver.mkDatatypeSort(dtypeSpec);
+  d = listSort.getDatatype();
+  consConstr = d[0];
+  sel = consConstr[0];
+
+  // verifying that the new objects are non-null
+  ASSERT_FALSE(dtypeSpec.isNull());
+  ASSERT_FALSE(cons.isNull());
+  ASSERT_FALSE(d.isNull());
+  ASSERT_FALSE(consConstr.isNull());
+  ASSERT_FALSE(sel.isNull());
+}
+
 TEST_F(TestApiBlackDatatype, mkDatatypeSorts)
 {
   /* Create two mutual datatypes corresponding to this definition