Split options holder class (#6527)

This PR splits the OptionsHolder class into separate holder classes for every options module and makes them directly accessible via appropriate Options::<module>() methods. We forward declare these new holder classes and thereby retain that we only need to recompile when we change an option module that is explicitly included.
All (generated) methods that previously accessed the old holder object are changed to instead use the new holder objects.
This PR does the bare minimum to do this change, further PRs will eventually get rid of all template specializations that currently surround our options class.

10 files changed, 128 insertions, 108 deletions

diff --git a/src/options/CMakeLists.txt b/src/options/CMakeLists.txt
index 38f68461b..078c2ad31 100644
--- a/src/options/CMakeLists.txt
+++ b/src/options/CMakeLists.txt
@@ -27,7 +27,6 @@ libcvc5_add_sources(
   open_ostream.h
   option_exception.cpp
   option_exception.h
-  options.h
   options_handler.cpp
   options_handler.h
   options_listener.h
@@ -67,13 +66,13 @@ set(options_toml_files
 string(REPLACE "toml" "cpp;" options_gen_cpp_files ${options_toml_files})
 string(REPLACE "toml" "h;"   options_gen_h_files ${options_toml_files})
 
-libcvc5_add_sources(GENERATED options.cpp ${options_gen_cpp_files})
+libcvc5_add_sources(GENERATED options.h options.cpp ${options_gen_cpp_files})
 
 list_prepend(options_toml_files "${CMAKE_CURRENT_LIST_DIR}/" abs_toml_files)
 
 add_custom_command(
     OUTPUT
-      options.cpp options_holder.h
+      options.h options.cpp
       ${options_gen_cpp_files} ${options_gen_h_files}
     COMMAND
       ${PYTHON_EXECUTABLE}
@@ -86,14 +85,14 @@ add_custom_command(
       ${options_toml_files}
       module_template.h
       module_template.cpp
-      options_holder_template.h
+      options_template.h
       options_template.cpp
 )
 
 add_custom_target(gen-options
   DEPENDS
+    options.h
     options.cpp
-    options_holder.h
     ${options_gen_cpp_files}
     ${options_gen_h_files}
 )
diff --git a/src/options/mkoptions.py b/src/options/mkoptions.py
index 74e8d690d..a9ef65899 100644
--- a/src/options/mkoptions.py
+++ b/src/options/mkoptions.py
@@ -79,8 +79,6 @@ g_getopt_long_start = 256
 
 ### Source code templates
 
-TPL_HOLDER_MACRO_NAME = 'CVC5_OPTIONS__{id}__FOR_OPTION_HOLDER'
-
 TPL_IMPL_ASSIGN = \
 """template <> void Options::assign(
     options::{name}__option_t,
@@ -89,8 +87,8 @@ TPL_IMPL_ASSIGN = \
 {{
   auto parsedval = {handler};
   {predicates}
-  d_holder->{name} = parsedval;
-  d_holder->{name}__setByUser__ = true;
+  {module}().{name} = parsedval;
+  {module}().{name}__setByUser__ = true;
   Trace("options") << "user assigned option {name}" << std::endl;
 }}"""
 
@@ -101,8 +99,8 @@ TPL_IMPL_ASSIGN_BOOL = \
     bool value)
 {{
   {predicates}
-  d_holder->{name} = value;
-  d_holder->{name}__setByUser__ = true;
+  {module}().{name} = value;
+  {module}().{name}__setByUser__ = true;
   Trace("options") << "user assigned option {name}" << std::endl;
 }}"""
 
@@ -117,13 +115,10 @@ TPL_GETOPT_LONG = '{{ "{}", {}_argument, nullptr, {} }},'
 
 TPL_PUSHBACK_PREEMPT = 'extender->pushBackPreemption({});'
 
-
-TPL_HOLDER_MACRO = '#define ' + TPL_HOLDER_MACRO_NAME
-
-TPL_HOLDER_MACRO_ATTR = "  {name}__option_t::type {name};\\\n"
+TPL_HOLDER_MACRO_ATTR = "  {type} {name};\\\n"
 TPL_HOLDER_MACRO_ATTR += "  bool {name}__setByUser__ = false;"
 
-TPL_HOLDER_MACRO_ATTR_DEF = "  {name}__option_t::type {name} = {default};\\\n"
+TPL_HOLDER_MACRO_ATTR_DEF = "  {type} {name} = {default};\\\n"
 TPL_HOLDER_MACRO_ATTR_DEF += "  bool {name}__setByUser__ = false;"
 
 TPL_OPTION_STRUCT_RW = \
@@ -141,7 +136,7 @@ TPL_DECL_SET = \
 TPL_IMPL_SET = TPL_DECL_SET[:-1] + \
 """
 {{
-    return d_holder->{name};
+    return {module}().{name};
 }}"""
 
 
@@ -152,7 +147,7 @@ TPL_DECL_OP_BRACKET = \
 TPL_IMPL_OP_BRACKET = TPL_DECL_OP_BRACKET[:-1] + \
 """
 {{
-  return d_holder->{name};
+  return {module}().{name};
 }}"""
 
 
@@ -162,7 +157,7 @@ TPL_DECL_WAS_SET_BY_USER = \
 TPL_IMPL_WAS_SET_BY_USER = TPL_DECL_WAS_SET_BY_USER[:-1] + \
 """
 {{
-  return d_holder->{name}__setByUser__;
+  return {module}().{name}__setByUser__;
 }}"""
 
 # Option specific methods
@@ -225,6 +220,42 @@ TPL_MODE_HANDLER_CASE = \
     return {type}::{enum};
   }}"""
 
+def concat_format(s, objs):
+    """Helper method to render a string for a list of object"""
+    return '\n'.join([s.format(**o.__dict__) for o in objs])
+
+
+def get_holder_fwd_decls(modules):
+    """Render forward declaration of holder structs"""
+    return concat_format('  struct Holder{id_cap};', modules)
+
+
+def get_holder_mem_decls(modules):
+    """Render declarations of holder members of the Option class"""
+    return concat_format('    std::unique_ptr<options::Holder{id_cap}> d_{id};', modules)
+
+
+def get_holder_mem_inits(modules):
+    """Render initializations of holder members of the Option class"""
+    return concat_format('        d_{id}(std::make_unique<options::Holder{id_cap}>()),', modules)
+
+
+def get_holder_mem_copy(modules):
+    """Render copy operation of holder members of the Option class"""
+    return concat_format('      *d_{id} = *options.d_{id};', modules)
+
+
+def get_holder_getter_decls(modules):
+    """Render getter declarations for holder members of the Option class"""
+    return concat_format('''  const options::Holder{id_cap}& {id}() const;
+  options::Holder{id_cap}& {id}();''', modules)
+
+
+def get_holder_getter_impl(modules):
+    """Render getter implementations for holder members of the Option class"""
+    return concat_format('''const options::Holder{id_cap}& Options::{id}() const {{ return *d_{id}; }}
+options::Holder{id_cap}& Options::{id}() {{ return *d_{id}; }}''', modules)
+
 
 class Module(object):
     """Options module.
@@ -432,8 +463,6 @@ def codegen_module(module, dst_dir, tpl_module_h, tpl_module_cpp):
     accs = []
     defs = []
 
-    holder_specs.append(TPL_HOLDER_MACRO.format(id=module.id))
-
     for option in \
         sorted(module.options, key=lambda x: x.long if x.long else x.name):
         if option.name is None:
@@ -447,9 +476,9 @@ def codegen_module(module, dst_dir, tpl_module_h, tpl_module_cpp):
             default = option.default
             if option.mode and option.type not in default:
                 default = '{}::{}'.format(option.type, default)
-            holder_specs.append(TPL_HOLDER_MACRO_ATTR_DEF.format(name=option.name, default=default))
+            holder_specs.append(TPL_HOLDER_MACRO_ATTR_DEF.format(type=option.type, name=option.name, default=default))
         else:
-            holder_specs.append(TPL_HOLDER_MACRO_ATTR.format(name=option.name))
+            holder_specs.append(TPL_HOLDER_MACRO_ATTR.format(type=option.type, name=option.name))
 
         # Generate module declaration
         tpl_decl = TPL_OPTION_STRUCT_RW
@@ -482,9 +511,9 @@ def codegen_module(module, dst_dir, tpl_module_h, tpl_module_cpp):
         ### Generate code for {module.name}_options.cpp
 
         # Accessors
-        accs.append(TPL_IMPL_SET.format(name=option.name))
-        accs.append(TPL_IMPL_OP_BRACKET.format(name=option.name))
-        accs.append(TPL_IMPL_WAS_SET_BY_USER.format(name=option.name))
+        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))
 
         # Global definitions
         defs.append('thread_local struct {name}__option_t {name};'.format(name=option.name))
@@ -593,14 +622,13 @@ def add_getopt_long(long_name, argument_req, getopt_long):
             'required' if argument_req else 'no', value))
 
 
-def codegen_all_modules(modules, dst_dir, tpl_options, tpl_options_holder):
+def codegen_all_modules(modules, dst_dir, tpl_options_h, tpl_options_cpp):
     """
     Generate code for all option modules (options.cpp, options_holder.h).
     """
 
     headers_module = []      # generated *_options.h header includes
     headers_handler = set()  # option includes (for handlers, predicates, ...)
-    macros_module = []       # option holder macro for options_holder.h
     getopt_short = []        # short options for getopt_long
     getopt_long = []         # long options for getopt_long
     options_smt = []         # all options names accessible via {set,get}-option
@@ -615,7 +643,6 @@ def codegen_all_modules(modules, dst_dir, tpl_options, tpl_options_holder):
 
     for module in modules:
         headers_module.append(format_include(module.header))
-        macros_module.append(TPL_HOLDER_MACRO_NAME.format(id=module.id))
 
         if module.options:
             help_others.append(
@@ -780,14 +807,14 @@ def codegen_all_modules(modules, dst_dir, tpl_options, tpl_options_holder):
                     options_smt.append('"{}",'.format(optname))
 
                     if option.type == 'bool':
-                        s = 'opts.push_back({{"{}", d_holder->{} ? "true" : "false"}});'.format(
-                            optname, option.name)
+                        s = 'opts.push_back({{"{}", {}().{} ? "true" : "false"}});'.format(
+                            optname, module.id, option.name)
                     elif is_numeric_cpp_type(option.type):
-                        s = 'opts.push_back({{"{}", std::to_string(d_holder->{})}});'.format(
-                            optname, option.name)
+                        s = 'opts.push_back({{"{}", std::to_string({}().{})}});'.format(
+                            optname, module.id, option.name)
                     else:
-                        s = '{{ std::stringstream ss; ss << d_holder->{}; opts.push_back({{"{}", ss.str()}}); }}'.format(
-                            option.name, optname)
+                        s = '{{ std::stringstream ss; ss << {}().{}; opts.push_back({{"{}", ss.str()}}); }}'.format(
+                            module.id, option.name, optname)
                     options_getoptions.append(s)
 
 
@@ -799,6 +826,7 @@ def codegen_all_modules(modules, dst_dir, tpl_options, tpl_options_holder):
                     tpl = TPL_IMPL_ASSIGN
                 if tpl:
                     custom_handlers.append(tpl.format(
+                        module=module.id,
                         name=option.name,
                         handler=handler,
                         predicates='\n'.join(predicates)
@@ -812,14 +840,18 @@ def codegen_all_modules(modules, dst_dir, tpl_options, tpl_options_holder):
                 defaults.append('{}({})'.format(option.name, default))
                 defaults.append('{}__setByUser__(false)'.format(option.name))
 
-    write_file(dst_dir, 'options_holder.h', tpl_options_holder.format(
-        headers_module='\n'.join(headers_module),
-        macros_module='\n  '.join(macros_module)
+    write_file(dst_dir, 'options.h', tpl_options_h.format(
+        holder_fwd_decls=get_holder_fwd_decls(modules),
+        holder_getter_decls=get_holder_getter_decls(modules),
+        holder_mem_decls=get_holder_mem_decls(modules),
     ))
 
-    write_file(dst_dir, 'options.cpp', tpl_options.format(
+    write_file(dst_dir, 'options.cpp', tpl_options_cpp.format(
         headers_module='\n'.join(headers_module),
         headers_handler='\n'.join(sorted(list(headers_handler))),
+        holder_getter_impl=get_holder_getter_impl(modules),
+        holder_mem_copy=get_holder_mem_copy(modules),
+        holder_mem_inits=get_holder_mem_inits(modules),
         custom_handlers='\n'.join(custom_handlers),
         module_defaults=',\n  '.join(defaults),
         help_common='\n'.join(help_common),
@@ -977,8 +1009,8 @@ def mkoptions_main():
     # Read source code template files from source directory.
     tpl_module_h = read_tpl(src_dir, 'module_template.h')
     tpl_module_cpp = read_tpl(src_dir, 'module_template.cpp')
-    tpl_options = read_tpl(src_dir, 'options_template.cpp')
-    tpl_options_holder = read_tpl(src_dir, 'options_holder_template.h')
+    tpl_options_h = read_tpl(src_dir, 'options_template.h')
+    tpl_options_cpp = read_tpl(src_dir, 'options_template.cpp')
 
     # Parse files, check attributes and create module/option objects
     modules = []
@@ -1002,7 +1034,7 @@ def mkoptions_main():
         codegen_module(module, dst_dir, tpl_module_h, tpl_module_cpp)
 
     # Create options.cpp and options_holder.h in destination directory
-    codegen_all_modules(modules, dst_dir, tpl_options, tpl_options_holder)
+    codegen_all_modules(modules, dst_dir, tpl_options_h, tpl_options_cpp)
 
 
 
diff --git a/src/options/module_template.cpp b/src/options/module_template.cpp
index 0a4d594b2..c79656e4b 100644
--- a/src/options/module_template.cpp
+++ b/src/options/module_template.cpp
@@ -21,7 +21,6 @@
 
 #include "base/check.h"
 #include "options/option_exception.h"
-#include "options/options_holder.h"
 
 // clang-format off
 namespace cvc5 {
diff --git a/src/options/module_template.h b/src/options/module_template.h
index b668a1e3f..4e031d843 100644
--- a/src/options/module_template.h
+++ b/src/options/module_template.h
@@ -25,25 +25,46 @@
 
 // clang-format off
 ${includes}$
-
-${holder_spec}$
+// clang-format on
 
 namespace cvc5 {
 namespace options {
 
+// clang-format off
 ${modes}$
+// clang-format on
 
+#if defined(CVC5_MUZZLED) || defined(CVC5_COMPETITION_MODE)
+#  define DO_SEMANTIC_CHECKS_BY_DEFAULT false
+#else /* CVC5_MUZZLED || CVC5_COMPETITION_MODE */
+#  define DO_SEMANTIC_CHECKS_BY_DEFAULT true
+#endif /* CVC5_MUZZLED || CVC5_COMPETITION_MODE */
+
+struct Holder${id_cap}$
+{
+// clang-format off
+${holder_spec}$
+// clang-format on
+};
+
+#undef DO_SEMANTIC_CHECKS_BY_DEFAULT
+
+// clang-format off
 ${decls}$
+// clang-format on
 
 }  // namespace options
 
+// clang-format off
 ${specs}$
+// clang-format on
 
 namespace options {
+// clang-format off
 ${inls}$
+// clang-format on
 
 }  // namespace options
 }  // namespace cvc5
 
 #endif /* CVC5__OPTIONS__${id_cap}$_H */
-//clang-format on
diff --git a/src/options/options_handler.cpp b/src/options/options_handler.cpp
index dd555ab56..ee5396dff 100644
--- a/src/options/options_handler.cpp
+++ b/src/options/options_handler.cpp
@@ -33,7 +33,7 @@
 #include "options/didyoumean.h"
 #include "options/language.h"
 #include "options/option_exception.h"
-#include "options/options_holder.h"
+#include "options/resource_manager_options.h"
 #include "options/smt_options.h"
 #include "options/theory_options.h"
 
@@ -83,7 +83,7 @@ unsigned long OptionsHandler::limitHandler(std::string option,
 
 void OptionsHandler::setResourceWeight(std::string option, std::string optarg)
 {
-  d_options->d_holder->resourceWeightHolder.emplace_back(optarg);
+  d_options->resman().resourceWeightHolder.emplace_back(optarg);
 }
 
 // theory/quantifiers/options_handlers.h
@@ -258,24 +258,24 @@ void OptionsHandler::setStats(const std::string& option, bool value)
   {
     if (opt == options::statisticsAll.name)
     {
-      d_options->d_holder->statistics = true;
+      d_options->base().statistics = true;
     }
     else if (opt == options::statisticsEveryQuery.name)
     {
-      d_options->d_holder->statistics = true;
+      d_options->base().statistics = true;
     }
     else if (opt == options::statisticsExpert.name)
     {
-      d_options->d_holder->statistics = true;
+      d_options->base().statistics = true;
     }
   }
   else
   {
     if (opt == options::statistics.name)
     {
-      d_options->d_holder->statisticsAll = false;
-      d_options->d_holder->statisticsEveryQuery = false;
-      d_options->d_holder->statisticsExpert = false;
+      d_options->base().statisticsAll = false;
+      d_options->base().statisticsEveryQuery = false;
+      d_options->base().statisticsExpert = false;
     }
   }
 }
diff --git a/src/options/options_holder_template.h b/src/options/options_holder_template.h
deleted file mode 100644
index 04e5eba53..000000000
--- a/src/options/options_holder_template.h
+++ /dev/null
@@ -1,45 +0,0 @@
-/******************************************************************************
- * Top contributors (to current version):
- *   Mathias Preiner, Aina Niemetz, Morgan Deters
- *
- * This file is part of the cvc5 project.
- *
- * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
- * in the top-level source directory and their institutional affiliations.
- * All rights reserved.  See the file COPYING in the top-level source
- * directory for licensing information.
- * ****************************************************************************
- *
- * Global (command-line, set-option, ...) parameters for SMT.
- */
-
-#include "cvc5_private.h"
-
-#ifndef CVC5__OPTIONS__OPTIONS_HOLDER_H
-#define CVC5__OPTIONS__OPTIONS_HOLDER_H
-
-// clang-format off
-${headers_module}$
-
-namespace cvc5 {
-namespace options {
-
-#if defined(CVC5_MUZZLED) || defined(CVC5_COMPETITION_MODE)
-#  define DO_SEMANTIC_CHECKS_BY_DEFAULT false
-#else /* CVC5_MUZZLED || CVC5_COMPETITION_MODE */
-#  define DO_SEMANTIC_CHECKS_BY_DEFAULT true
-#endif /* CVC5_MUZZLED || CVC5_COMPETITION_MODE */
-
-struct OptionsHolder
-{
-  ${macros_module}$
-
-}; /* struct OptionsHolder */
-
-#undef DO_SEMANTIC_CHECKS_BY_DEFAULT
-
-}  // namespace options
-}  // namespace cvc5
-
-#endif /* CVC5__OPTIONS__OPTIONS_HOLDER_H */
-// clang-format on
diff --git a/src/options/options_public_functions.cpp b/src/options/options_public_functions.cpp
index 8c55a19eb..d1cae6d64 100644
--- a/src/options/options_public_functions.cpp
+++ b/src/options/options_public_functions.cpp
@@ -23,7 +23,7 @@
 
 #include "base/listener.h"
 #include "base/modal_exception.h"
-#include "options.h"
+#include "options/options.h"
 #include "options/base_options.h"
 #include "options/language.h"
 #include "options/main_options.h"
diff --git a/src/options/options_template.cpp b/src/options/options_template.cpp
index 49a35ab38..9419e9914 100644
--- a/src/options/options_template.cpp
+++ b/src/options/options_template.cpp
@@ -57,7 +57,6 @@ extern int optreset;
 // clang-format off
 ${headers_module}$
 
-#include "options/options_holder.h"
 #include "base/cvc5config.h"
 #include "options/base_handlers.h"
 
@@ -223,8 +222,10 @@ void runBoolPredicates(T, std::string option, bool b, options::OptionsHandler* h
 }
 
 Options::Options(OptionsListener* ol)
-    : d_holder(new options::OptionsHolder()),
-      d_handler(new options::OptionsHandler(this)),
+    : d_handler(new options::OptionsHandler(this)),
+// clang-format off
+${holder_mem_inits}$
+// clang-format on
       d_olisten(ol)
 {}
 
@@ -234,10 +235,14 @@ Options::~Options() {
 
 void Options::copyValues(const Options& options){
   if(this != &options) {
-    *d_holder = *options.d_holder;
+// clang-format off
+${holder_mem_copy}$
+// clang-format on
   }
 }
 
+${holder_getter_impl}$
+
 std::string Options::formatThreadOptionException(const std::string& option) {
   std::stringstream ss;
   ss << "can't understand option `" << option
@@ -390,7 +395,7 @@ std::vector<std::string> Options::parseOptions(Options* options,
   if(x != NULL) {
     progName = x + 1;
   }
-  options->d_holder->binary_name = std::string(progName);
+  options->base().binary_name = std::string(progName);
 
   std::vector<std::string> nonoptions;
   options->parseOptionsRecursive(argc, argv, &nonoptions);
diff --git a/src/options/options.h b/src/options/options_template.h
index 324850c43..a25ddc58c 100644
--- a/src/options/options.h
+++ b/src/options/options_template.h
@@ -36,6 +36,9 @@ class Solver;
 namespace options {
   struct OptionsHolder;
   class OptionsHandler;
+// clang-format off
+${holder_fwd_decls}$
+// clang-format on
   }  // namespace options
 
 class OptionsListener;
@@ -43,12 +46,14 @@ class OptionsListener;
 class CVC5_EXPORT Options
 {
   friend api::Solver;
-  /** The struct that holds all option values. */
-  std::unique_ptr<options::OptionsHolder> d_holder;
 
   /** The handler for the options of the theory. */
   options::OptionsHandler* d_handler;
 
+// clang-format off
+${holder_mem_decls}$
+// clang-format on
+
   /** The current Options in effect */
   static thread_local Options* s_current;
 
@@ -104,6 +109,10 @@ public:
   Options(OptionsListener* ol = nullptr);
   ~Options();
 
+// clang-format off
+${holder_getter_decls}$
+// clang-format on
+
   /**
    * Copies the value of the options stored in OptionsHolder into the current
    * Options object.
diff --git a/src/options/resource_manager_options.toml b/src/options/resource_manager_options.toml
index 85cdf1bef..96bc30aaa 100644
--- a/src/options/resource_manager_options.toml
+++ b/src/options/resource_manager_options.toml
@@ -1,4 +1,4 @@
-id     = "resource_manager"
+id     = "RESMAN"
 name   = "Resource Manager options"
 
 [[option]]