Simplify generation of option module code. (#6995)

This commit simplifies both the code that generates the option modules and the generated code itself. It removes placeholders in the templates that are no longer used, gets rid of the option holder types (and replaces them by simple inline functions) and does some clean up on the related code in the `mkoptions.py` script.

diff --git a/src/options/mkoptions.py b/src/options/mkoptions.py
index ec5eda17e832a5270ac4044a058bc6887eb250e3..edc0f88f4d9c26d865fb899ef4349adf90ac448f 100644 (file)
--- a/src/options/mkoptions.py
+++ b/src/options/mkoptions.py
@@ -110,56 +110,37 @@ TPL_IMPL_SET_DEFAULT = TPL_DECL_SET_DEFAULT[:-1] + '''
 
 TPL_NAME_DECL = 'static constexpr const char* {name}__name = "{long_name}";'
 
-TPL_OPTION_STRUCT_RW = \
-"""extern struct {name}__option_t
-{{
-  typedef {type} type;
-  type operator()() const;
-}} thread_local {name};"""
-
 # Option specific methods
 
-TPL_IMPL_OP_PAR = \
-"""inline {type} {name}__option_t::operator()() const
-{{ return Options::current().{module}.{name}; }}"""
+TPL_IMPL_OP_PAR = 'inline {type} {name}() {{ return Options::current().{module}.{name}; }}'
 
 # Mode templates
-TPL_DECL_MODE_ENUM = \
-"""
+TPL_DECL_MODE_ENUM = '''
 enum class {type}
 {{
   {values}
 }};
 
 static constexpr size_t {type}__numValues = {nvalues};
-"""
+'''
 
-TPL_DECL_MODE_FUNC = \
-"""
-std::ostream& operator<<(std::ostream& os, {type} mode);"""
-
-TPL_IMPL_MODE_FUNC = TPL_DECL_MODE_FUNC[:-len(";")] + \
-"""
+TPL_DECL_MODE_FUNC = 'std::ostream& operator<<(std::ostream& os, {type} mode);'
+TPL_IMPL_MODE_FUNC = TPL_DECL_MODE_FUNC[:-1] + '''
 {{
   switch(mode) {{{cases}
     default:
       Unreachable();
   }}
   return os;
-}}
-"""
+}}'''
 
 TPL_IMPL_MODE_CASE = \
 """
     case {type}::{enum}:
       return os << "{type}::{enum}";"""
 
-TPL_DECL_MODE_HANDLER = \
-"""
-{type} stringTo{type}(const std::string& optarg);"""
-
-TPL_IMPL_MODE_HANDLER = TPL_DECL_MODE_HANDLER[:-1] + \
-"""
+TPL_DECL_MODE_HANDLER = '{type} stringTo{type}(const std::string& optarg);'
+TPL_IMPL_MODE_HANDLER = TPL_DECL_MODE_HANDLER[:-1] + '''
 {{
   {cases}
   else if (optarg == "help")
@@ -169,8 +150,7 @@ TPL_IMPL_MODE_HANDLER = TPL_DECL_MODE_HANDLER[:-1] + \
   }}
   throw OptionException(std::string("unknown option for --{long}: `") +
                         optarg + "'.  Try --{long}=help.");
-}}
-"""
+}}'''
 
 TPL_MODE_HANDLER_CASE = \
 """if (optarg == "{name}")
@@ -559,18 +539,12 @@ def codegen_module(module, dst_dir, tpls):
     includes = set()
     holder_specs = []
     option_names = []
-    decls = []
-    specs = []
-    inls = []
+    wrap_funs = []
     default_decl = []
     default_impl = []
     mode_decl = []
     mode_impl = []
 
-    # *_options_.cpp
-    accs = []
-    defs = []
-
     for option in \
         sorted(module.options, key=lambda x: x.long if x.long else x.name):
         if option.name is None:
@@ -589,12 +563,10 @@ def codegen_module(module, dst_dir, tpls):
             holder_specs.append(TPL_HOLDER_MACRO_ATTR.format(type=option.type, name=option.name))
 
         # Generate module declaration
-        tpl_decl = TPL_OPTION_STRUCT_RW
         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))
         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:]
@@ -614,7 +586,7 @@ def codegen_module(module, dst_dir, tpls):
                     module.id, option.long, option.type))
 
         # Generate module inlines
-        inls.append(TPL_IMPL_OP_PAR.format(module=module.id, name=option.name, type=option.type))
+        wrap_funs.append(TPL_IMPL_OP_PAR.format(module=module.id, name=option.name, type=option.type))
 
 
         ### Generate code for {module.name}_options.cpp
@@ -622,9 +594,6 @@ def codegen_module(module, dst_dir, tpls):
         # Accessors
         default_impl.append(TPL_IMPL_SET_DEFAULT.format(module=module.id, name=option.name, funcname=capoptionname, type=option.type))
 
-        # Global definitions
-        defs.append('thread_local struct {name}__option_t {name};'.format(name=option.name))
-
         if option.mode:
             values = option.mode.keys()
             mode_decl.append(
@@ -670,16 +639,12 @@ def codegen_module(module, dst_dir, tpls):
         'id': module.id,
         'includes': '\n'.join(sorted(list(includes))),
         'holder_spec': '\n'.join(holder_specs),
-        'decls': '\n'.join(decls),
-        'specs': '\n'.join(specs),
         'option_names': '\n'.join(option_names),
-        'inls': '\n'.join(inls),
-        'defaults_decl': '\n'.join(default_decl),
+        'wrap_funs': '\n'.join(wrap_funs),
+        'defaults_decl': ''.join(default_decl),
         'modes_decl': '\n'.join(mode_decl),
         'header': module.header,
-        'accs': '\n'.join(accs),
         'defaults_impl': '\n'.join(default_impl),
-        'defs': '\n'.join(defs),
         'modes_impl': '\n'.join(mode_impl),
     }
 

diff --git a/src/options/module_template.cpp b/src/options/module_template.cpp
index 0d5e2d4ee4686dd0e52b81fb21dc5f73f4a0ef48..97b31df16a4c8ee14cbc257457fb07f43f01987d 100644 (file)
--- a/src/options/module_template.cpp
+++ b/src/options/module_template.cpp
@@ -23,17 +23,10 @@
 #include "options/option_exception.h"
 
 // clang-format off
-namespace cvc5 {
-
-${accs}$
-
-namespace options {
-
-${defs}$
+namespace cvc5::options {
 
 ${modes_impl}$
 
-
 namespace ${id}$
 {
 // clang-format off
@@ -41,6 +34,5 @@ ${defaults_impl}$
 // clang-format on
 }
 
-}  // namespace options
-}  // namespace cvc5
+}  // namespace cvc5::options
 // clang-format on

diff --git a/src/options/module_template.h b/src/options/module_template.h
index a0719ea328e9140ad6d3f292d5912c8c6f278320..3a8e2a9810cf2623c4bec2015563def156eb65f0 100644 (file)
--- a/src/options/module_template.h
+++ b/src/options/module_template.h
@@ -27,8 +27,7 @@ ${visibility_include}$
 ${includes}$
 // clang-format on
 
-namespace cvc5 {
-namespace options {
+namespace cvc5::options {
 
 // clang-format off
 ${modes_decl}$
@@ -50,35 +49,18 @@ ${holder_spec}$
 #undef DO_SEMANTIC_CHECKS_BY_DEFAULT
 
 // clang-format off
-${decls}$
+${wrap_funs}$
 // clang-format on
 
 namespace ${id}$
 {
 // clang-format off
 ${option_names}$
-// clang-format on
-}
-
-}  // namespace options
-
-// clang-format off
-${specs}$
-// clang-format on
 
-namespace options {
-// clang-format off
-${inls}$
-// clang-format on
-
-namespace ${id}$
-{
-// clang-format off
 ${defaults_decl}$
 // clang-format on
 }
 
-}  // namespace options
-}  // namespace cvc5
+}  // namespace cvc5::options
 
 #endif /* CVC5__OPTIONS__${id_cap}$_H */