diff options
author | Abdalrhman Mohamed <32971963+abdoo8080@users.noreply.github.com> | 2020-10-05 20:11:44 -0500 |
---|---|---|
committer | GitHub <noreply@github.com> | 2020-10-05 20:11:44 -0500 |
commit | cd7680c5a23ade0bd8d7f0dfac4623ed318639bb (patch) | |
tree | f58de3855231eb57ac320db90cd67df2f73efc19 /src/api/cvc4cpp.cpp | |
parent | cedeef257a8031bcfb16aa6e6f500121348458bf (diff) |
Recover from some exceptions. (#5203)
This PR replaces more calls to SmtEngine functions with calls to corresponding Solver functions in command.cpp. The PR also adds CVC4_API_RECOVERABLE_CHECK macro to use for recoverable exceptions.
Diffstat (limited to 'src/api/cvc4cpp.cpp')
-rw-r--r-- | src/api/cvc4cpp.cpp | 27 |
1 files changed, 26 insertions, 1 deletions
diff --git a/src/api/cvc4cpp.cpp b/src/api/cvc4cpp.cpp index 179eb672e..30e95714d 100644 --- a/src/api/cvc4cpp.cpp +++ b/src/api/cvc4cpp.cpp @@ -752,10 +752,35 @@ class CVC4ApiExceptionStream std::stringstream d_stream; }; +class CVC4ApiRecoverableExceptionStream +{ + public: + CVC4ApiRecoverableExceptionStream() {} + /* Note: This needs to be explicitly set to 'noexcept(false)' since it is + * a destructor that throws an exception and in C++11 all destructors + * default to noexcept(true) (else this triggers a call to std::terminate). */ + ~CVC4ApiRecoverableExceptionStream() noexcept(false) + { + if (!std::uncaught_exception()) + { + throw CVC4ApiRecoverableException(d_stream.str()); + } + } + + std::ostream& ostream() { return d_stream; } + + private: + std::stringstream d_stream; +}; + #define CVC4_API_CHECK(cond) \ CVC4_PREDICT_TRUE(cond) \ ? (void)0 : OstreamVoider() & CVC4ApiExceptionStream().ostream() +#define CVC4_API_RECOVERABLE_CHECK(cond) \ + CVC4_PREDICT_TRUE(cond) \ + ? (void)0 : OstreamVoider() & CVC4ApiRecoverableExceptionStream().ostream() + #define CVC4_API_CHECK_NOT_NULL \ CVC4_API_CHECK(!isNullHelper()) \ << "Invalid call to '" << __PRETTY_FUNCTION__ \ @@ -5075,7 +5100,7 @@ std::vector<Term> Solver::getUnsatCore(void) const CVC4_API_CHECK(d_smtEngine->getOptions()[options::unsatCores]) << "Cannot get unsat core unless explicitly enabled " "(try --produce-unsat-cores)"; - CVC4_API_CHECK(d_smtEngine->getSmtMode() == SmtMode::UNSAT) + CVC4_API_RECOVERABLE_CHECK(d_smtEngine->getSmtMode() == SmtMode::UNSAT) << "Cannot get unsat core unless in unsat mode."; UnsatCore core = d_smtEngine->getUnsatCore(); /* Can not use |