From: makaimann Date: Tue, 3 Dec 2019 14:58:47 +0000 (-0800) Subject: Add isNullHelper to avoid calling API function isNull with CVC4_API_CHECK_NOT_NULL... X-Git-Tag: cvc5-1.0.0~3807 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=8a114b1899a5b31dfe733b0dd4ed897942e43f03;p=cvc5.git Add isNullHelper to avoid calling API function isNull with CVC4_API_CHECK_NOT_NULL (#3520) --- diff --git a/src/api/cvc4cpp.cpp b/src/api/cvc4cpp.cpp index 4fd3c4276..651ed60e4 100644 --- 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::typeVectorToSorts( + const std::vector& types) const +{ + std::vector 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::getTupleSorts() const /* --------------------------------------------------------------------- */ -std::vector Sort::typeVectorToSorts( - const std::vector& types) const -{ - std::vector 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 d73fbfdbd..326a8fb70 100644 --- a/src/api/cvc4cpp.h +++ b/src/api/cvc4cpp.h @@ -495,6 +495,12 @@ class CVC4_PUBLIC Sort std::vector 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 typeVectorToSorts( const std::vector& 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 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 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 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