Add isNullHelper to avoid calling API function isNull with CVC4_API_CHECK_NOT_NULL...

diff --git a/src/api/cvc4cpp.cpp b/src/api/cvc4cpp.cpp
index 4fd3c42769205522f791abe70fe992ccba23bec8..651ed60e4d576dcf420876d68782167947b44d6c 100644 (file)
--- a/src/api/cvc4cpp.cpp
+++ b/src/api/cvc4cpp.cpp
@@ -623,8 +623,8 @@ class CVC4ApiExceptionStream
   ? (void)0 : OstreamVoider() & CVC4ApiExceptionStream().ostream()
 
 #define CVC4_API_CHECK_NOT_NULL                                           \
-  CVC4_API_CHECK(!isNull()) << "Invalid call to '" << __PRETTY_FUNCTION__ \
-                            << "', expected non-null object";
+  CVC4_API_CHECK(!isNullHelper()) << "Invalid call to '" << __PRETTY_FUNCTION__ \
+                                  << "', expected non-null object";
 
 #define CVC4_API_ARG_CHECK_NOT_NULL(arg) \
   CVC4_API_CHECK(!arg.isNull()) << "Invalid null argument for '" << #arg << "'";
@@ -757,11 +757,30 @@ Sort::Sort() : d_type(new CVC4::Type()) {}
 
 Sort::~Sort() {}
 
+/* Helpers                                                                    */
+/* -------------------------------------------------------------------------- */
+
+/* Split out to avoid nested API calls (problematic with API tracing).        */
+/* .......................................................................... */
+
+bool Sort::isNullHelper() const { return d_type->isNull(); }
+
+std::vector<Sort> Sort::typeVectorToSorts(
+                                          const std::vector<CVC4::Type>& types) const
+{
+  std::vector<Sort> res;
+  for (const CVC4::Type& t : types)
+    {
+      res.push_back(Sort(t));
+    }
+  return res;
+}
+
 bool Sort::operator==(const Sort& s) const { return *d_type == *s.d_type; }
 
 bool Sort::operator!=(const Sort& s) const { return *d_type != *s.d_type; }
 
-bool Sort::isNull() const { return d_type->isNull(); }
+bool Sort::isNull() const { return isNullHelper(); }
 
 bool Sort::isBoolean() const { return d_type->isBoolean(); }
 
@@ -968,19 +987,6 @@ std::vector<Sort> Sort::getTupleSorts() const
 
 /* --------------------------------------------------------------------- */
 
-std::vector<Sort> Sort::typeVectorToSorts(
-    const std::vector<CVC4::Type>& types) const
-{
-  std::vector<Sort> res;
-  for (const CVC4::Type& t : types)
-  {
-    res.push_back(Sort(t));
-  }
-  return res;
-}
-
-/* --------------------------------------------------------------------- */
-
 std::ostream& operator<<(std::ostream& out, const Sort& s)
 {
   out << s.toString();
@@ -1012,6 +1018,8 @@ Op::~Op() {}
 /* Split out to avoid nested API calls (problematic with API tracing).        */
 /* .......................................................................... */
 
+bool Op::isNullHelper() const { return (d_expr->isNull() && (d_kind == NULL_EXPR)); }
+
 bool Op::isIndexedHelper() const { return !d_expr->isNull(); }
 
 /* Public methods                                                             */
@@ -1038,7 +1046,7 @@ Sort Op::getSort() const
   return Sort(d_expr->getType());
 }
 
-bool Op::isNull() const { return (d_expr->isNull() && (d_kind == NULL_EXPR)); }
+bool Op::isNull() const { return isNullHelper(); }
 
 bool Op::isIndexed() const { return isIndexedHelper(); }
 
@@ -1236,6 +1244,14 @@ Term::Term(const CVC4::Expr& e) : d_expr(new CVC4::Expr(e)) {}
 
 Term::~Term() {}
 
+/* Helpers                                                                    */
+/* -------------------------------------------------------------------------- */
+
+/* Split out to avoid nested API calls (problematic with API tracing).        */
+/* .......................................................................... */
+
+bool Term::isNullHelper() const { return d_expr->isNull(); }
+
 bool Term::operator==(const Term& t) const { return *d_expr == *t.d_expr; }
 
 bool Term::operator!=(const Term& t) const { return *d_expr != *t.d_expr; }
@@ -1291,7 +1307,7 @@ Op Term::getOp() const
   }
 }
 
-bool Term::isNull() const { return d_expr->isNull(); }
+bool Term::isNull() const { return isNullHelper(); }
 
 bool Term::isParameterized() const
 {

diff --git a/src/api/cvc4cpp.h b/src/api/cvc4cpp.h
index d73fbfdbd0bfe89a70551d993841e279f64caeb9..326a8fb70101cbfe75d08108a5dd709fe0e7f156 100644 (file)
--- 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;
@@ -890,6 +902,12 @@ class CVC4_PUBLIC Term
   CVC4::Expr getExpr(void) const;
 
  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