First part of options refactoring (#6428)

This PR does a first round of refactoring and gets rid of a significant portion of generated code. In particular

- it removes options::optionName.wasSetByUser() (we still have Options::wasSetByUser())
- it removes options::optionName.set() (we still have Options::set())
- it removes options::optionName.getName() in favor of options::optionName.name
- it removes the specializations of Options::assign() and Options::assignBool() from the headers
- it eliminates runHandlerAndPredicates() and runBoolPredicates()

The removed methods are only used in few places with are changed to using Options::current().X() instead.

In the future, we also want to get rid of options::optionName() and use Options::operator[]() instead, and furthermore not use Options::current() but use the options from the Env object. This PR already adds Env::getOption() as a shorthand for Env::getOptions()[...] and uses it as a proof of concept within SmtEngine.

8 files changed, 100 insertions, 189 deletions

diff --git a/src/options/bv_options.toml b/src/options/bv_options.toml
index acb010a2e..18f190ff1 100644
--- a/src/options/bv_options.toml
+++ b/src/options/bv_options.toml
@@ -51,6 +51,7 @@ header = "options/bv_options.h"
   category   = "expert"
   long       = "bv-aig-simp=COMMAND"
   type       = "std::string"
+  default    = "\"balance;drw\""
   predicates = ["abcEnabledBuild"]
   help       = "abc command to run AIG simplifications (implies --bitblast-aig, default is \"balance;drw\")"
 
diff --git a/src/options/mkoptions.py b/src/options/mkoptions.py
index 9c66c6b61..fa2a39b04 100644
--- a/src/options/mkoptions.py
+++ b/src/options/mkoptions.py
@@ -81,63 +81,35 @@ g_getopt_long_start = 256
 
 TPL_HOLDER_MACRO_NAME = 'CVC5_OPTIONS__{id}__FOR_OPTION_HOLDER'
 
-TPL_RUN_HANDLER = \
-"""template <> options::{name}__option_t::type runHandlerAndPredicates(
-    options::{name}__option_t,
-    std::string option,
-    std::string optionarg,
-    options::OptionsHandler* handler)
-{{
-  options::{name}__option_t::type retval = {handler};
-  {predicates}
-  return retval;
-}}"""
-
-TPL_DECL_ASSIGN = \
+TPL_IMPL_ASSIGN = \
 """template <> void Options::assign(
     options::{name}__option_t,
     std::string option,
-    std::string value);"""
-
-TPL_IMPL_ASSIGN = TPL_DECL_ASSIGN[:-1] + \
-"""
+    std::string optionarg)
 {{
-  d_holder->{name} =
-    runHandlerAndPredicates(options::{name}, option, value, d_handler);
+  auto parsedval = {handler};
+  {predicates}
+  d_holder->{name} = parsedval;
   d_holder->{name}__setByUser__ = true;
   Trace("options") << "user assigned option {name}" << std::endl;
 }}"""
 
-
-TPL_RUN_HANDLER_BOOL = \
-"""template <> void runBoolPredicates(
-    options::{name}__option_t,
-    std::string option,
-    bool b,
-    options::OptionsHandler* handler)
-{{
-  {predicates}
-}}"""
-
-TPL_DECL_ASSIGN_BOOL = \
+TPL_IMPL_ASSIGN_BOOL = \
 """template <> void Options::assignBool(
     options::{name}__option_t,
     std::string option,
-    bool value);"""
-
-TPL_IMPL_ASSIGN_BOOL = TPL_DECL_ASSIGN_BOOL[:-1] + \
-"""
+    bool value)
 {{
-  runBoolPredicates(options::{name}, option, value, d_handler);
+  {predicates}
   d_holder->{name} = value;
   d_holder->{name}__setByUser__ = true;
   Trace("options") << "user assigned option {name}" << std::endl;
 }}"""
 
 TPL_CALL_ASSIGN_BOOL = \
-    '  options->assignBool(options::{name}, {option}, {value});'
+    '  assignBool(options::{name}, {option}, {value});'
 
-TPL_CALL_ASSIGN = '  options->assign(options::{name}, {option}, optionarg);'
+TPL_CALL_ASSIGN = '  assign(options::{name}, {option}, optionarg);'
 
 TPL_CALL_SET_OPTION = 'setOption(std::string("{smtname}"), ("{value}"));'
 
@@ -157,9 +129,7 @@ TPL_OPTION_STRUCT_RW = \
 {{
   typedef {type} type;
   type operator()() const;
-  bool wasSetByUser() const;
-  void set(const type& v);
-  const char* getName() const;
+  static constexpr const char* name = "{long_name}";
 }} thread_local {name};"""
 
 TPL_OPTION_STRUCT_RO = \
@@ -167,20 +137,18 @@ TPL_OPTION_STRUCT_RO = \
 {{
   typedef {type} type;
   type operator()() const;
-  bool wasSetByUser() const;
-  const char* getName() const;
+  static constexpr const char* name = "{long_name}";
 }} thread_local {name};"""
 
 
 TPL_DECL_SET = \
-"""template <> void Options::set(
-    options::{name}__option_t,
-    const options::{name}__option_t::type& x);"""
+"""template <> options::{name}__option_t::type& Options::ref(
+    options::{name}__option_t);"""
 
 TPL_IMPL_SET = TPL_DECL_SET[:-1] + \
 """
 {{
-  d_holder->{name} = x;
+    return d_holder->{name};
 }}"""
 
 
@@ -206,32 +174,12 @@ TPL_IMPL_WAS_SET_BY_USER = TPL_DECL_WAS_SET_BY_USER[:-1] + \
 
 # Option specific methods
 
-TPL_IMPL_OPTION_SET = \
-"""inline void {name}__option_t::set(const {name}__option_t::type& v)
-{{
-  Options::current()->set(*this, v);
-}}"""
-
 TPL_IMPL_OP_PAR = \
 """inline {name}__option_t::type {name}__option_t::operator()() const
 {{
-  return (*Options::current())[*this];
-}}"""
-
-TPL_IMPL_OPTION_WAS_SET_BY_USER = \
-"""inline bool {name}__option_t::wasSetByUser() const
-{{
-  return Options::current()->wasSetByUser(*this);
-}}"""
-
-TPL_IMPL_GET_NAME = \
-"""inline const char* {name}__option_t::getName() const
-{{
-  return "{long_name}";
+  return Options::current()[*this];
 }}"""
 
-
-
 # Mode templates
 TPL_DECL_MODE_ENUM = \
 """
@@ -242,16 +190,14 @@ enum class {type}
 
 TPL_DECL_MODE_FUNC = \
 """
-std::ostream&
-operator<<(std::ostream& os, {type} mode);"""
+std::ostream& operator<<(std::ostream& os, {type} mode);"""
 
 TPL_IMPL_MODE_FUNC = TPL_DECL_MODE_FUNC[:-len(";")] + \
 """
 {{
-  os << "{type}::";
   switch(mode) {{{cases}
     default:
-        Unreachable();
+      Unreachable();
   }}
   return os;
 }}
@@ -260,13 +206,11 @@ TPL_IMPL_MODE_FUNC = TPL_DECL_MODE_FUNC[:-len(";")] + \
 TPL_IMPL_MODE_CASE = \
 """
     case {type}::{enum}:
-      os << "{enum}";
-      break;"""
+      return os << "{type}::{enum}";"""
 
 TPL_DECL_MODE_HANDLER = \
 """
-{type}
-stringTo{type}(const std::string& option, const std::string& optarg);"""
+{type} stringTo{type}(const std::string& optarg);"""
 
 TPL_IMPL_MODE_HANDLER = TPL_DECL_MODE_HANDLER[:-1] + \
 """
@@ -274,14 +218,11 @@ TPL_IMPL_MODE_HANDLER = TPL_DECL_MODE_HANDLER[:-1] + \
   {cases}
   else if (optarg == "help")
   {{
-    puts({help});
-    exit(1);
-  }}
-  else
-  {{
-    throw OptionException(std::string("unknown option for --{long}: `") +
-                          optarg + "'.  Try --{long}=help.");
+    std::cerr << {help};
+    std::exit(1);
   }}
+  throw OptionException(std::string("unknown option for --{long}: `") +
+                        optarg + "'.  Try --{long}=help.");
 }}
 """
 
@@ -513,7 +454,11 @@ def codegen_module(module, dst_dir, tpl_module_h, tpl_module_cpp):
 
         # Generate module declaration
         tpl_decl = TPL_OPTION_STRUCT_RO if option.read_only else TPL_OPTION_STRUCT_RW
-        decls.append(tpl_decl.format(name=option.name, type=option.type))
+        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))
 
         # Generate module specialization
         if not option.read_only:
@@ -521,11 +466,6 @@ def codegen_module(module, dst_dir, tpl_module_h, tpl_module_cpp):
         specs.append(TPL_DECL_OP_BRACKET.format(name=option.name))
         specs.append(TPL_DECL_WAS_SET_BY_USER.format(name=option.name))
 
-        if option.type == 'bool':
-            specs.append(TPL_DECL_ASSIGN_BOOL.format(name=option.name))
-        else:
-            specs.append(TPL_DECL_ASSIGN.format(name=option.name))
-
         if option.long and option.type not in ['bool', 'void'] and \
            '=' not in option.long:
             die("module '{}': option '{}' with type '{}' needs an argument " \
@@ -539,15 +479,6 @@ def codegen_module(module, dst_dir, tpl_module_h, tpl_module_cpp):
 
         # Generate module inlines
         inls.append(TPL_IMPL_OP_PAR.format(name=option.name))
-        inls.append(TPL_IMPL_OPTION_WAS_SET_BY_USER.format(name=option.name))
-        if not option.read_only:
-            inls.append(TPL_IMPL_OPTION_SET.format(name=option.name))
-        if option.long:
-            long_name = option.long.split('=')[0]
-        else:
-            long_name = ""
-        inls.append(TPL_IMPL_GET_NAME.format(
-                        name=option.name, long_name=long_name))
 
 
         ### Generate code for {module.name}_options.cpp
@@ -704,12 +635,12 @@ def codegen_all_modules(modules, dst_dir, tpl_options, tpl_options_holder):
             handler = None
             if option.handler:
                 if option.type == 'void':
-                    handler = 'handler->{}(option)'.format(option.handler)
+                    handler = 'd_handler->{}(option)'.format(option.handler)
                 else:
                     handler = \
-                        'handler->{}(option, optionarg)'.format(option.handler)
+                        'd_handler->{}(option, optionarg)'.format(option.handler)
             elif option.mode:
-                handler = 'stringTo{}(option, optionarg)'.format(option.type)
+                handler = 'stringTo{}(optionarg)'.format(option.type)
             elif option.type != 'bool':
                 handler = \
                     'handleOption<{}>(option, optionarg)'.format(option.type)
@@ -719,12 +650,12 @@ def codegen_all_modules(modules, dst_dir, tpl_options, tpl_options_holder):
             if option.predicates:
                 if option.type == 'bool':
                     predicates = \
-                        ['handler->{}(option, b);'.format(x) \
+                        ['d_handler->{}(option, value);'.format(x) \
                             for x in option.predicates]
                 else:
                     assert option.type != 'void'
                     predicates = \
-                        ['handler->{}(option, retval);'.format(x) \
+                        ['d_handler->{}(option, parsedval);'.format(x) \
                             for x in option.predicates]
 
             # Generate options_handler and getopt_long
@@ -867,24 +798,6 @@ def codegen_all_modules(modules, dst_dir, tpl_options, tpl_options_holder):
                     options_getoptions.append(s)
 
 
-                # Define runBoolPredicates/runHandlerAndPredicates
-                tpl = None
-                if option.type == 'bool':
-                    if predicates:
-                        assert handler is None
-                        tpl = TPL_RUN_HANDLER_BOOL
-                elif option.short or option.long:
-                    assert option.type != 'void'
-                    assert handler
-                    tpl = TPL_RUN_HANDLER
-                if tpl:
-                    custom_handlers.append(
-                        tpl.format(
-                            name=option.name,
-                            handler=handler,
-                            predicates='\n'.join(predicates)
-                        ))
-
                 # Define handler assign/assignBool
                 tpl = None
                 if option.type == 'bool':
@@ -893,7 +806,9 @@ def codegen_all_modules(modules, dst_dir, tpl_options, tpl_options_holder):
                     tpl = TPL_IMPL_ASSIGN
                 if tpl:
                     custom_handlers.append(tpl.format(
-                        name=option.name
+                        name=option.name,
+                        handler=handler,
+                        predicates='\n'.join(predicates)
                     ))
 
                 # Default option values
diff --git a/src/options/module_template.cpp b/src/options/module_template.cpp
index 3b928dba0..0de77e8a6 100644
--- a/src/options/module_template.cpp
+++ b/src/options/module_template.cpp
@@ -19,6 +19,8 @@
 #include "options/options_holder.h"
 #include "base/check.h"
 
+#include <iostream>
+
 // clang-format off
 namespace cvc5 {
 
diff --git a/src/options/open_ostream.cpp b/src/options/open_ostream.cpp
index 3b13c42e2..9ebea6da0 100644
--- a/src/options/open_ostream.cpp
+++ b/src/options/open_ostream.cpp
@@ -20,6 +20,7 @@
 
 
 #include <cerrno>
+#include <fstream>
 #include <iostream>
 #include <ostream>
 #include <sstream>
diff --git a/src/options/options.h b/src/options/options.h
index 67707c990..b249c90ed 100644
--- a/src/options/options.h
+++ b/src/options/options.h
@@ -18,8 +18,7 @@
 #ifndef CVC5__OPTIONS__OPTIONS_H
 #define CVC5__OPTIONS__OPTIONS_H
 
-#include <fstream>
-#include <ostream>
+#include <iosfwd>
 #include <string>
 #include <vector>
 
@@ -77,9 +76,6 @@ class CVC5_EXPORT Options
 
   static std::string formatThreadOptionException(const std::string& option);
 
-  static const size_t s_maxoptlen = 128;
-  static const unsigned s_preemptAdditional = 6;
-
 public:
  class OptionsScope
  {
@@ -102,8 +98,8 @@ public:
   }
 
   /** Get the current Options in effect */
-  static inline Options* current() {
-    return s_current;
+  static inline Options& current() {
+    return *s_current;
   }
 
   Options(OptionsListener* ol = nullptr);
@@ -117,15 +113,39 @@ public:
   void copyValues(const Options& options);
 
   /**
-   * Set the value of the given option.  Use of this default
-   * implementation causes a compile-time error; write-able
-   * options specialize this template with a real implementation.
+   * Set the value of the given option.  Uses `ref()`, which causes a
+   * compile-time error if the given option is read-only.
+   */
+  template <class T>
+  void set(T t, const typename T::type& val) {
+    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 <class T>
+  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
+   * specialize this template with a real implementation.
    */
   template <class T>
-  void set(T, const typename T::type&) {
-    // Flag a compile-time error.  Write-able options specialize
-    // this template to provide an implementation.
-    T::you_are_trying_to_assign_to_a_read_only_option;
+  typename T::type& ref(T) {
+    // Flag a compile-time error.
+    T::you_are_trying_to_get_nonconst_access_to_a_read_only_option;
+    // Ensure the compiler does not complain about the return value.
+    return *static_cast<typename T::type*>(nullptr);
   }
 
   /**
@@ -297,8 +317,7 @@ public:
    *
    * Preconditions: options, extender and nonoptions are non-null.
    */
-  static void parseOptionsRecursive(Options* options,
-                                    int argc,
+  void parseOptionsRecursive(int argc,
                                     char* argv[],
                                     std::vector<std::string>* nonoptions);
 }; /* class Options */
diff --git a/src/options/options_handler.cpp b/src/options/options_handler.cpp
index 0e2315aa0..dd555ab56 100644
--- a/src/options/options_handler.cpp
+++ b/src/options/options_handler.cpp
@@ -159,14 +159,11 @@ void OptionsHandler::checkBvSatSolver(std::string option, SatSolverMode m)
           || m == SatSolverMode::KISSAT))
   {
     if (options::bitblastMode() == options::BitblastMode::LAZY
-        && options::bitblastMode.wasSetByUser())
+        && Options::current().wasSetByUser(options::bitblastMode))
     {
       throwLazyBBUnsupported(m);
     }
-    if (!options::bitvectorToBool.wasSetByUser())
-    {
-      options::bitvectorToBool.set(true);
-    }
+    Options::current().setDefault(options::bitvectorToBool, true);
   }
 }
 
@@ -174,23 +171,10 @@ void OptionsHandler::checkBitblastMode(std::string option, BitblastMode m)
 {
   if (m == options::BitblastMode::LAZY)
   {
-    if (!options::bitvectorPropagate.wasSetByUser())
-    {
-      options::bitvectorPropagate.set(true);
-    }
-    if (!options::bitvectorEqualitySolver.wasSetByUser())
-    {
-      options::bitvectorEqualitySolver.set(true);
-    }
-
-    if (!options::bitvectorInequalitySolver.wasSetByUser())
-    {
-      options::bitvectorInequalitySolver.set(true);
-    }
-    if (!options::bitvectorAlgebraicSolver.wasSetByUser())
-    {
-      options::bitvectorAlgebraicSolver.set(true);
-    }
+    Options::current().setDefault(options::bitvectorPropagate, true);
+    Options::current().setDefault(options::bitvectorEqualitySolver, true);
+    Options::current().setDefault(options::bitvectorInequalitySolver, true);
+    Options::current().setDefault(options::bitvectorAlgebraicSolver, true);
     if (options::bvSatSolver() != options::SatSolverMode::MINISAT)
     {
       throwLazyBBUnsupported(options::bvSatSolver());
@@ -198,27 +182,21 @@ void OptionsHandler::checkBitblastMode(std::string option, BitblastMode m)
   }
   else if (m == BitblastMode::EAGER)
   {
-    if (!options::bitvectorToBool.wasSetByUser())
-    {
-      options::bitvectorToBool.set(true);
-    }
+    Options::current().setDefault(options::bitvectorToBool, true);
   }
 }
 
 void OptionsHandler::setBitblastAig(std::string option, bool arg)
 {
   if(arg) {
-    if(options::bitblastMode.wasSetByUser()) {
+    if(Options::current().wasSetByUser(options::bitblastMode)) {
       if (options::bitblastMode() != options::BitblastMode::EAGER)
       {
         throw OptionException("bitblast-aig must be used with eager bitblaster");
       }
     } else {
-      options::BitblastMode mode = stringToBitblastMode("", "eager");
-      options::bitblastMode.set(mode);
-    }
-    if(!options::bitvectorAigSimplifications.wasSetByUser()) {
-      options::bitvectorAigSimplifications.set("balance;drw");
+      options::BitblastMode mode = stringToBitblastMode("eager");
+      Options::current().set(options::bitblastMode, mode);
     }
   }
 }
@@ -253,13 +231,13 @@ InstFormatMode OptionsHandler::stringToInstFormatMode(std::string option,
 // decision/options_handlers.h
 void OptionsHandler::setDecisionModeStopOnly(std::string option, DecisionMode m)
 {
-  options::decisionStopOnly.set(m == DecisionMode::RELEVANCY);
+  Options::current().set(options::decisionStopOnly, m == DecisionMode::RELEVANCY);
 }
 
 void OptionsHandler::setProduceAssertions(std::string option, bool value)
 {
-  options::produceAssertions.set(value);
-  options::interactiveMode.set(value);
+  Options::current().set(options::produceAssertions, value);
+  Options::current().set(options::interactiveMode, value);
 }
 
 void OptionsHandler::setStats(const std::string& option, bool value)
@@ -278,22 +256,22 @@ void OptionsHandler::setStats(const std::string& option, bool value)
   std::string opt = option.substr(2);
   if (value)
   {
-    if (opt == options::statisticsAll.getName())
+    if (opt == options::statisticsAll.name)
     {
       d_options->d_holder->statistics = true;
     }
-    else if (opt == options::statisticsEveryQuery.getName())
+    else if (opt == options::statisticsEveryQuery.name)
     {
       d_options->d_holder->statistics = true;
     }
-    else if (opt == options::statisticsExpert.getName())
+    else if (opt == options::statisticsExpert.name)
     {
       d_options->d_holder->statistics = true;
     }
   }
   else
   {
-    if (opt == options::statistics.getName())
+    if (opt == options::statistics.name)
     {
       d_options->d_holder->statisticsAll = false;
       d_options->d_holder->statisticsEveryQuery = false;
@@ -508,7 +486,7 @@ OutputLanguage OptionsHandler::stringToOutputLanguage(std::string option,
                                                       std::string optarg)
 {
   if(optarg == "help") {
-    options::languageHelp.set(true);
+    Options::current().set(options::languageHelp, true);
     return language::output::LANG_AUTO;
   }
 
@@ -526,7 +504,7 @@ InputLanguage OptionsHandler::stringToInputLanguage(std::string option,
                                                     std::string optarg)
 {
   if(optarg == "help") {
-    options::languageHelp.set(true);
+    Options::current().set(options::languageHelp, true);
     return language::input::LANG_AUTO;
   }
 
@@ -571,12 +549,12 @@ void OptionsHandler::setVerbosity(std::string option, int value)
 }
 
 void OptionsHandler::increaseVerbosity(std::string option) {
-  options::verbosity.set(options::verbosity() + 1);
+  Options::current().set(options::verbosity, options::verbosity() + 1);
   setVerbosity(option, options::verbosity());
 }
 
 void OptionsHandler::decreaseVerbosity(std::string option) {
-  options::verbosity.set(options::verbosity() - 1);
+  Options::current().set(options::verbosity, options::verbosity() - 1);
   setVerbosity(option, options::verbosity());
 }
 
diff --git a/src/options/options_public_functions.cpp b/src/options/options_public_functions.cpp
index f70c1ce3b..6ad537240 100644
--- a/src/options/options_public_functions.cpp
+++ b/src/options/options_public_functions.cpp
@@ -179,7 +179,7 @@ std::string Options::getBinaryName() const{
 }
 
 std::ostream* Options::currentGetOut() {
-  return current()->getOut();
+  return current().getOut();
 }
 
 
diff --git a/src/options/options_template.cpp b/src/options/options_template.cpp
index f24f83b2b..4493f6094 100644
--- a/src/options/options_template.cpp
+++ b/src/options/options_template.cpp
@@ -408,7 +408,7 @@ std::vector<std::string> Options::parseOptions(Options* options,
   options->d_holder->binary_name = std::string(progName);
 
   std::vector<std::string> nonoptions;
-  parseOptionsRecursive(options, argc, argv, &nonoptions);
+  options->parseOptionsRecursive(argc, argv, &nonoptions);
   if(Debug.isOn("options")){
     for(std::vector<std::string>::const_iterator i = nonoptions.begin(),
           iend = nonoptions.end(); i != iend; ++i){
@@ -419,8 +419,7 @@ std::vector<std::string> Options::parseOptions(Options* options,
   return nonoptions;
 }
 
-void Options::parseOptionsRecursive(Options* options,
-                                    int argc,
+void Options::parseOptionsRecursive(int argc,
                                     char* argv[],
                                     std::vector<std::string>* nonoptions)
 {
@@ -434,9 +433,6 @@ void Options::parseOptionsRecursive(Options* options,
     }
   }
 
-  // Having this synonym simplifies the generation code in mkoptions.
-  options::OptionsHandler* handler = options->d_handler;
-
   // Reset getopt(), in the case of multiple calls to parseOptions().
   // This can be = 1 in newer GNU getopt, but older (< 2007) require = 0.
   optind = 0;
@@ -597,7 +593,6 @@ void Options::setOptionInternal(const std::string& key,
                                 const std::string& optionarg)
 {
   options::OptionsHandler* handler = d_handler;
-  Options* options = this;
   ${setoption_handlers}$
   throw UnrecognizedOptionException(key);
 }