diff options
Diffstat (limited to 'src/api/cvc4cpp.cpp')
| -rw-r--r-- | src/api/cvc4cpp.cpp | 25 |
1 files changed, 19 insertions, 6 deletions
diff --git a/src/api/cvc4cpp.cpp b/src/api/cvc4cpp.cpp index 5eabcfe62..748a1ce06 100644 --- a/src/api/cvc4cpp.cpp +++ b/src/api/cvc4cpp.cpp @@ -354,6 +354,7 @@ const static std::unordered_map<CVC4::Kind, Kind, CVC4::kind::KindHashFunction> {CVC4::Kind::DISTINCT, DISTINCT}, {CVC4::Kind::VARIABLE, CONSTANT}, {CVC4::Kind::BOUND_VARIABLE, VARIABLE}, + {CVC4::Kind::SEXPR, SEXPR}, {CVC4::Kind::LAMBDA, LAMBDA}, {CVC4::Kind::WITNESS, WITNESS}, /* Boolean --------------------------------------------------------- */ @@ -822,6 +823,14 @@ class CVC4ApiRecoverableExceptionStream << "Invalid argument '" << arg << "' for '" << #arg \ << "', expected " +#define CVC4_API_RECOVERABLE_ARG_CHECK_EXPECTED(cond, arg) \ + CVC4_PREDICT_TRUE(cond) \ + ? (void)0 \ + : OstreamVoider() \ + & CVC4ApiRecoverableExceptionStream().ostream() \ + << "Invalid argument '" << arg << "' for '" << #arg \ + << "', expected " + #define CVC4_API_ARG_SIZE_CHECK_EXPECTED(cond, arg) \ CVC4_PREDICT_TRUE(cond) \ ? (void)0 \ @@ -842,6 +851,10 @@ class CVC4ApiRecoverableExceptionStream { #define CVC4_API_SOLVER_TRY_CATCH_END \ } \ + catch (const UnrecognizedOptionException& e) \ + { \ + throw CVC4ApiRecoverableException(e.getMessage()); \ + } \ catch (const CVC4::RecoverableModalException& e) \ { \ throw CVC4ApiRecoverableException(e.getMessage()); \ @@ -5083,7 +5096,7 @@ std::vector<Term> Solver::getAssertions(void) const std::string Solver::getInfo(const std::string& flag) const { CVC4_API_SOLVER_TRY_CATCH_BEGIN; - CVC4_API_CHECK(d_smtEngine->isValidGetInfoFlag(flag)) + CVC4_API_RECOVERABLE_CHECK(d_smtEngine->isValidGetInfoFlag(flag)) << "Unrecognized flag for getInfo."; return d_smtEngine->getInfo(flag).toString(); @@ -5415,7 +5428,7 @@ void Solver::resetAssertions(void) const void Solver::setInfo(const std::string& keyword, const std::string& value) const { CVC4_API_SOLVER_TRY_CATCH_BEGIN; - CVC4_API_ARG_CHECK_EXPECTED( + CVC4_API_RECOVERABLE_ARG_CHECK_EXPECTED( keyword == "source" || keyword == "category" || keyword == "difficulty" || keyword == "filename" || keyword == "license" || keyword == "name" || keyword == "notes" || keyword == "smt-lib-version" @@ -5423,10 +5436,10 @@ void Solver::setInfo(const std::string& keyword, const std::string& value) const keyword) << "'source', 'category', 'difficulty', 'filename', 'license', 'name', " "'notes', 'smt-lib-version' or 'status'"; - CVC4_API_ARG_CHECK_EXPECTED(keyword != "smt-lib-version" || value == "2" - || value == "2.0" || value == "2.5" - || value == "2.6", - value) + CVC4_API_RECOVERABLE_ARG_CHECK_EXPECTED( + keyword != "smt-lib-version" || value == "2" || value == "2.0" + || value == "2.5" || value == "2.6", + value) << "'2.0', '2.5', '2.6'"; CVC4_API_ARG_CHECK_EXPECTED(keyword != "status" || value == "sat" || value == "unsat" || value == "unknown", |