From dae75929c02225ff519bf8d4cf9f9a38e1d61b08 Mon Sep 17 00:00:00 2001 From: Abdalrhman Mohamed <32971963+abdoo8080@users.noreply.github.com> Date: Fri, 5 Nov 2021 22:30:23 -0500 Subject: Print `unsupported` for unrecognized flags. (#7384) Fixes #7374. --- src/api/cpp/cvc5.cpp | 56 +++++++++++++++++----- src/api/cpp/cvc5.h | 25 ++++++++++ src/api/cpp/cvc5_checks.h | 8 ++++ src/smt/command.cpp | 20 ++++++-- test/regress/regress0/smtlib/issue7374.smt2 | 9 ++++ .../abduction_1255.corecstrs.readable.smt2 | 2 +- .../abduction/abduction_streq.readable.smt2 | 2 +- 7 files changed, 103 insertions(+), 19 deletions(-) create mode 100644 test/regress/regress0/smtlib/issue7374.smt2 diff --git a/src/api/cpp/cvc5.cpp b/src/api/cpp/cvc5.cpp index 90f6f0d56..f587bbfc0 100644 --- a/src/api/cpp/cvc5.cpp +++ b/src/api/cpp/cvc5.cpp @@ -855,6 +855,27 @@ class CVC5ApiRecoverableExceptionStream std::stringstream d_stream; }; +class CVC5ApiUnsupportedExceptionStream +{ + public: + CVC5ApiUnsupportedExceptionStream() {} + /* 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). */ + ~CVC5ApiUnsupportedExceptionStream() noexcept(false) + { + if (std::uncaught_exceptions() == 0) + { + throw CVC5ApiUnsupportedException(d_stream.str()); + } + } + + std::ostream& ostream() { return d_stream; } + + private: + std::stringstream d_stream; +}; + #define CVC5_API_TRY_CATCH_BEGIN \ try \ { @@ -6917,8 +6938,8 @@ std::vector Solver::getAssertions(void) const std::string Solver::getInfo(const std::string& flag) const { CVC5_API_TRY_CATCH_BEGIN; - CVC5_API_RECOVERABLE_CHECK(d_slv->isValidGetInfoFlag(flag)) - << "Unrecognized flag for getInfo."; + CVC5_API_UNSUPPORTED_CHECK(d_slv->isValidGetInfoFlag(flag)) + << "Unrecognized flag: " << flag << "."; //////// all checks before this line return d_slv->getInfo(flag); //////// @@ -6927,11 +6948,14 @@ std::string Solver::getInfo(const std::string& flag) const std::string Solver::getOption(const std::string& option) const { - CVC5_API_TRY_CATCH_BEGIN; - //////// all checks before this line - return d_slv->getOption(option); - //////// - CVC5_API_TRY_CATCH_END; + try + { + return d_slv->getOption(option); + } + catch (OptionException& e) + { + throw CVC5ApiUnsupportedException(e.getMessage()); + } } // Supports a visitor from a list of lambdas @@ -7564,13 +7588,14 @@ void Solver::resetAssertions(void) const void Solver::setInfo(const std::string& keyword, const std::string& value) const { CVC5_API_TRY_CATCH_BEGIN; - CVC5_API_RECOVERABLE_ARG_CHECK_EXPECTED( + CVC5_API_UNSUPPORTED_CHECK( keyword == "source" || keyword == "category" || keyword == "difficulty" - || keyword == "filename" || keyword == "license" || keyword == "name" - || keyword == "notes" || keyword == "smt-lib-version" - || keyword == "status", - keyword) - << "'source', 'category', 'difficulty', 'filename', 'license', 'name', " + || keyword == "filename" || keyword == "license" || keyword == "name" + || keyword == "notes" || keyword == "smt-lib-version" + || keyword == "status") + << "Unrecognized keyword: " << keyword + << ", expected 'source', 'category', 'difficulty', " + "'filename', 'license', 'name', " "'notes', 'smt-lib-version' or 'status'"; CVC5_API_RECOVERABLE_ARG_CHECK_EXPECTED( keyword != "smt-lib-version" || value == "2" || value == "2.0" @@ -7603,6 +7628,11 @@ void Solver::setOption(const std::string& option, const std::string& value) const { CVC5_API_TRY_CATCH_BEGIN; + std::vector options = options::getNames(); + CVC5_API_UNSUPPORTED_CHECK( + option.find("command-verbosity") != std::string::npos + || std::find(options.cbegin(), options.cend(), option) != options.cend()) + << "Unrecognized option: " << option << '.'; static constexpr auto mutableOpts = {"diagnostic-output-channel", "print-success", "regular-output-channel", diff --git a/src/api/cpp/cvc5.h b/src/api/cpp/cvc5.h index f348ae4e5..b73c1ce27 100644 --- a/src/api/cpp/cvc5.h +++ b/src/api/cpp/cvc5.h @@ -120,6 +120,31 @@ class CVC5_EXPORT CVC5ApiRecoverableException : public CVC5ApiException } }; +/** + * Exception for unsupported command arguments. + * If thrown, API objects can still be used. + */ +class CVC5_EXPORT CVC5ApiUnsupportedException : public CVC5ApiRecoverableException +{ + public: + /** + * Construct with message from a string. + * @param str The error message. + */ + CVC5ApiUnsupportedException(const std::string& str) + : CVC5ApiRecoverableException(str) + { + } + /** + * Construct with message from a string stream. + * @param stream The error message. + */ + CVC5ApiUnsupportedException(const std::stringstream& stream) + : CVC5ApiRecoverableException(stream.str()) + { + } +}; + /** * An option-related API exception. * If thrown, API objects can still be used. diff --git a/src/api/cpp/cvc5_checks.h b/src/api/cpp/cvc5_checks.h index 35c21df9c..71b17cef1 100644 --- a/src/api/cpp/cvc5_checks.h +++ b/src/api/cpp/cvc5_checks.h @@ -43,6 +43,14 @@ namespace api { CVC5_PREDICT_TRUE(cond) \ ? (void)0 : OstreamVoider() & CVC5ApiRecoverableExceptionStream().ostream() +/** + * The base check macro for throwing unsupported exceptions. + * Throws a CVC5ApiUnsupportedException if 'cond' is false. + */ +#define CVC5_API_UNSUPPORTED_CHECK(cond) \ + CVC5_PREDICT_TRUE(cond) \ + ? (void)0 : OstreamVoider() & CVC5ApiUnsupportedExceptionStream().ostream() + /* -------------------------------------------------------------------------- */ /* Not null checks. */ /* -------------------------------------------------------------------------- */ diff --git a/src/smt/command.cpp b/src/smt/command.cpp index a15e20998..419167e7e 100644 --- a/src/smt/command.cpp +++ b/src/smt/command.cpp @@ -2557,11 +2557,15 @@ void SetInfoCommand::invoke(api::Solver* solver, SymbolManager* sm) solver->setInfo(d_flag, d_value); d_commandStatus = CommandSuccess::instance(); } - catch (api::CVC5ApiRecoverableException&) + catch (api::CVC5ApiUnsupportedException&) { // As per SMT-LIB spec, silently accept unknown set-info keys d_commandStatus = CommandSuccess::instance(); } + catch (api::CVC5ApiRecoverableException& e) + { + d_commandStatus = new CommandRecoverableFailure(e.getMessage()); + } catch (exception& e) { d_commandStatus = new CommandFailure(e.what()); @@ -2599,9 +2603,13 @@ void GetInfoCommand::invoke(api::Solver* solver, SymbolManager* sm) d_result = sexprToString(solver->mkTerm(api::SEXPR, v)); d_commandStatus = CommandSuccess::instance(); } + catch (api::CVC5ApiUnsupportedException&) + { + d_commandStatus = new CommandUnsupported(); + } catch (api::CVC5ApiRecoverableException& e) { - d_commandStatus = new CommandRecoverableFailure(e.what()); + d_commandStatus = new CommandRecoverableFailure(e.getMessage()); } catch (exception& e) { @@ -2658,10 +2666,14 @@ void SetOptionCommand::invoke(api::Solver* solver, SymbolManager* sm) solver->setOption(d_flag, d_value); d_commandStatus = CommandSuccess::instance(); } - catch (api::CVC5ApiRecoverableException&) + catch (api::CVC5ApiUnsupportedException&) { d_commandStatus = new CommandUnsupported(); } + catch (api::CVC5ApiRecoverableException& e) + { + d_commandStatus = new CommandRecoverableFailure(e.getMessage()); + } catch (exception& e) { d_commandStatus = new CommandFailure(e.what()); @@ -2696,7 +2708,7 @@ void GetOptionCommand::invoke(api::Solver* solver, SymbolManager* sm) d_result = solver->getOption(d_flag); d_commandStatus = CommandSuccess::instance(); } - catch (api::CVC5ApiRecoverableException&) + catch (api::CVC5ApiUnsupportedException&) { d_commandStatus = new CommandUnsupported(); } diff --git a/test/regress/regress0/smtlib/issue7374.smt2 b/test/regress/regress0/smtlib/issue7374.smt2 new file mode 100644 index 000000000..59caef57c --- /dev/null +++ b/test/regress/regress0/smtlib/issue7374.smt2 @@ -0,0 +1,9 @@ +; EXPECT: unsupported +; EXPECT: unsupported +; EXPECT: unsupported + +(set-logic QF_SAT) +(set-info :zzz true) +(get-info :zzz) +(set-option :zzz true) +(get-option :zzz) diff --git a/test/regress/regress1/abduction/abduction_1255.corecstrs.readable.smt2 b/test/regress/regress1/abduction/abduction_1255.corecstrs.readable.smt2 index 1595b0865..44bccd264 100644 --- a/test/regress/regress1/abduction/abduction_1255.corecstrs.readable.smt2 +++ b/test/regress/regress1/abduction/abduction_1255.corecstrs.readable.smt2 @@ -3,7 +3,7 @@ ; EXIT: 0 -(set-info :smt-lib-version |2.6|) +(set-info :smt-lib-version 2.6) (set-logic QF_SLIA) (set-info :source | Generated by: Andrew Reynolds diff --git a/test/regress/regress1/abduction/abduction_streq.readable.smt2 b/test/regress/regress1/abduction/abduction_streq.readable.smt2 index b466ab33e..c13f3175e 100644 --- a/test/regress/regress1/abduction/abduction_streq.readable.smt2 +++ b/test/regress/regress1/abduction/abduction_streq.readable.smt2 @@ -2,7 +2,7 @@ ; SCRUBBER: grep -v -E '(\(define-fun)' ; EXIT: 0 -(set-info :smt-lib-version |2.6|) +(set-info :smt-lib-version 2.6) (set-logic QF_SLIA) (set-info :source | Generated by: Andrew Reynolds -- cgit v1.2.3