diff options
| -rw-r--r-- | src/options/mkoptions.py | 34 | ||||
| -rw-r--r-- | src/options/module_template.cpp | 7 | ||||
| -rw-r--r-- | src/options/module_template.h | 2 | ||||
| -rw-r--r-- | src/options/options_handler.cpp | 5 |
4 files changed, 4 insertions, 44 deletions
diff --git a/src/options/mkoptions.py b/src/options/mkoptions.py index a8f631de6..57f8b64e6 100644 --- a/src/options/mkoptions.py +++ b/src/options/mkoptions.py @@ -480,17 +480,6 @@ def generate_module_option_names(module): 'static constexpr const char* {name}__name = "{long_name}";', relevant) -def generate_module_setdefaults_decl(module): - res = [] - for option in module.options: - if option.name is None: - continue - funcname = option.name[0].capitalize() + option.name[1:] - res.append('void setDefault{}(Options& opts, {} value);'.format( - funcname, option.type)) - return '\n'.join(res) - - ################################################################################ # for options/<module>.cpp @@ -581,27 +570,6 @@ def generate_module_mode_impl(module): return '\n'.join(res) -TPL_SETDEFAULT_IMPL = '''void setDefault{capname}(Options& opts, {type} value) -{{ - if (!opts.{module}.{name}WasSetByUser) opts.{module}.{name} = value; -}}''' - - -def generate_module_setdefaults_impl(module): - res = [] - for option in module.options: - if option.name is None: - continue - fmt = { - 'capname': option.name[0].capitalize() + option.name[1:], - 'type': option.type, - 'module': module.id, - 'name': option.name, - } - res.append(TPL_SETDEFAULT_IMPL.format(**fmt)) - return '\n'.join(res) - - ################################################################################ # for main/options.cpp @@ -875,11 +843,9 @@ def codegen_module(module, dst_dir, tpls): 'holder_decl': generate_module_holder_decl(module), 'wrapper_functions': generate_module_wrapper_functions(module), 'option_names': generate_module_option_names(module), - 'setdefaults_decl': generate_module_setdefaults_decl(module), # module source 'header': module.header, 'modes_impl': generate_module_mode_impl(module), - 'setdefaults_impl': generate_module_setdefaults_impl(module), } for tpl in tpls: filename = tpl['output'].replace('module', module.filename) diff --git a/src/options/module_template.cpp b/src/options/module_template.cpp index ee5260f34..d2ece3f13 100644 --- a/src/options/module_template.cpp +++ b/src/options/module_template.cpp @@ -28,11 +28,4 @@ namespace cvc5::options { ${modes_impl}$ // clang-format on -namespace ${id}$ -{ -// clang-format off -${setdefaults_impl}$ -// clang-format on -} - } // namespace cvc5::options diff --git a/src/options/module_template.h b/src/options/module_template.h index 61d689b72..d9b591f11 100644 --- a/src/options/module_template.h +++ b/src/options/module_template.h @@ -56,8 +56,6 @@ namespace ${id}$ { // clang-format off ${option_names}$ - -${setdefaults_decl}$ // clang-format on } diff --git a/src/options/options_handler.cpp b/src/options/options_handler.cpp index 93b08a858..ec6c831e4 100644 --- a/src/options/options_handler.cpp +++ b/src/options/options_handler.cpp @@ -387,7 +387,10 @@ void OptionsHandler::checkBvSatSolver(const std::string& option, + " does not support lazy bit-blasting.\n" + "Try --bv-sat-solver=minisat"); } - options::bv::setDefaultBitvectorToBool(*d_options, true); + if (!d_options->bv.bitvectorToBoolWasSetByUser) + { + d_options->bv.bitvectorToBool = true; + } } } |