diff options
author | Gereon Kremer <gkremer@stanford.edu> | 2021-04-26 21:43:15 +0200 |
---|---|---|
committer | GitHub <noreply@github.com> | 2021-04-26 19:43:15 +0000 |
commit | c32f952b1e496a5bd05552f676d51b5af3e49ed0 (patch) | |
tree | 50ad233923f494b5f551d3ba0b6a4705ed5b24db /src/options | |
parent | 2bf51317486cfbfc8c19e32256ca9727bfb2e42a (diff) |
First part of options refactoring (#6428)
This PR does a first round of refactoring and gets rid of a significant portion of generated code. In particular
- it removes options::optionName.wasSetByUser() (we still have Options::wasSetByUser())
- it removes options::optionName.set() (we still have Options::set())
- it removes options::optionName.getName() in favor of options::optionName.name
- it removes the specializations of Options::assign() and Options::assignBool() from the headers
- it eliminates runHandlerAndPredicates() and runBoolPredicates()
The removed methods are only used in few places with are changed to using Options::current().X() instead.
In the future, we also want to get rid of options::optionName() and use Options::operator[]() instead, and furthermore not use Options::current() but use the options from the Env object. This PR already adds Env::getOption() as a shorthand for Env::getOptions()[...] and uses it as a proof of concept within SmtEngine.
Diffstat (limited to 'src/options')
-rw-r--r-- | src/options/bv_options.toml | 1 | ||||
-rw-r--r-- | src/options/mkoptions.py | 159 | ||||
-rw-r--r-- | src/options/module_template.cpp | 2 | ||||
-rw-r--r-- | src/options/open_ostream.cpp | 1 | ||||
-rw-r--r-- | src/options/options.h | 51 | ||||
-rw-r--r-- | src/options/options_handler.cpp | 64 | ||||
-rw-r--r-- | src/options/options_public_functions.cpp | 2 | ||||
-rw-r--r-- | src/options/options_template.cpp | 9 |
8 files changed, 100 insertions, 189 deletions
diff --git a/src/options/bv_options.toml b/src/options/bv_options.toml index acb010a2e..18f190ff1 100644 --- a/src/options/bv_options.toml +++ b/src/options/bv_options.toml @@ -51,6 +51,7 @@ header = "options/bv_options.h" category = "expert" long = "bv-aig-simp=COMMAND" type = "std::string" + default = "\"balance;drw\"" predicates = ["abcEnabledBuild"] help = "abc command to run AIG simplifications (implies --bitblast-aig, default is \"balance;drw\")" diff --git a/src/options/mkoptions.py b/src/options/mkoptions.py index 9c66c6b61..fa2a39b04 100644 --- a/src/options/mkoptions.py +++ b/src/options/mkoptions.py @@ -81,63 +81,35 @@ g_getopt_long_start = 256 TPL_HOLDER_MACRO_NAME = 'CVC5_OPTIONS__{id}__FOR_OPTION_HOLDER' -TPL_RUN_HANDLER = \ -"""template <> options::{name}__option_t::type runHandlerAndPredicates( - options::{name}__option_t, - std::string option, - std::string optionarg, - options::OptionsHandler* handler) -{{ - options::{name}__option_t::type retval = {handler}; - {predicates} - return retval; -}}""" - -TPL_DECL_ASSIGN = \ +TPL_IMPL_ASSIGN = \ """template <> void Options::assign( options::{name}__option_t, std::string option, - std::string value);""" - -TPL_IMPL_ASSIGN = TPL_DECL_ASSIGN[:-1] + \ -""" + std::string optionarg) {{ - d_holder->{name} = - runHandlerAndPredicates(options::{name}, option, value, d_handler); + auto parsedval = {handler}; + {predicates} + d_holder->{name} = parsedval; d_holder->{name}__setByUser__ = true; Trace("options") << "user assigned option {name}" << std::endl; }}""" - -TPL_RUN_HANDLER_BOOL = \ -"""template <> void runBoolPredicates( - options::{name}__option_t, - std::string option, - bool b, - options::OptionsHandler* handler) -{{ - {predicates} -}}""" - -TPL_DECL_ASSIGN_BOOL = \ +TPL_IMPL_ASSIGN_BOOL = \ """template <> void Options::assignBool( options::{name}__option_t, std::string option, - bool value);""" - -TPL_IMPL_ASSIGN_BOOL = TPL_DECL_ASSIGN_BOOL[:-1] + \ -""" + bool value) {{ - runBoolPredicates(options::{name}, option, value, d_handler); + {predicates} d_holder->{name} = value; d_holder->{name}__setByUser__ = true; Trace("options") << "user assigned option {name}" << std::endl; }}""" TPL_CALL_ASSIGN_BOOL = \ - ' options->assignBool(options::{name}, {option}, {value});' + ' assignBool(options::{name}, {option}, {value});' -TPL_CALL_ASSIGN = ' options->assign(options::{name}, {option}, optionarg);' +TPL_CALL_ASSIGN = ' assign(options::{name}, {option}, optionarg);' TPL_CALL_SET_OPTION = 'setOption(std::string("{smtname}"), ("{value}"));' @@ -157,9 +129,7 @@ TPL_OPTION_STRUCT_RW = \ {{ typedef {type} type; type operator()() const; - bool wasSetByUser() const; - void set(const type& v); - const char* getName() const; + static constexpr const char* name = "{long_name}"; }} thread_local {name};""" TPL_OPTION_STRUCT_RO = \ @@ -167,20 +137,18 @@ TPL_OPTION_STRUCT_RO = \ {{ typedef {type} type; type operator()() const; - bool wasSetByUser() const; - const char* getName() const; + static constexpr const char* name = "{long_name}"; }} thread_local {name};""" TPL_DECL_SET = \ -"""template <> void Options::set( - options::{name}__option_t, - const options::{name}__option_t::type& x);""" +"""template <> options::{name}__option_t::type& Options::ref( + options::{name}__option_t);""" TPL_IMPL_SET = TPL_DECL_SET[:-1] + \ """ {{ - d_holder->{name} = x; + return d_holder->{name}; }}""" @@ -206,32 +174,12 @@ TPL_IMPL_WAS_SET_BY_USER = TPL_DECL_WAS_SET_BY_USER[:-1] + \ # Option specific methods -TPL_IMPL_OPTION_SET = \ -"""inline void {name}__option_t::set(const {name}__option_t::type& v) -{{ - Options::current()->set(*this, v); -}}""" - TPL_IMPL_OP_PAR = \ """inline {name}__option_t::type {name}__option_t::operator()() const {{ - return (*Options::current())[*this]; -}}""" - -TPL_IMPL_OPTION_WAS_SET_BY_USER = \ -"""inline bool {name}__option_t::wasSetByUser() const -{{ - return Options::current()->wasSetByUser(*this); -}}""" - -TPL_IMPL_GET_NAME = \ -"""inline const char* {name}__option_t::getName() const -{{ - return "{long_name}"; + return Options::current()[*this]; }}""" - - # Mode templates TPL_DECL_MODE_ENUM = \ """ @@ -242,16 +190,14 @@ enum class {type} TPL_DECL_MODE_FUNC = \ """ -std::ostream& -operator<<(std::ostream& os, {type} mode);""" +std::ostream& operator<<(std::ostream& os, {type} mode);""" TPL_IMPL_MODE_FUNC = TPL_DECL_MODE_FUNC[:-len(";")] + \ """ {{ - os << "{type}::"; switch(mode) {{{cases} default: - Unreachable(); + Unreachable(); }} return os; }} @@ -260,13 +206,11 @@ TPL_IMPL_MODE_FUNC = TPL_DECL_MODE_FUNC[:-len(";")] + \ TPL_IMPL_MODE_CASE = \ """ case {type}::{enum}: - os << "{enum}"; - break;""" + return os << "{type}::{enum}";""" TPL_DECL_MODE_HANDLER = \ """ -{type} -stringTo{type}(const std::string& option, const std::string& optarg);""" +{type} stringTo{type}(const std::string& optarg);""" TPL_IMPL_MODE_HANDLER = TPL_DECL_MODE_HANDLER[:-1] + \ """ @@ -274,14 +218,11 @@ TPL_IMPL_MODE_HANDLER = TPL_DECL_MODE_HANDLER[:-1] + \ {cases} else if (optarg == "help") {{ - puts({help}); - exit(1); - }} - else - {{ - throw OptionException(std::string("unknown option for --{long}: `") + - optarg + "'. Try --{long}=help."); + std::cerr << {help}; + std::exit(1); }} + throw OptionException(std::string("unknown option for --{long}: `") + + optarg + "'. Try --{long}=help."); }} """ @@ -513,7 +454,11 @@ def codegen_module(module, dst_dir, tpl_module_h, tpl_module_cpp): # Generate module declaration tpl_decl = TPL_OPTION_STRUCT_RO if option.read_only else TPL_OPTION_STRUCT_RW - decls.append(tpl_decl.format(name=option.name, type=option.type)) + if option.long: + long_name = option.long.split('=')[0] + else: + long_name = "" + decls.append(tpl_decl.format(name=option.name, type=option.type, long_name = long_name)) # Generate module specialization if not option.read_only: @@ -521,11 +466,6 @@ def codegen_module(module, dst_dir, tpl_module_h, tpl_module_cpp): specs.append(TPL_DECL_OP_BRACKET.format(name=option.name)) specs.append(TPL_DECL_WAS_SET_BY_USER.format(name=option.name)) - if option.type == 'bool': - specs.append(TPL_DECL_ASSIGN_BOOL.format(name=option.name)) - else: - specs.append(TPL_DECL_ASSIGN.format(name=option.name)) - if option.long and option.type not in ['bool', 'void'] and \ '=' not in option.long: die("module '{}': option '{}' with type '{}' needs an argument " \ @@ -539,15 +479,6 @@ def codegen_module(module, dst_dir, tpl_module_h, tpl_module_cpp): # Generate module inlines inls.append(TPL_IMPL_OP_PAR.format(name=option.name)) - inls.append(TPL_IMPL_OPTION_WAS_SET_BY_USER.format(name=option.name)) - if not option.read_only: - inls.append(TPL_IMPL_OPTION_SET.format(name=option.name)) - if option.long: - long_name = option.long.split('=')[0] - else: - long_name = "" - inls.append(TPL_IMPL_GET_NAME.format( - name=option.name, long_name=long_name)) ### Generate code for {module.name}_options.cpp @@ -704,12 +635,12 @@ def codegen_all_modules(modules, dst_dir, tpl_options, tpl_options_holder): handler = None if option.handler: if option.type == 'void': - handler = 'handler->{}(option)'.format(option.handler) + handler = 'd_handler->{}(option)'.format(option.handler) else: handler = \ - 'handler->{}(option, optionarg)'.format(option.handler) + 'd_handler->{}(option, optionarg)'.format(option.handler) elif option.mode: - handler = 'stringTo{}(option, optionarg)'.format(option.type) + handler = 'stringTo{}(optionarg)'.format(option.type) elif option.type != 'bool': handler = \ 'handleOption<{}>(option, optionarg)'.format(option.type) @@ -719,12 +650,12 @@ def codegen_all_modules(modules, dst_dir, tpl_options, tpl_options_holder): if option.predicates: if option.type == 'bool': predicates = \ - ['handler->{}(option, b);'.format(x) \ + ['d_handler->{}(option, value);'.format(x) \ for x in option.predicates] else: assert option.type != 'void' predicates = \ - ['handler->{}(option, retval);'.format(x) \ + ['d_handler->{}(option, parsedval);'.format(x) \ for x in option.predicates] # Generate options_handler and getopt_long @@ -867,24 +798,6 @@ def codegen_all_modules(modules, dst_dir, tpl_options, tpl_options_holder): options_getoptions.append(s) - # Define runBoolPredicates/runHandlerAndPredicates - tpl = None - if option.type == 'bool': - if predicates: - assert handler is None - tpl = TPL_RUN_HANDLER_BOOL - elif option.short or option.long: - assert option.type != 'void' - assert handler - tpl = TPL_RUN_HANDLER - if tpl: - custom_handlers.append( - tpl.format( - name=option.name, - handler=handler, - predicates='\n'.join(predicates) - )) - # Define handler assign/assignBool tpl = None if option.type == 'bool': @@ -893,7 +806,9 @@ def codegen_all_modules(modules, dst_dir, tpl_options, tpl_options_holder): tpl = TPL_IMPL_ASSIGN if tpl: custom_handlers.append(tpl.format( - name=option.name + name=option.name, + handler=handler, + predicates='\n'.join(predicates) )) # Default option values diff --git a/src/options/module_template.cpp b/src/options/module_template.cpp index 3b928dba0..0de77e8a6 100644 --- a/src/options/module_template.cpp +++ b/src/options/module_template.cpp @@ -19,6 +19,8 @@ #include "options/options_holder.h" #include "base/check.h" +#include <iostream> + // clang-format off namespace cvc5 { diff --git a/src/options/open_ostream.cpp b/src/options/open_ostream.cpp index 3b13c42e2..9ebea6da0 100644 --- a/src/options/open_ostream.cpp +++ b/src/options/open_ostream.cpp @@ -20,6 +20,7 @@ #include <cerrno> +#include <fstream> #include <iostream> #include <ostream> #include <sstream> diff --git a/src/options/options.h b/src/options/options.h index 67707c990..b249c90ed 100644 --- a/src/options/options.h +++ b/src/options/options.h @@ -18,8 +18,7 @@ #ifndef CVC5__OPTIONS__OPTIONS_H #define CVC5__OPTIONS__OPTIONS_H -#include <fstream> -#include <ostream> +#include <iosfwd> #include <string> #include <vector> @@ -77,9 +76,6 @@ class CVC5_EXPORT Options static std::string formatThreadOptionException(const std::string& option); - static const size_t s_maxoptlen = 128; - static const unsigned s_preemptAdditional = 6; - public: class OptionsScope { @@ -102,8 +98,8 @@ public: } /** Get the current Options in effect */ - static inline Options* current() { - return s_current; + static inline Options& current() { + return *s_current; } Options(OptionsListener* ol = nullptr); @@ -117,15 +113,39 @@ public: void copyValues(const Options& options); /** - * Set the value of the given option. Use of this default - * implementation causes a compile-time error; write-able - * options specialize this template with a real implementation. + * Set the value of the given option. Uses `ref()`, which causes a + * compile-time error if the given option is read-only. + */ + template <class T> + void set(T t, const typename T::type& val) { + ref(t) = val; + } + + /** + * Set the default value of the given option. Is equivalent to calling `set()` + * if `wasSetByUser()` returns false. Uses `ref()`, which causes a compile-time + * error if the given option is read-only. + */ + template <class T> + void setDefault(T t, const typename T::type& val) + { + if (!wasSetByUser(t)) + { + ref(t) = val; + } + } + + /** + * Get a non-const reference to the value of the given option. Causes a + * compile-time error if the given option is read-only. Writeable options + * specialize this template with a real implementation. */ template <class T> - void set(T, const typename T::type&) { - // Flag a compile-time error. Write-able options specialize - // this template to provide an implementation. - T::you_are_trying_to_assign_to_a_read_only_option; + typename T::type& ref(T) { + // Flag a compile-time error. + T::you_are_trying_to_get_nonconst_access_to_a_read_only_option; + // Ensure the compiler does not complain about the return value. + return *static_cast<typename T::type*>(nullptr); } /** @@ -297,8 +317,7 @@ public: * * Preconditions: options, extender and nonoptions are non-null. */ - static void parseOptionsRecursive(Options* options, - int argc, + void parseOptionsRecursive(int argc, char* argv[], std::vector<std::string>* nonoptions); }; /* class Options */ diff --git a/src/options/options_handler.cpp b/src/options/options_handler.cpp index 0e2315aa0..dd555ab56 100644 --- a/src/options/options_handler.cpp +++ b/src/options/options_handler.cpp @@ -159,14 +159,11 @@ void OptionsHandler::checkBvSatSolver(std::string option, SatSolverMode m) || m == SatSolverMode::KISSAT)) { if (options::bitblastMode() == options::BitblastMode::LAZY - && options::bitblastMode.wasSetByUser()) + && Options::current().wasSetByUser(options::bitblastMode)) { throwLazyBBUnsupported(m); } - if (!options::bitvectorToBool.wasSetByUser()) - { - options::bitvectorToBool.set(true); - } + Options::current().setDefault(options::bitvectorToBool, true); } } @@ -174,23 +171,10 @@ void OptionsHandler::checkBitblastMode(std::string option, BitblastMode m) { if (m == options::BitblastMode::LAZY) { - if (!options::bitvectorPropagate.wasSetByUser()) - { - options::bitvectorPropagate.set(true); - } - if (!options::bitvectorEqualitySolver.wasSetByUser()) - { - options::bitvectorEqualitySolver.set(true); - } - - if (!options::bitvectorInequalitySolver.wasSetByUser()) - { - options::bitvectorInequalitySolver.set(true); - } - if (!options::bitvectorAlgebraicSolver.wasSetByUser()) - { - options::bitvectorAlgebraicSolver.set(true); - } + Options::current().setDefault(options::bitvectorPropagate, true); + Options::current().setDefault(options::bitvectorEqualitySolver, true); + Options::current().setDefault(options::bitvectorInequalitySolver, true); + Options::current().setDefault(options::bitvectorAlgebraicSolver, true); if (options::bvSatSolver() != options::SatSolverMode::MINISAT) { throwLazyBBUnsupported(options::bvSatSolver()); @@ -198,27 +182,21 @@ void OptionsHandler::checkBitblastMode(std::string option, BitblastMode m) } else if (m == BitblastMode::EAGER) { - if (!options::bitvectorToBool.wasSetByUser()) - { - options::bitvectorToBool.set(true); - } + Options::current().setDefault(options::bitvectorToBool, true); } } void OptionsHandler::setBitblastAig(std::string option, bool arg) { if(arg) { - if(options::bitblastMode.wasSetByUser()) { + if(Options::current().wasSetByUser(options::bitblastMode)) { if (options::bitblastMode() != options::BitblastMode::EAGER) { throw OptionException("bitblast-aig must be used with eager bitblaster"); } } else { - options::BitblastMode mode = stringToBitblastMode("", "eager"); - options::bitblastMode.set(mode); - } - if(!options::bitvectorAigSimplifications.wasSetByUser()) { - options::bitvectorAigSimplifications.set("balance;drw"); + options::BitblastMode mode = stringToBitblastMode("eager"); + Options::current().set(options::bitblastMode, mode); } } } @@ -253,13 +231,13 @@ InstFormatMode OptionsHandler::stringToInstFormatMode(std::string option, // decision/options_handlers.h void OptionsHandler::setDecisionModeStopOnly(std::string option, DecisionMode m) { - options::decisionStopOnly.set(m == DecisionMode::RELEVANCY); + Options::current().set(options::decisionStopOnly, m == DecisionMode::RELEVANCY); } void OptionsHandler::setProduceAssertions(std::string option, bool value) { - options::produceAssertions.set(value); - options::interactiveMode.set(value); + Options::current().set(options::produceAssertions, value); + Options::current().set(options::interactiveMode, value); } void OptionsHandler::setStats(const std::string& option, bool value) @@ -278,22 +256,22 @@ void OptionsHandler::setStats(const std::string& option, bool value) std::string opt = option.substr(2); if (value) { - if (opt == options::statisticsAll.getName()) + if (opt == options::statisticsAll.name) { d_options->d_holder->statistics = true; } - else if (opt == options::statisticsEveryQuery.getName()) + else if (opt == options::statisticsEveryQuery.name) { d_options->d_holder->statistics = true; } - else if (opt == options::statisticsExpert.getName()) + else if (opt == options::statisticsExpert.name) { d_options->d_holder->statistics = true; } } else { - if (opt == options::statistics.getName()) + if (opt == options::statistics.name) { d_options->d_holder->statisticsAll = false; d_options->d_holder->statisticsEveryQuery = false; @@ -508,7 +486,7 @@ OutputLanguage OptionsHandler::stringToOutputLanguage(std::string option, std::string optarg) { if(optarg == "help") { - options::languageHelp.set(true); + Options::current().set(options::languageHelp, true); return language::output::LANG_AUTO; } @@ -526,7 +504,7 @@ InputLanguage OptionsHandler::stringToInputLanguage(std::string option, std::string optarg) { if(optarg == "help") { - options::languageHelp.set(true); + Options::current().set(options::languageHelp, true); return language::input::LANG_AUTO; } @@ -571,12 +549,12 @@ void OptionsHandler::setVerbosity(std::string option, int value) } void OptionsHandler::increaseVerbosity(std::string option) { - options::verbosity.set(options::verbosity() + 1); + Options::current().set(options::verbosity, options::verbosity() + 1); setVerbosity(option, options::verbosity()); } void OptionsHandler::decreaseVerbosity(std::string option) { - options::verbosity.set(options::verbosity() - 1); + Options::current().set(options::verbosity, options::verbosity() - 1); setVerbosity(option, options::verbosity()); } diff --git a/src/options/options_public_functions.cpp b/src/options/options_public_functions.cpp index f70c1ce3b..6ad537240 100644 --- a/src/options/options_public_functions.cpp +++ b/src/options/options_public_functions.cpp @@ -179,7 +179,7 @@ std::string Options::getBinaryName() const{ } std::ostream* Options::currentGetOut() { - return current()->getOut(); + return current().getOut(); } diff --git a/src/options/options_template.cpp b/src/options/options_template.cpp index f24f83b2b..4493f6094 100644 --- a/src/options/options_template.cpp +++ b/src/options/options_template.cpp @@ -408,7 +408,7 @@ std::vector<std::string> Options::parseOptions(Options* options, options->d_holder->binary_name = std::string(progName); std::vector<std::string> nonoptions; - parseOptionsRecursive(options, argc, argv, &nonoptions); + options->parseOptionsRecursive(argc, argv, &nonoptions); if(Debug.isOn("options")){ for(std::vector<std::string>::const_iterator i = nonoptions.begin(), iend = nonoptions.end(); i != iend; ++i){ @@ -419,8 +419,7 @@ std::vector<std::string> Options::parseOptions(Options* options, return nonoptions; } -void Options::parseOptionsRecursive(Options* options, - int argc, +void Options::parseOptionsRecursive(int argc, char* argv[], std::vector<std::string>* nonoptions) { @@ -434,9 +433,6 @@ void Options::parseOptionsRecursive(Options* options, } } - // Having this synonym simplifies the generation code in mkoptions. - options::OptionsHandler* handler = options->d_handler; - // Reset getopt(), in the case of multiple calls to parseOptions(). // This can be = 1 in newer GNU getopt, but older (< 2007) require = 0. optind = 0; @@ -597,7 +593,6 @@ void Options::setOptionInternal(const std::string& key, const std::string& optionarg) { options::OptionsHandler* handler = d_handler; - Options* options = this; ${setoption_handlers}$ throw UnrecognizedOptionException(key); } |