From b5ac06abf4b2cc6b027dedd045595187589bcc35 Mon Sep 17 00:00:00 2001 From: Gereon Kremer Date: Wed, 28 Apr 2021 19:31:41 +0200 Subject: Clean up options holder class (#6458) This PR does some cleanup on the options class: it puts the option defaults into the member declaration and removes the explicit constructor; it puts the holder into a unique_ptr; it uses the regular struct copy operation instead of reconstructing the holder object; it moves some macros required for option defaults into the option holder header. Also, this PR removes some obsolete code related to suggestions for typos. --- src/options/mkoptions.py | 12 +++++-- src/options/options.h | 19 ++-------- src/options/options_holder_template.h | 9 ++++- src/options/options_template.cpp | 67 ++++++++--------------------------- 4 files changed, 34 insertions(+), 73 deletions(-) (limited to 'src') diff --git a/src/options/mkoptions.py b/src/options/mkoptions.py index fa2a39b04..13df7b8bd 100644 --- a/src/options/mkoptions.py +++ b/src/options/mkoptions.py @@ -121,8 +121,10 @@ TPL_PUSHBACK_PREEMPT = 'extender->pushBackPreemption({});' TPL_HOLDER_MACRO = '#define ' + TPL_HOLDER_MACRO_NAME TPL_HOLDER_MACRO_ATTR = " {name}__option_t::type {name};\\\n" -TPL_HOLDER_MACRO_ATTR += " bool {name}__setByUser__;" +TPL_HOLDER_MACRO_ATTR += " bool {name}__setByUser__ = false;" +TPL_HOLDER_MACRO_ATTR_DEF = " {name}__option_t::type {name} = {default};\\\n" +TPL_HOLDER_MACRO_ATTR_DEF += " bool {name}__setByUser__ = false;" TPL_OPTION_STRUCT_RW = \ """extern struct {name}__option_t @@ -450,7 +452,13 @@ def codegen_module(module, dst_dir, tpl_module_h, tpl_module_cpp): includes.update([format_include(x) for x in option.includes]) # Generate option holder macro - holder_specs.append(TPL_HOLDER_MACRO_ATTR.format(name=option.name)) + if option.default: + default = option.default + if option.mode and option.type not in default: + default = '{}::{}'.format(option.type, default) + holder_specs.append(TPL_HOLDER_MACRO_ATTR_DEF.format(name=option.name, default=default)) + else: + holder_specs.append(TPL_HOLDER_MACRO_ATTR.format(name=option.name)) # Generate module declaration tpl_decl = TPL_OPTION_STRUCT_RO if option.read_only else TPL_OPTION_STRUCT_RW diff --git a/src/options/options.h b/src/options/options.h index b249c90ed..a8fc50b68 100644 --- a/src/options/options.h +++ b/src/options/options.h @@ -19,6 +19,7 @@ #define CVC5__OPTIONS__OPTIONS_H #include +#include #include #include @@ -45,7 +46,7 @@ class CVC5_EXPORT Options { friend api::Solver; /** The struct that holds all option values. */ - options::OptionsHolder* d_holder; + std::unique_ptr d_holder; /** The handler for the options of the theory. */ options::OptionsHandler* d_handler; @@ -251,22 +252,6 @@ public: /** Print help for the --lang command line option */ static void printLanguageHelp(std::ostream& out); - /** - * Look up long command-line option names that bear some similarity - * to the given name. Returns an empty string if there are no - * suggestions. - */ - static std::string suggestCommandLineOptions(const std::string& optionName); - - /** - * Look up SMT option names that bear some similarity to - * the given name. Don't include the initial ":". This might be - * useful in case of typos. Can return an empty vector if there are - * no suggestions. - */ - static std::vector suggestSmtOptions( - const std::string& optionName); - /** * Initialize the Options object options based on the given * command-line arguments given in argc and argv. The return value diff --git a/src/options/options_holder_template.h b/src/options/options_holder_template.h index 8f5a0e096..04e5eba53 100644 --- a/src/options/options_holder_template.h +++ b/src/options/options_holder_template.h @@ -24,13 +24,20 @@ ${headers_module}$ namespace cvc5 { namespace options { +#if defined(CVC5_MUZZLED) || defined(CVC5_COMPETITION_MODE) +# define DO_SEMANTIC_CHECKS_BY_DEFAULT false +#else /* CVC5_MUZZLED || CVC5_COMPETITION_MODE */ +# define DO_SEMANTIC_CHECKS_BY_DEFAULT true +#endif /* CVC5_MUZZLED || CVC5_COMPETITION_MODE */ + struct OptionsHolder { - OptionsHolder(); ${macros_module}$ }; /* struct OptionsHolder */ +#undef DO_SEMANTIC_CHECKS_BY_DEFAULT + } // namespace options } // namespace cvc5 diff --git a/src/options/options_template.cpp b/src/options/options_template.cpp index 4493f6094..49a35ab38 100644 --- a/src/options/options_template.cpp +++ b/src/options/options_template.cpp @@ -230,13 +230,11 @@ Options::Options(OptionsListener* ol) Options::~Options() { delete d_handler; - delete d_holder; } void Options::copyValues(const Options& options){ if(this != &options) { - delete d_holder; - d_holder = new options::OptionsHolder(*options.d_holder); + *d_holder = *options.d_holder; } } @@ -254,19 +252,6 @@ void Options::setListener(OptionsListener* ol) { d_olisten = ol; } ${custom_handlers}$ // clang-format on -#if defined(CVC5_MUZZLED) || defined(CVC5_COMPETITION_MODE) -# define DO_SEMANTIC_CHECKS_BY_DEFAULT false -#else /* CVC5_MUZZLED || CVC5_COMPETITION_MODE */ -# define DO_SEMANTIC_CHECKS_BY_DEFAULT true -#endif /* CVC5_MUZZLED || CVC5_COMPETITION_MODE */ - -// clang-format off -options::OptionsHolder::OptionsHolder() : - ${module_defaults}$ -{ -} -// clang-format on - static const std::string mostCommonOptionsDescription = "\ Most commonly-used cvc5 options:\n" @@ -419,6 +404,18 @@ std::vector Options::parseOptions(Options* options, return nonoptions; } +std::string suggestCommandLineOptions(const std::string& optionName) +{ + DidYouMean didYouMean; + + const char* opt; + for(size_t i = 0; (opt = cmdlineOptions[i].name) != nullptr; ++i) { + didYouMean.addWord(std::string("--") + cmdlineOptions[i].name); + } + + return didYouMean.getMatchAsString(optionName.substr(0, optionName.find('='))); +} + void Options::parseOptionsRecursive(int argc, char* argv[], std::vector* nonoptions) @@ -531,39 +528,6 @@ ${options_handler}$ << " non-option arguments." << std::endl; } -std::string Options::suggestCommandLineOptions(const std::string& optionName) -{ - DidYouMean didYouMean; - - const char* opt; - for(size_t i = 0; (opt = cmdlineOptions[i].name) != NULL; ++i) { - didYouMean.addWord(std::string("--") + cmdlineOptions[i].name); - } - - return didYouMean.getMatchAsString(optionName.substr(0, optionName.find('='))); -} - -// clang-format off -static const char* smtOptions[] = { - ${options_smt}$ - nullptr}; -// clang-format on - -std::vector Options::suggestSmtOptions( - const std::string& optionName) -{ - std::vector suggestions; - - const char* opt; - for(size_t i = 0; (opt = smtOptions[i]) != NULL; ++i) { - if(std::strstr(opt, optionName.c_str()) != NULL) { - suggestions.push_back(opt); - } - } - - return suggestions; -} - // clang-format off std::vector > Options::getOptions() const { @@ -608,8 +572,5 @@ std::string Options::getOption(const std::string& key) const } // clang-format on -#undef USE_EARLY_TYPE_CHECKING_BY_DEFAULT -#undef DO_SEMANTIC_CHECKS_BY_DEFAULT - } // namespace cvc5 -// clang-format on + -- cgit v1.2.3