New C++ Api: Comprehensive guards for member functions of Datatype classes. (#6141)

3 files changed, 378 insertions, 32 deletions

diff --git a/src/api/checks.h b/src/api/checks.h
index bc99825db..fe7b14653 100644
--- a/src/api/checks.h
+++ b/src/api/checks.h
@@ -1,5 +1,5 @@
 /*********************                                                        */
-/*! \file cvc4cpp.h
+/*! \file checks.h
  ** \verbatim
  ** Top contributors (to current version):
  **   Aina Niemetz
@@ -16,8 +16,8 @@
 
 #include "cvc4_public.h"
 
-#ifndef CVC5__API__CHECKS_H
-#define CVC5__API__CHECKS_H
+#ifndef CVC4__API__CHECKS_H
+#define CVC4__API__CHECKS_H
 
 namespace cvc4 {
 namespace api {
@@ -134,24 +134,75 @@ namespace api {
                 << "Invalid size of argument '" << #arg << "', expected "
 
 /**
- * Check condition 'cond' for given argument 'arg' at given index.
+ * Check condition 'cond' for the argument at given index in container 'args'.
  * Argument 'what' identifies what is being checked (e.g., "term").
  * Creates a stream to provide a message that identifies what was expected to
  * hold if condition is false.
  * Usage:
- *   CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED(<condition>, "what", <arg>, <idx>)
- *     << "message";
+ *   CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED(
+ *     <condition>, "what", <container>, <idx>) << "message";
  */
-#define CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED(cond, what, arg, idx)           \
+#define CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED(cond, what, args, idx)          \
   CVC4_PREDICT_TRUE(cond)                                                    \
   ? (void)0                                                                  \
   : OstreamVoider()                                                          \
           & CVC4ApiExceptionStream().ostream()                               \
-                << "Invalid " << what << " '" << arg << "' at index " << idx \
-                << ", expected "
+                << "Invalid " << (what) << " in '" << #args << "' at index " \
+                << (idx) << ", expected "
 
 /* -------------------------------------------------------------------------- */
-/* Solver checks.                                                             */
+/* Solver checks. */
+/* -------------------------------------------------------------------------- */
+
+/**
+ * Solver check for member functions of classes other than class Solver.
+ * Check if given solver matches the solver object this object is associated
+ * with.
+ */
+#define CVC4_API_ARG_CHECK_SOLVER(what, arg)                              \
+  CVC4_API_CHECK(this->d_solver == arg.d_solver)                          \
+      << "Given " << (what) << " is not associated with the solver this " \
+      << (what)                                                           \
+      << " is "                                                           \
+         "associated with";
+
+/* -------------------------------------------------------------------------- */
+/* Sort checks.                                                               */
+/* -------------------------------------------------------------------------- */
+
+/**
+ * Sort check for member functions of classes other than class Solver.
+ * Check if given sort is not null and associated with the solver object this
+ * Sort object is associated with.
+ */
+#define CVC4_API_CHECK_SORT(sort)            \
+  do                                         \
+  {                                          \
+    CVC4_API_ARG_CHECK_NOT_NULL(sort);       \
+    CVC4_API_ARG_CHECK_SOLVER("sort", sort); \
+  } while (0)
+
+/**
+ * Sort check for member functions of classes other than class Solver.
+ * Check if each sort in the given container of sorts is not null and
+ * associated with the solver object this Sort object is associated with.
+ */
+#define CVC4_API_CHECK_SORTS(sorts)                                            \
+  do                                                                           \
+  {                                                                            \
+    size_t i = 0;                                                              \
+    for (const auto& s : sorts)                                                \
+    {                                                                          \
+      CVC4_API_ARG_AT_INDEX_CHECK_NOT_NULL("sort", s, sorts, i);               \
+      CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED(                                    \
+          this->d_solver == s.d_solver, "sort", sorts, i)                      \
+          << "a sort associated with the solver this sort is associated with"; \
+      i += 1;                                                                  \
+    }                                                                          \
+  } while (0)
+
+/* -------------------------------------------------------------------------- */
+/* Checks for class Solver.                                                   */
 /* -------------------------------------------------------------------------- */
 
 /** Sort checks for member functions of class Solver. */
diff --git a/src/api/cvc4cpp.cpp b/src/api/cvc4cpp.cpp
index 06fe1e788..72fa55d6f 100644
--- a/src/api/cvc4cpp.cpp
+++ b/src/api/cvc4cpp.cpp
@@ -2266,22 +2266,46 @@ void DatatypeConstructorDecl::addSelector(const std::string& name,
                                           const Sort& sort)
 {
   NodeManagerScope scope(d_solver->getNodeManager());
+  CVC4_API_TRY_CATCH_BEGIN;
+  CVC4_API_CHECK_NOT_NULL;
+  CVC4_API_CHECK_SORT(sort);
   CVC4_API_ARG_CHECK_EXPECTED(!sort.isNull(), sort)
       << "non-null range sort for selector";
+  //////// all checks before this line
   d_ctor->addArg(name, *sort.d_type);
+  ////////
+  CVC4_API_TRY_CATCH_END;
 }
 
 void DatatypeConstructorDecl::addSelectorSelf(const std::string& name)
 {
   NodeManagerScope scope(d_solver->getNodeManager());
+  CVC4_API_TRY_CATCH_BEGIN;
+  CVC4_API_CHECK_NOT_NULL;
+  //////// all checks before this line
   d_ctor->addArgSelf(name);
+  ////////
+  CVC4_API_TRY_CATCH_END;
+}
+
+bool DatatypeConstructorDecl::isNull() const
+{
+  CVC4_API_TRY_CATCH_BEGIN;
+  //////// all checks before this line
+  return isNullHelper();
+  ////////
+  CVC4_API_TRY_CATCH_END;
 }
 
 std::string DatatypeConstructorDecl::toString() const
 {
+  CVC4_API_TRY_CATCH_BEGIN;
+  //////// all checks before this line
   std::stringstream ss;
   ss << *d_ctor;
   return ss.str();
+  ////////
+  CVC4_API_TRY_CATCH_END;
 }
 
 std::ostream& operator<<(std::ostream& out,
@@ -2298,6 +2322,8 @@ std::ostream& operator<<(std::ostream& out,
   return out;
 }
 
+bool DatatypeConstructorDecl::isNullHelper() const { return d_ctor == nullptr; }
+
 /* DatatypeDecl ------------------------------------------------------------- */
 
 DatatypeDecl::DatatypeDecl() : d_solver(nullptr), d_dtype(nullptr) {}
@@ -2345,37 +2371,66 @@ DatatypeDecl::~DatatypeDecl()
 void DatatypeDecl::addConstructor(const DatatypeConstructorDecl& ctor)
 {
   NodeManagerScope scope(d_solver->getNodeManager());
+  CVC4_API_TRY_CATCH_BEGIN;
   CVC4_API_CHECK_NOT_NULL;
+  CVC4_API_ARG_CHECK_NOT_NULL(ctor);
+  CVC4_API_ARG_CHECK_SOLVER("datatype constructor declaration", ctor);
+  //////// all checks before this line
   d_dtype->addConstructor(ctor.d_ctor);
+  ////////
+  CVC4_API_TRY_CATCH_END;
 }
 
 size_t DatatypeDecl::getNumConstructors() const
 {
+  CVC4_API_TRY_CATCH_BEGIN;
   CVC4_API_CHECK_NOT_NULL;
+  //////// all checks before this line
   return d_dtype->getNumConstructors();
+  ////////
+  CVC4_API_TRY_CATCH_END;
 }
 
 bool DatatypeDecl::isParametric() const
 {
+  CVC4_API_TRY_CATCH_BEGIN;
   CVC4_API_CHECK_NOT_NULL;
+  //////// all checks before this line
   return d_dtype->isParametric();
+  ////////
+  CVC4_API_TRY_CATCH_END;
 }
 
 std::string DatatypeDecl::toString() const
 {
+  CVC4_API_TRY_CATCH_BEGIN;
   CVC4_API_CHECK_NOT_NULL;
+  //////// all checks before this line
   std::stringstream ss;
   ss << *d_dtype;
   return ss.str();
+  ////////
+  CVC4_API_TRY_CATCH_END;
 }
 
 std::string DatatypeDecl::getName() const
 {
+  CVC4_API_TRY_CATCH_BEGIN;
   CVC4_API_CHECK_NOT_NULL;
+  //////// all checks before this line
   return d_dtype->getName();
+  ////////
+  CVC4_API_TRY_CATCH_END;
 }
 
-bool DatatypeDecl::isNull() const { return isNullHelper(); }
+bool DatatypeDecl::isNull() const
+{
+  CVC4_API_TRY_CATCH_BEGIN;
+  //////// all checks before this line
+  return isNullHelper();
+  ////////
+  CVC4_API_TRY_CATCH_END;
+}
 
 std::ostream& operator<<(std::ostream& out, const DatatypeDecl& dtdecl)
 {
@@ -2406,24 +2461,54 @@ DatatypeSelector::~DatatypeSelector()
   }
 }
 
-std::string DatatypeSelector::getName() const { return d_stor->getName(); }
+std::string DatatypeSelector::getName() const
+{
+  CVC4_API_TRY_CATCH_BEGIN;
+  CVC4_API_CHECK_NOT_NULL;
+  //////// all checks before this line
+  return d_stor->getName();
+  ////////
+  CVC4_API_TRY_CATCH_END;
+}
 
 Term DatatypeSelector::getSelectorTerm() const
 {
-  Term sel = Term(d_solver, d_stor->getSelector());
-  return sel;
+  CVC4_API_TRY_CATCH_BEGIN;
+  CVC4_API_CHECK_NOT_NULL;
+  //////// all checks before this line
+  return Term(d_solver, d_stor->getSelector());
+  ////////
+  CVC4_API_TRY_CATCH_END;
 }
 
 Sort DatatypeSelector::getRangeSort() const
 {
+  CVC4_API_TRY_CATCH_BEGIN;
+  CVC4_API_CHECK_NOT_NULL;
+  //////// all checks before this line
   return Sort(d_solver, d_stor->getRangeType());
+  ////////
+  CVC4_API_TRY_CATCH_END;
+}
+
+bool DatatypeSelector::isNull() const
+{
+  CVC4_API_TRY_CATCH_BEGIN;
+  //////// all checks before this line
+  return isNullHelper();
+  ////////
+  CVC4_API_TRY_CATCH_END;
 }
 
 std::string DatatypeSelector::toString() const
 {
+  CVC4_API_TRY_CATCH_BEGIN;
+  //////// all checks before this line
   std::stringstream ss;
   ss << *d_stor;
   return ss.str();
+  ////////
+  CVC4_API_TRY_CATCH_END;
 }
 
 std::ostream& operator<<(std::ostream& out, const DatatypeSelector& stor)
@@ -2432,6 +2517,8 @@ std::ostream& operator<<(std::ostream& out, const DatatypeSelector& stor)
   return out;
 }
 
+bool DatatypeSelector::isNullHelper() const { return d_stor == nullptr; }
+
 /* DatatypeConstructor ------------------------------------------------------ */
 
 DatatypeConstructor::DatatypeConstructor() : d_solver(nullptr), d_ctor(nullptr)
@@ -2456,24 +2543,38 @@ DatatypeConstructor::~DatatypeConstructor()
   }
 }
 
-std::string DatatypeConstructor::getName() const { return d_ctor->getName(); }
+std::string DatatypeConstructor::getName() const
+{
+  CVC4_API_TRY_CATCH_BEGIN;
+  CVC4_API_CHECK_NOT_NULL;
+  //////// all checks before this line
+  return d_ctor->getName();
+  ////////
+  CVC4_API_TRY_CATCH_END;
+}
 
 Term DatatypeConstructor::getConstructorTerm() const
 {
-  Term ctor = Term(d_solver, d_ctor->getConstructor());
-  return ctor;
+  CVC4_API_TRY_CATCH_BEGIN;
+  CVC4_API_CHECK_NOT_NULL;
+  //////// all checks before this line
+  return Term(d_solver, d_ctor->getConstructor());
+  ////////
+  CVC4_API_TRY_CATCH_END;
 }
 
 Term DatatypeConstructor::getSpecializedConstructorTerm(
     const Sort& retSort) const
 {
   NodeManagerScope scope(d_solver->getNodeManager());
+  CVC4_API_TRY_CATCH_BEGIN;
+  CVC4_API_CHECK_NOT_NULL;
   CVC4_API_CHECK(d_ctor->isResolved())
       << "Expected resolved datatype constructor";
   CVC4_API_CHECK(retSort.isDatatype())
       << "Cannot get specialized constructor type for non-datatype type "
       << retSort;
-  CVC4_API_TRY_CATCH_BEGIN;
+  //////// all checks before this line
 
   NodeManager* nm = d_solver->getNodeManager();
   Node ret =
@@ -2491,34 +2592,62 @@ Term DatatypeConstructor::getSpecializedConstructorTerm(
 
 Term DatatypeConstructor::getTesterTerm() const
 {
-  Term tst = Term(d_solver, d_ctor->getTester());
-  return tst;
+  CVC4_API_TRY_CATCH_BEGIN;
+  CVC4_API_CHECK_NOT_NULL;
+  //////// all checks before this line
+  return Term(d_solver, d_ctor->getTester());
+  ////////
+  CVC4_API_TRY_CATCH_END;
 }
 
 size_t DatatypeConstructor::getNumSelectors() const
 {
+  CVC4_API_TRY_CATCH_BEGIN;
+  CVC4_API_CHECK_NOT_NULL;
+  //////// all checks before this line
   return d_ctor->getNumArgs();
+  ////////
+  CVC4_API_TRY_CATCH_END;
 }
 
 DatatypeSelector DatatypeConstructor::operator[](size_t index) const
 {
+  CVC4_API_TRY_CATCH_BEGIN;
+  CVC4_API_CHECK_NOT_NULL;
+  //////// all checks before this line
   return DatatypeSelector(d_solver, (*d_ctor)[index]);
+  ////////
+  CVC4_API_TRY_CATCH_END;
 }
 
 DatatypeSelector DatatypeConstructor::operator[](const std::string& name) const
 {
+  CVC4_API_TRY_CATCH_BEGIN;
+  CVC4_API_CHECK_NOT_NULL;
+  //////// all checks before this line
   return getSelectorForName(name);
+  ////////
+  CVC4_API_TRY_CATCH_END;
 }
 
 DatatypeSelector DatatypeConstructor::getSelector(const std::string& name) const
 {
+  CVC4_API_TRY_CATCH_BEGIN;
+  CVC4_API_CHECK_NOT_NULL;
+  //////// all checks before this line
   return getSelectorForName(name);
+  ////////
+  CVC4_API_TRY_CATCH_END;
 }
 
 Term DatatypeConstructor::getSelectorTerm(const std::string& name) const
 {
-  DatatypeSelector sel = getSelector(name);
-  return sel.getSelectorTerm();
+  CVC4_API_TRY_CATCH_BEGIN;
+  CVC4_API_CHECK_NOT_NULL;
+  //////// all checks before this line
+  return getSelector(name).getSelectorTerm();
+  ////////
+  CVC4_API_TRY_CATCH_END;
 }
 
 DatatypeConstructor::const_iterator DatatypeConstructor::begin() const
@@ -2600,13 +2729,28 @@ bool DatatypeConstructor::const_iterator::operator!=(
   return d_int_stors != other.d_int_stors || d_idx != other.d_idx;
 }
 
+bool DatatypeConstructor::isNull() const
+{
+  CVC4_API_TRY_CATCH_BEGIN;
+  //////// all checks before this line
+  return isNullHelper();
+  ////////
+  CVC4_API_TRY_CATCH_END;
+}
+
 std::string DatatypeConstructor::toString() const
 {
+  CVC4_API_TRY_CATCH_BEGIN;
+  //////// all checks before this line
   std::stringstream ss;
   ss << *d_ctor;
   return ss.str();
+  ////////
+  CVC4_API_TRY_CATCH_END;
 }
 
+bool DatatypeConstructor::isNullHelper() const { return d_ctor == nullptr; }
+
 DatatypeSelector DatatypeConstructor::getSelectorForName(
     const std::string& name) const
 {
@@ -2664,48 +2808,153 @@ Datatype::~Datatype()
 
 DatatypeConstructor Datatype::operator[](size_t idx) const
 {
+  CVC4_API_TRY_CATCH_BEGIN;
+  CVC4_API_CHECK_NOT_NULL;
   CVC4_API_CHECK(idx < getNumConstructors()) << "Index out of bounds.";
+  //////// all checks before this line
   return DatatypeConstructor(d_solver, (*d_dtype)[idx]);
+  ////////
+  CVC4_API_TRY_CATCH_END;
 }
 
 DatatypeConstructor Datatype::operator[](const std::string& name) const
 {
+  CVC4_API_TRY_CATCH_BEGIN;
+  CVC4_API_CHECK_NOT_NULL;
+  //////// all checks before this line
   return getConstructorForName(name);
+  ////////
+  CVC4_API_TRY_CATCH_END;
 }
 
 DatatypeConstructor Datatype::getConstructor(const std::string& name) const
 {
+  CVC4_API_TRY_CATCH_BEGIN;
+  CVC4_API_CHECK_NOT_NULL;
+  //////// all checks before this line
   return getConstructorForName(name);
+  ////////
+  CVC4_API_TRY_CATCH_END;
 }
 
 Term Datatype::getConstructorTerm(const std::string& name) const
 {
-  DatatypeConstructor ctor = getConstructor(name);
-  return ctor.getConstructorTerm();
+  CVC4_API_TRY_CATCH_BEGIN;
+  CVC4_API_CHECK_NOT_NULL;
+  //////// all checks before this line
+  return getConstructor(name).getConstructorTerm();
+  ////////
+  CVC4_API_TRY_CATCH_END;
 }
 
-std::string Datatype::getName() const { return d_dtype->getName(); }
+std::string Datatype::getName() const
+{
+  CVC4_API_TRY_CATCH_BEGIN;
+  CVC4_API_CHECK_NOT_NULL;
+  //////// all checks before this line
+  return d_dtype->getName();
+  ////////
+  CVC4_API_TRY_CATCH_END;
+}
 
 size_t Datatype::getNumConstructors() const
 {
+  CVC4_API_TRY_CATCH_BEGIN;
+  CVC4_API_CHECK_NOT_NULL;
+  //////// all checks before this line
   return d_dtype->getNumConstructors();
+  ////////
+  CVC4_API_TRY_CATCH_END;
 }
 
-bool Datatype::isParametric() const { return d_dtype->isParametric(); }
-bool Datatype::isCodatatype() const { return d_dtype->isCodatatype(); }
+bool Datatype::isParametric() const
+{
+  CVC4_API_TRY_CATCH_BEGIN;
+  CVC4_API_CHECK_NOT_NULL;
+  //////// all checks before this line
+  return d_dtype->isParametric();
+  ////////
+  CVC4_API_TRY_CATCH_END;
+}
 
-bool Datatype::isTuple() const { return d_dtype->isTuple(); }
+bool Datatype::isCodatatype() const
+{
+  CVC4_API_TRY_CATCH_BEGIN;
+  CVC4_API_CHECK_NOT_NULL;
+  //////// all checks before this line
+  return d_dtype->isCodatatype();
+  ////////
+  CVC4_API_TRY_CATCH_END;
+}
+
+bool Datatype::isTuple() const
+{
+  CVC4_API_TRY_CATCH_BEGIN;
+  CVC4_API_CHECK_NOT_NULL;
+  //////// all checks before this line
+  return d_dtype->isTuple();
+  ////////
+  CVC4_API_TRY_CATCH_END;
+}
+
+bool Datatype::isRecord() const
+{
+  CVC4_API_TRY_CATCH_BEGIN;
+  CVC4_API_CHECK_NOT_NULL;
+  //////// all checks before this line
+  return d_dtype->isRecord();
+  ////////
+  CVC4_API_TRY_CATCH_END;
+}
 
-bool Datatype::isRecord() const { return d_dtype->isRecord(); }
+bool Datatype::isFinite() const
+{
+  CVC4_API_TRY_CATCH_BEGIN;
+  CVC4_API_CHECK_NOT_NULL;
+  //////// all checks before this line
+  return d_dtype->isFinite();
+  ////////
+  CVC4_API_TRY_CATCH_END;
+}
 
-bool Datatype::isFinite() const { return d_dtype->isFinite(); }
-bool Datatype::isWellFounded() const { return d_dtype->isWellFounded(); }
+bool Datatype::isWellFounded() const
+{
+  CVC4_API_TRY_CATCH_BEGIN;
+  CVC4_API_CHECK_NOT_NULL;
+  //////// all checks before this line
+  return d_dtype->isWellFounded();
+  ////////
+  CVC4_API_TRY_CATCH_END;
+}
 bool Datatype::hasNestedRecursion() const
 {
+  CVC4_API_TRY_CATCH_BEGIN;
+  CVC4_API_CHECK_NOT_NULL;
+  //////// all checks before this line
   return d_dtype->hasNestedRecursion();
+  ////////
+  CVC4_API_TRY_CATCH_END;
+}
+
+bool Datatype::isNull() const
+{
+  CVC4_API_TRY_CATCH_BEGIN;
+  CVC4_API_CHECK_NOT_NULL;
+  //////// all checks before this line
+  return isNullHelper();
+  ////////
+  CVC4_API_TRY_CATCH_END;
 }
 
-std::string Datatype::toString() const { return d_dtype->getName(); }
+std::string Datatype::toString() const
+{
+  CVC4_API_TRY_CATCH_BEGIN;
+  CVC4_API_CHECK_NOT_NULL;
+  //////// all checks before this line
+  return d_dtype->getName();
+  ////////
+  CVC4_API_TRY_CATCH_END;
+}
 
 Datatype::const_iterator Datatype::begin() const
 {
@@ -2811,6 +3060,8 @@ bool Datatype::const_iterator::operator!=(
   return d_int_ctors != other.d_int_ctors || d_idx != other.d_idx;
 }
 
+bool Datatype::isNullHelper() const { return d_dtype == nullptr; }
+
 /* -------------------------------------------------------------------------- */
 /* Grammar                                                                    */
 /* -------------------------------------------------------------------------- */
diff --git a/src/api/cvc4cpp.h b/src/api/cvc4cpp.h
index 968ed0522..5a1a75024 100644
--- a/src/api/cvc4cpp.h
+++ b/src/api/cvc4cpp.h
@@ -1412,6 +1412,11 @@ class CVC4_PUBLIC DatatypeConstructorDecl
   void addSelectorSelf(const std::string& name);
 
   /**
+   * @return true if this DatatypeConstructorDecl is a null declaration.
+   */
+  bool isNull() const;
+
+  /**
    * @return a string representation of this datatype constructor declaration
    */
   std::string toString() const;
@@ -1426,6 +1431,12 @@ class CVC4_PUBLIC DatatypeConstructorDecl
   DatatypeConstructorDecl(const Solver* slv, const std::string& name);
 
   /**
+   * Helper for isNull checks. This prevents calling an API function with
+   * CVC4_API_CHECK_NOT_NULL
+   */
+  bool isNullHelper() const;
+
+  /**
    * The associated solver object.
    */
   const Solver* d_solver;
@@ -1577,6 +1588,11 @@ class CVC4_PUBLIC DatatypeSelector
   Sort getRangeSort() const;
 
   /**
+   * @return true if this DatatypeSelector is a null object
+   */
+  bool isNull() const;
+
+  /**
    * @return a string representation of this datatype selector
    */
   std::string toString() const;
@@ -1591,6 +1607,12 @@ class CVC4_PUBLIC DatatypeSelector
   DatatypeSelector(const Solver* slv, const CVC4::DTypeSelector& stor);
 
   /**
+   * Helper for isNull checks. This prevents calling an API function with
+   * CVC4_API_CHECK_NOT_NULL
+   */
+  bool isNullHelper() const;
+
+  /**
    * The associated solver object.
    */
   const Solver* d_solver;
@@ -1689,6 +1711,11 @@ class CVC4_PUBLIC DatatypeConstructor
   Term getSelectorTerm(const std::string& name) const;
 
   /**
+   * @return true if this DatatypeConstructor is a null object
+   */
+  bool isNull() const;
+
+  /**
    * @return a string representation of this datatype constructor
    */
   std::string toString() const;
@@ -1806,6 +1833,12 @@ class CVC4_PUBLIC DatatypeConstructor
   DatatypeSelector getSelectorForName(const std::string& name) const;
 
   /**
+   * Helper for isNull checks. This prevents calling an API function with
+   * CVC4_API_CHECK_NOT_NULL
+   */
+  bool isNullHelper() const;
+
+  /**
    * The associated solver object.
    */
   const Solver* d_solver;
@@ -1902,6 +1935,11 @@ class CVC4_PUBLIC Datatype
   bool hasNestedRecursion() const;
 
   /**
+   * @return true if this Datatype is a null object
+   */
+  bool isNull() const;
+
+  /**
    * @return a string representation of this datatype
    */
   std::string toString() const;
@@ -2016,6 +2054,12 @@ class CVC4_PUBLIC Datatype
   DatatypeConstructor getConstructorForName(const std::string& name) const;
 
   /**
+   * Helper for isNull checks. This prevents calling an API function with
+   * CVC4_API_CHECK_NOT_NULL
+   */
+  bool isNullHelper() const;
+
+  /**
    * The associated solver object.
    */
   const Solver* d_solver;