diff options
| author | Aina Niemetz <aina.niemetz@gmail.com> | 2018-12-14 10:25:15 -0800 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2018-12-14 10:25:15 -0800 |
| commit | a383b73fbb01acb8bc1726c6a1b61c8d1b214aae (patch) | |
| tree | f0f418fa2fd5043c69b68f2f6e260309b9762d82 /src/api | |
| parent | 075e3d97974c89dcbd4cf6c7a1c3b37cbb27403d (diff) | |
New C++ API: Add tests for opterm object. (#2756)
Diffstat (limited to 'src/api')
| -rw-r--r-- | src/api/cvc4cpp.cpp | 16 |
1 files changed, 14 insertions, 2 deletions
diff --git a/src/api/cvc4cpp.cpp b/src/api/cvc4cpp.cpp index cadad4eff..68b0301ec 100644 --- a/src/api/cvc4cpp.cpp +++ b/src/api/cvc4cpp.cpp @@ -635,6 +635,10 @@ class CVC4ApiExceptionStream CVC4_PREDICT_FALSE(cond) \ ? (void)0 : OstreamVoider() & CVC4ApiExceptionStream().ostream() +#define CVC4_API_CHECK_NOT_NULL \ + CVC4_API_CHECK(!isNull()) << "Invalid call to '" << __PRETTY_FUNCTION__ \ + << "', expected non-null object"; + #define CVC4_API_KIND_CHECK(kind) \ CVC4_API_CHECK(isDefinedKind(kind)) \ << "Invalid kind '" << kindToString(kind) << "'"; @@ -1166,9 +1170,17 @@ bool OpTerm::operator==(const OpTerm& t) const { return *d_expr == *t.d_expr; } bool OpTerm::operator!=(const OpTerm& t) const { return *d_expr != *t.d_expr; } -Kind OpTerm::getKind() const { return intToExtKind(d_expr->getKind()); } +Kind OpTerm::getKind() const +{ + CVC4_API_CHECK_NOT_NULL; + return intToExtKind(d_expr->getKind()); +} -Sort OpTerm::getSort() const { return Sort(d_expr->getType()); } +Sort OpTerm::getSort() const +{ + CVC4_API_CHECK_NOT_NULL; + return Sort(d_expr->getType()); +} bool OpTerm::isNull() const { return d_expr->isNull(); } |