Add isNullHelper to avoid calling API function isNull with CVC4_API_CHECK_NOT_NULL (#3520)

1 files changed, 27 insertions, 9 deletions

diff --git a/src/api/cvc4cpp.h b/src/api/cvc4cpp.h
index d73fbfdbd..326a8fb70 100644
--- a/src/api/cvc4cpp.h
+++ b/src/api/cvc4cpp.h
@@ -495,6 +495,12 @@ class CVC4_PUBLIC Sort
   std::vector<Sort> getTupleSorts() const;
 
  private:
+  /**
+   * Helper for isNull checks. This prevents calling an API function with
+   * CVC4_API_CHECK_NOT_NULL
+   */
+  bool isNullHelper() const;
+
   /* Helper to convert a vector of sorts into a vector of internal types. */
   std::vector<Sort> typeVectorToSorts(
       const std::vector<CVC4::Type>& vector) const;
@@ -627,16 +633,11 @@ class CVC4_PUBLIC Op
   CVC4::Expr getExpr(void) const;
 
  private:
-  /* The kind of this operator. */
-  Kind d_kind;
-
   /**
-   * The internal expression wrapped by this operator.
-   * This is a shared_ptr rather than a unique_ptr to avoid overhead due to
-   * memory allocation (CVC4::Expr is already ref counted, so this could be
-   * a unique_ptr instead).
+   * Helper for isNull checks. This prevents calling an API function with
+   * CVC4_API_CHECK_NOT_NULL
    */
-  std::shared_ptr<CVC4::Expr> d_expr;
+  bool isNullHelper() const;
 
   /**
    * Note: An indexed operator has a non-null internal expr, d_expr
@@ -645,6 +646,17 @@ class CVC4_PUBLIC Op
    * @return true iff this Op is indexed
    */
   bool isIndexedHelper() const;
+
+  /* The kind of this operator. */
+  Kind d_kind;
+
+  /**
+   * The internal expression wrapped by this operator.
+   * This is a shared_ptr rather than a unique_ptr to avoid overhead due to
+   * memory allocation (CVC4::Expr is already ref counted, so this could be
+   * a unique_ptr instead).
+   */
+  std::shared_ptr<CVC4::Expr> d_expr;
 };
 
 /* -------------------------------------------------------------------------- */
@@ -869,7 +881,7 @@ class CVC4_PUBLIC Term
     Term operator*() const;
 
    private:
-    /* The original expression to be iteratoed over */
+    /* The original expression to be iterated over */
     std::shared_ptr<CVC4::Expr> d_orig_expr;
     /* Keeps track of the iteration position */
     uint32_t d_pos;
@@ -891,6 +903,12 @@ class CVC4_PUBLIC Term
 
  private:
   /**
+   * Helper for isNull checks. This prevents calling an API function with
+   * CVC4_API_CHECK_NOT_NULL
+   */
+  bool isNullHelper() const;
+
+  /**
    * The internal expression wrapped by this term.
    * This is a shared_ptr rather than a unique_ptr to avoid overhead due to
    * memory allocation (CVC4::Expr is already ref counted, so this could be