From 15d38800b9f493fcf4573160b420f0ab9563b4a8 Mon Sep 17 00:00:00 2001 From: Gereon Kremer Date: Fri, 28 May 2021 21:46:54 +0200 Subject: Add non-templated method to set option defaults (#6540) This PR replaces the templated Options::setDefault() methods by new non-templated free functions options::{module}::setDefault{option}(). These methods should be used instead of the common if (!set by user) { set option value } pattern. --- src/options/decision_options.toml | 2 +- src/options/mkoptions.py | 34 +++++++++++++++++++++++++--------- src/options/module_template.cpp | 8 ++++++++ src/options/module_template.h | 7 +++++++ src/options/options_handler.cpp | 12 ++++++------ src/options/options_template.h | 14 -------------- 6 files changed, 47 insertions(+), 30 deletions(-) diff --git a/src/options/decision_options.toml b/src/options/decision_options.toml index 796fd26fa..840eaa08f 100644 --- a/src/options/decision_options.toml +++ b/src/options/decision_options.toml @@ -33,7 +33,7 @@ name = "Decision Heuristics" name = "decisionThreshold" category = "expert" long = "decision-threshold=N" - type = "decision::DecisionWeight" + type = "cvc5::decision::DecisionWeight" default = "0" includes = ["options/decision_weight.h"] help = "ignore all nodes greater than threshold in first attempt to pick decision" diff --git a/src/options/mkoptions.py b/src/options/mkoptions.py index b99fbc1b6..9277fa8d9 100644 --- a/src/options/mkoptions.py +++ b/src/options/mkoptions.py @@ -89,7 +89,7 @@ TPL_IMPL_ASSIGN = \ auto parsedval = {handler}; {predicates} {module}.{name} = parsedval; - {module}.{name}__setByUser__ = true; + {module}.{name}__setByUser = true; Trace("options") << "user assigned option {name}" << std::endl; }}""" @@ -101,7 +101,7 @@ TPL_IMPL_ASSIGN_BOOL = \ {{ {predicates} {module}.{name} = value; - {module}.{name}__setByUser__ = true; + {module}.{name}__setByUser = true; Trace("options") << "user assigned option {name}" << std::endl; }}""" @@ -116,11 +116,19 @@ TPL_GETOPT_LONG = '{{ "{}", {}_argument, nullptr, {} }},' TPL_PUSHBACK_PREEMPT = 'extender->pushBackPreemption({});' -TPL_HOLDER_MACRO_ATTR = " {type} {name};\\\n" -TPL_HOLDER_MACRO_ATTR += " bool {name}__setByUser__ = false;" +TPL_HOLDER_MACRO_ATTR = ''' {type} {name}; + bool {name}__setByUser = false;''' -TPL_HOLDER_MACRO_ATTR_DEF = " {type} {name} = {default};\\\n" -TPL_HOLDER_MACRO_ATTR_DEF += " bool {name}__setByUser__ = false;" +TPL_HOLDER_MACRO_ATTR_DEF = ''' {type} {name} = {default}; + bool {name}__setByUser = false;''' + +TPL_DECL_SET_DEFAULT = 'void setDefault{funcname}(Options& opts, {type} value);' +TPL_IMPL_SET_DEFAULT = TPL_DECL_SET_DEFAULT[:-1] + ''' +{{ + if (!opts.{module}.{name}__setByUser) {{ + opts.{module}.{name} = value; + }} +}}''' TPL_NAME_DECL = 'static constexpr const char* {name}__name = "{long_name}";' @@ -152,14 +160,13 @@ TPL_IMPL_OP_BRACKET = TPL_DECL_OP_BRACKET[:-1] + \ return {module}.{name}; }}""" - TPL_DECL_WAS_SET_BY_USER = \ """template <> bool Options::wasSetByUser(options::{name}__option_t) const;""" TPL_IMPL_WAS_SET_BY_USER = TPL_DECL_WAS_SET_BY_USER[:-1] + \ """ {{ - return {module}.{name}__setByUser__; + return {module}.{name}__setByUser; }}""" # Option specific methods @@ -566,6 +573,8 @@ def codegen_module(module, dst_dir, tpl_module_h, tpl_module_cpp): decls = [] specs = [] inls = [] + default_decl = [] + default_impl = [] mode_decl = [] mode_impl = [] @@ -599,7 +608,10 @@ def codegen_module(module, dst_dir, tpl_module_h, tpl_module_cpp): decls.append(tpl_decl.format(name=option.name, type=option.type, long_name = long_name)) option_names.append(TPL_NAME_DECL.format(name=option.name, type=option.type, long_name = long_name)) + capoptionname = option.name[0].capitalize() + option.name[1:] + # Generate module specialization + default_decl.append(TPL_DECL_SET_DEFAULT.format(module=module.id, name=option.name, funcname=capoptionname, type=option.type)) specs.append(TPL_DECL_SET.format(name=option.name)) specs.append(TPL_DECL_OP_BRACKET.format(name=option.name)) specs.append(TPL_DECL_WAS_SET_BY_USER.format(name=option.name)) @@ -622,6 +634,7 @@ def codegen_module(module, dst_dir, tpl_module_h, tpl_module_cpp): ### Generate code for {module.name}_options.cpp # Accessors + default_impl.append(TPL_IMPL_SET_DEFAULT.format(module=module.id, name=option.name, funcname=capoptionname, type=option.type)) accs.append(TPL_IMPL_SET.format(module=module.id, name=option.name)) accs.append(TPL_IMPL_OP_BRACKET.format(module=module.id, name=option.name)) accs.append(TPL_IMPL_WAS_SET_BY_USER.format(module=module.id, name=option.name)) @@ -674,11 +687,14 @@ def codegen_module(module, dst_dir, tpl_module_h, tpl_module_cpp): specs='\n'.join(specs), option_names='\n'.join(option_names), inls='\n'.join(inls), + defaults='\n'.join(default_decl), modes=''.join(mode_decl))) write_file(dst_dir, '{}.cpp'.format(filename), tpl_module_cpp.format( header=module.header, + id=module.id, accs='\n'.join(accs), + defaults='\n'.join(default_impl), defs='\n'.join(defs), modes=''.join(mode_impl))) @@ -959,7 +975,7 @@ def codegen_all_modules(modules, build_dir, dst_dir, tpl_options_h, tpl_options_ if option.mode and option.type not in default: default = '{}::{}'.format(option.type, default) defaults.append('{}({})'.format(option.name, default)) - defaults.append('{}__setByUser__(false)'.format(option.name)) + defaults.append('{}__setByUser(false)'.format(option.name)) write_file(dst_dir, 'options.h', tpl_options_h.format( holder_fwd_decls=get_holder_fwd_decls(modules), diff --git a/src/options/module_template.cpp b/src/options/module_template.cpp index c79656e4b..bc953b952 100644 --- a/src/options/module_template.cpp +++ b/src/options/module_template.cpp @@ -33,6 +33,14 @@ ${defs}$ ${modes}$ + +namespace ${id}$ +{ +// clang-format off +${defaults}$ +// clang-format on +} + } // namespace options } // namespace cvc5 // clang-format on diff --git a/src/options/module_template.h b/src/options/module_template.h index 219775dd6..722490948 100644 --- a/src/options/module_template.h +++ b/src/options/module_template.h @@ -71,6 +71,13 @@ namespace options { ${inls}$ // clang-format on +namespace ${id}$ +{ +// clang-format off +${defaults}$ +// clang-format on +} + } // namespace options } // namespace cvc5 diff --git a/src/options/options_handler.cpp b/src/options/options_handler.cpp index a6ddbec1e..7d9fcffab 100644 --- a/src/options/options_handler.cpp +++ b/src/options/options_handler.cpp @@ -163,7 +163,7 @@ void OptionsHandler::checkBvSatSolver(std::string option, SatSolverMode m) { throwLazyBBUnsupported(m); } - Options::current().setDefault(options::bitvectorToBool, true); + options::bv::setDefaultBitvectorToBool(*d_options, true); } } @@ -171,10 +171,10 @@ void OptionsHandler::checkBitblastMode(std::string option, BitblastMode m) { if (m == options::BitblastMode::LAZY) { - Options::current().setDefault(options::bitvectorPropagate, true); - Options::current().setDefault(options::bitvectorEqualitySolver, true); - Options::current().setDefault(options::bitvectorInequalitySolver, true); - Options::current().setDefault(options::bitvectorAlgebraicSolver, true); + options::bv::setDefaultBitvectorPropagate(*d_options, true); + options::bv::setDefaultBitvectorEqualitySolver(*d_options, true); + options::bv::setDefaultBitvectorInequalitySolver(*d_options, true); + options::bv::setDefaultBitvectorAlgebraicSolver(*d_options, true); if (options::bvSatSolver() != options::SatSolverMode::MINISAT) { throwLazyBBUnsupported(options::bvSatSolver()); @@ -182,7 +182,7 @@ void OptionsHandler::checkBitblastMode(std::string option, BitblastMode m) } else if (m == BitblastMode::EAGER) { - Options::current().setDefault(options::bitvectorToBool, true); + options::bv::setDefaultBitvectorToBool(*d_options, true); } } diff --git a/src/options/options_template.h b/src/options/options_template.h index 9d5e70099..f5ea87c54 100644 --- a/src/options/options_template.h +++ b/src/options/options_template.h @@ -132,20 +132,6 @@ public: 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 - 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 -- cgit v1.2.3