From 2dfdd5adaf2e10067aaf708e055ed5fd6047aae4 Mon Sep 17 00:00:00 2001 From: Gereon Kremer Date: Thu, 19 Aug 2021 17:31:58 -0700 Subject: [PATCH] Add CVC5ApiOptionException (#6992) This PR adds the new CVC5ApiOptionException. While the driver does not (and can not) do anything special for the two existing api exceptions, it can (and should) properly inform the user about incorrect command line option usage. The PR also removes the UnrecognizedOptionException. It is purely internal now, and immediately catched by the API wrapper. Having a separate exception for this is no longer useful. The additional catch block in main.cpp is only temporary until option parsing has been migrated to the driver and setting the options is done properly via the API. --- src/api/cpp/cvc5.cpp | 4 ++-- src/api/cpp/cvc5.h | 25 +++++++++++++++++++++ src/main/driver_unified.cpp | 3 ++- src/main/main.cpp | 29 ++++++++++++++++++++----- src/options/option_exception.h | 27 ++--------------------- src/options/options_public_template.cpp | 13 ++++++----- 6 files changed, 62 insertions(+), 39 deletions(-) diff --git a/src/api/cpp/cvc5.cpp b/src/api/cpp/cvc5.cpp index 60ef49cb4..82064b758 100644 --- a/src/api/cpp/cvc5.cpp +++ b/src/api/cpp/cvc5.cpp @@ -858,9 +858,9 @@ class CVC5ApiRecoverableExceptionStream { #define CVC5_API_TRY_CATCH_END \ } \ - catch (const UnrecognizedOptionException& e) \ + catch (const OptionException& e) \ { \ - throw CVC5ApiRecoverableException(e.getMessage()); \ + throw CVC5ApiOptionException(e.getMessage()); \ } \ catch (const cvc5::RecoverableModalException& e) \ { \ diff --git a/src/api/cpp/cvc5.h b/src/api/cpp/cvc5.h index a232f9c7e..62ee9ac32 100644 --- a/src/api/cpp/cvc5.h +++ b/src/api/cpp/cvc5.h @@ -118,6 +118,31 @@ class CVC5_EXPORT CVC5ApiRecoverableException : public CVC5ApiException } }; +/** + * An option-related API exception. + * If thrown, API objects can still be used. + */ +class CVC5_EXPORT CVC5ApiOptionException : public CVC5ApiRecoverableException +{ + public: + /** + * Construct with message from a string. + * @param str The error message. + */ + CVC5ApiOptionException(const std::string& str) + : CVC5ApiRecoverableException(str) + { + } + /** + * Construct with message from a string stream. + * @param stream The error message. + */ + CVC5ApiOptionException(const std::stringstream& stream) + : CVC5ApiRecoverableException(stream.str()) + { + } +}; + /* -------------------------------------------------------------------------- */ /* Result */ /* -------------------------------------------------------------------------- */ diff --git a/src/main/driver_unified.cpp b/src/main/driver_unified.cpp index 606f18095..0f1130234 100644 --- a/src/main/driver_unified.cpp +++ b/src/main/driver_unified.cpp @@ -34,10 +34,11 @@ #include "main/signal_handlers.h" #include "main/time_limit.h" #include "options/base_options.h" +#include "options/main_options.h" +#include "options/option_exception.h" #include "options/options.h" #include "options/options_public.h" #include "options/parser_options.h" -#include "options/main_options.h" #include "options/set_language.h" #include "parser/parser.h" #include "parser/parser_builder.h" diff --git a/src/main/main.cpp b/src/main/main.cpp index a00e29b04..6173cfd69 100644 --- a/src/main/main.cpp +++ b/src/main/main.cpp @@ -47,25 +47,42 @@ using namespace cvc5::language; * problems. That's why main() wraps runCvc5() in the first place. * Put everything in runCvc5(). */ -int main(int argc, char* argv[]) { +int main(int argc, char* argv[]) +{ Options opts; - try { + try + { return runCvc5(argc, argv, opts); - } catch(OptionException& e) { + } + catch (cvc5::api::CVC5ApiOptionException& e) + { +#ifdef CVC5_COMPETITION_MODE + *opts.base.out << "unknown" << endl; +#endif + cerr << "(error \"" << e.getMessage() << "\")" << endl + << endl + << "Please use --help to get help on command-line options." << endl; + } + catch (cvc5::OptionException& e) + { #ifdef CVC5_COMPETITION_MODE *opts.base.out << "unknown" << endl; #endif - cerr << "(error \"" << e << "\")" << endl + cerr << "(error \"" << e.getMessage() << "\")" << endl << endl << "Please use --help to get help on command-line options." << endl; - } catch(Exception& e) { + } + catch (Exception& e) + { #ifdef CVC5_COMPETITION_MODE *opts.base.out << "unknown" << endl; #endif if (language::isOutputLang_smt2(opts.base.outputLanguage)) { *opts.base.out << "(error \"" << e << "\")" << endl; - } else { + } + else + { *opts.base.err << "(error \"" << e << "\")" << endl; } if (opts.base.statistics && pExecutor != nullptr) diff --git a/src/options/option_exception.h b/src/options/option_exception.h index f5590709e..6d24e7c39 100644 --- a/src/options/option_exception.h +++ b/src/options/option_exception.h @@ -19,17 +19,14 @@ #define CVC5__OPTION_EXCEPTION_H #include "base/exception.h" -#include "cvc5_export.h" namespace cvc5 { /** * Class representing an option-parsing exception such as badly-typed - * or missing arguments, arguments out of bounds, etc. If an option - * name is itself unrecognized, a UnrecognizedOptionException (a derived - * class, below) should be used instead. + * or missing arguments, arguments out of bounds, etc. */ -class CVC5_EXPORT OptionException : public cvc5::Exception +class OptionException : public cvc5::Exception { public: OptionException(const std::string& s) : cvc5::Exception(s_errPrefix + s) {} @@ -48,26 +45,6 @@ class CVC5_EXPORT OptionException : public cvc5::Exception static const std::string s_errPrefix; }; /* class OptionException */ -/** - * Class representing an exception in option processing due to an - * unrecognized or unsupported option key. - */ -class UnrecognizedOptionException : public cvc5::OptionException -{ - public: - UnrecognizedOptionException() - : cvc5::OptionException( - "Unrecognized informational or option key or setting") - { - } - - UnrecognizedOptionException(const std::string& msg) - : cvc5::OptionException( - "Unrecognized informational or option key or setting: " + msg) - { - } -}; /* class UnrecognizedOptionException */ - } // namespace cvc5 #endif /* CVC5__OPTION_EXCEPTION_H */ diff --git a/src/options/options_public_template.cpp b/src/options/options_public_template.cpp index 33c363b55..dc09c0618 100644 --- a/src/options/options_public_template.cpp +++ b/src/options/options_public_template.cpp @@ -501,16 +501,19 @@ std::vector parse( std::string get(const Options& options, const std::string& name) { Trace("options") << "Options::getOption(" << name << ")" << std::endl; + // clang-format off ${getoption_handlers}$ - - throw UnrecognizedOptionException(name); + // clang-format on + throw OptionException("Unrecognized option key or setting: " + name); } void setInternal(Options& opts, const std::string& name, const std::string& optionarg) - { -${setoption_handlers}$ - throw UnrecognizedOptionException(name); +{ + // clang-format off + ${setoption_handlers}$ + // clang-format on + throw OptionException("Unrecognized option key or setting: " + name); } void set(Options& opts, const std::string& name, const std::string& optionarg) -- 2.30.2