diff options
Diffstat (limited to 'src/api/cvc4cpp.cpp')
| -rw-r--r-- | src/api/cvc4cpp.cpp | 105 |
1 files changed, 65 insertions, 40 deletions
diff --git a/src/api/cvc4cpp.cpp b/src/api/cvc4cpp.cpp index 72fa55d6f..cbf576deb 100644 --- a/src/api/cvc4cpp.cpp +++ b/src/api/cvc4cpp.cpp @@ -1383,22 +1383,11 @@ Op::~Op() } } -/* Helpers */ -/* -------------------------------------------------------------------------- */ - -/* Split out to avoid nested API calls (problematic with API tracing). */ -/* .......................................................................... */ - -bool Op::isNullHelper() const -{ - return (d_node->isNull() && (d_kind == NULL_EXPR)); -} - -bool Op::isIndexedHelper() const { return !d_node->isNull(); } - /* Public methods */ bool Op::operator==(const Op& t) const { + CVC4_API_TRY_CATCH_BEGIN; + //////// all checks before this line if (d_node->isNull() && t.d_node->isNull()) { return (d_kind == t.d_kind); @@ -1408,56 +1397,70 @@ bool Op::operator==(const Op& t) const return false; } return (d_kind == t.d_kind) && (*d_node == *t.d_node); + //////// + CVC4_API_TRY_CATCH_END; } -bool Op::operator!=(const Op& t) const { return !(*this == t); } +bool Op::operator!=(const Op& t) const +{ + CVC4_API_TRY_CATCH_BEGIN; + //////// all checks before this line + return !(*this == t); + //////// + CVC4_API_TRY_CATCH_END; +} Kind Op::getKind() const { CVC4_API_CHECK(d_kind != NULL_EXPR) << "Expecting a non-null Kind"; + //////// all checks before this line return d_kind; } -bool Op::isNull() const { return isNullHelper(); } +bool Op::isNull() const +{ + CVC4_API_TRY_CATCH_BEGIN; + //////// all checks before this line + return isNullHelper(); + //////// + CVC4_API_TRY_CATCH_END; +} -bool Op::isIndexed() const { return isIndexedHelper(); } +bool Op::isIndexed() const +{ + CVC4_API_TRY_CATCH_BEGIN; + //////// all checks before this line + return isIndexedHelper(); + //////// + CVC4_API_TRY_CATCH_END; +} template <> std::string Op::getIndices() const { + CVC4_API_TRY_CATCH_BEGIN; CVC4_API_CHECK_NOT_NULL; CVC4_API_CHECK(!d_node->isNull()) << "Expecting a non-null internal expression. This Op is not indexed."; - - std::string i; Kind k = intToExtKind(d_node->getKind()); - - if (k == DIVISIBLE) - { - // DIVISIBLE returns a string index to support - // arbitrary precision integers - CVC4::Integer _int = d_node->getConst<Divisible>().k; - i = _int.toString(); - } - else if (k == RECORD_UPDATE) - { - i = d_node->getConst<RecordUpdate>().getField(); - } - else - { - CVC4_API_CHECK(false) << "Can't get string index from" - << " kind " << kindToString(k); - } - - return i; + CVC4_API_CHECK(k == DIVISIBLE || k == RECORD_UPDATE) + << "Can't get string index from" + << " kind " << kindToString(k); + //////// all checks before this line + return k == DIVISIBLE ? d_node->getConst<Divisible>().k.toString() + : d_node->getConst<RecordUpdate>().getField(); + //////// + CVC4_API_TRY_CATCH_END; } template <> uint32_t Op::getIndices() const { + CVC4_API_TRY_CATCH_BEGIN; CVC4_API_CHECK_NOT_NULL; CVC4_API_CHECK(!d_node->isNull()) << "Expecting a non-null internal expression. This Op is not indexed."; + //////// all checks before this line uint32_t i = 0; Kind k = intToExtKind(d_node->getKind()); @@ -1491,18 +1494,22 @@ uint32_t Op::getIndices() const i = d_node->getConst<RegExpRepeat>().d_repeatAmount; break; default: - CVC4ApiExceptionStream().ostream() << "Can't get uint32_t index from" - << " kind " << kindToString(k); + CVC4_API_CHECK(false) << "Can't get uint32_t index from" + << " kind " << kindToString(k); } return i; + //////// + CVC4_API_TRY_CATCH_END; } template <> std::pair<uint32_t, uint32_t> Op::getIndices() const { + CVC4_API_TRY_CATCH_BEGIN; CVC4_API_CHECK_NOT_NULL; CVC4_API_CHECK(!d_node->isNull()) << "Expecting a non-null internal expression. This Op is not indexed."; + //////// all checks before this line std::pair<uint32_t, uint32_t> indices; Kind k = intToExtKind(d_node->getKind()); @@ -1565,11 +1572,14 @@ std::pair<uint32_t, uint32_t> Op::getIndices() const << " kind " << kindToString(k); } return indices; + //////// + CVC4_API_TRY_CATCH_END; } std::string Op::toString() const { - CVC4_API_CHECK_NOT_NULL; + CVC4_API_TRY_CATCH_BEGIN; + //////// all checks before this line if (d_node->isNull()) { return kindToString(d_kind); @@ -1585,6 +1595,8 @@ std::string Op::toString() const } return d_node->toString(); } + //////// + CVC4_API_TRY_CATCH_END; } std::ostream& operator<<(std::ostream& out, const Op& t) @@ -1605,6 +1617,19 @@ size_t OpHashFunction::operator()(const Op& t) const } } +/* Helpers */ +/* -------------------------------------------------------------------------- */ + +/* Split out to avoid nested API calls (problematic with API tracing). */ +/* .......................................................................... */ + +bool Op::isNullHelper() const +{ + return (d_node->isNull() && (d_kind == NULL_EXPR)); +} + +bool Op::isIndexedHelper() const { return !d_node->isNull(); } + /* -------------------------------------------------------------------------- */ /* Term */ /* -------------------------------------------------------------------------- */ |