diff options
| author | Abdalrhman Mohamed <32971963+abdoo8080@users.noreply.github.com> | 2020-11-30 13:32:51 -0600 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2020-11-30 13:32:51 -0600 |
| commit | aa7585a6083884ad76ecc83af60020403096129a (patch) | |
| tree | bd3fcc79604a2f49d87160e20a14a38cc689f2a2 /src/api/cvc4cpp.cpp | |
| parent | 9f372f084f5c558e3ff618d02abfdb384a82e066 (diff) | |
Eliminate uses of SExpr from the parser. (#5496)
This is a step towards migrating Commands to the API. SExpr is an internal module that's not used by the API but is used by the parser and some commands. This PR replaces SExpr with terms of kind SEXPR in the parser and strings in commands (which brings them more inline with the API).
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", |