Remove setDefaults methods (#7413)

This PR removes some auto-generated utility methods to set an option if it has not been set by the user. It was once added as we thought it might be useful, but we do not actually use it.

diff --git a/src/options/mkoptions.py b/src/options/mkoptions.py
index a8f631de64d09f709f9aa9bd47000a332089a0bf..57f8b64e63a36041d61728583939fd858c314acd 100644 (file)
--- 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 ee5260f34f14a4652ac32b39427c9165d2f33171..d2ece3f1310ba25358dc681bb151c09575ca0bb7 100644 (file)
--- 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 61d689b7209c6bbc0b983dab8e351b27b95a17c9..d9b591f1110b929a583579063ae875d13242b9b4 100644 (file)
--- 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 93b08a858f573b874804266dcb0ddab265d2ab41..ec6c831e437770797f1fe083bfa0c1bdec293671 100644 (file)
--- 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;
+    }
   }
 }