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.

2 files changed, 71 insertions, 1 deletions

diff --git a/test/python/unit/api/test_datatype_api.py b/test/python/unit/api/test_datatype_api.py
index 24a47bd76..d8a4c26f7 100644
--- 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 f82e722d3..745abc17c 100644
--- 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