Remove void as possible option type (#7731)

This PR removes the possibility to have void options. While there are (very) few options that may legitimately be considered void (they do not actually hold a value, but merely trigger a handler or predicate), the type being void introduces a number of special cases in the options setup. Their only real benefit was to avoid having data members that would never be used.
As it turns out, though, the same can be achieved by not specifying a name, which already supported as well.

9 files changed, 80 insertions, 115 deletions

diff --git a/src/options/README.md b/src/options/README.md
index 54d7d4878..c3e018215 100644
--- a/src/options/README.md
+++ b/src/options/README.md
@@ -64,7 +64,6 @@ Option types
 
 Though not enforced explicitly, option types are commonly expected to come from
 a rather restricted set of C++ types:
-some options are merely used to have a handler function called and use `void`;
 Boolean options should use `bool`;
 numeric options should use one of `int64_t`, `uint64_t` and `double`, possibly
 using `minimum` and `maximum` to further restrict the options domain;
@@ -81,10 +80,9 @@ Handler functions
 Custom handler functions are used to turn the option value from an `std::string`
 into the type specified by `type`. Standard handler functions are provided for
 basic types (`std::string`, `bool`, `int64_t`, `uint64_t`, and `double`) as
-well as enums specified by `mode`. A custom handler function needs to be member
-function of `options::OptionsHandler` with signature
-`{type} {handler}(const std::string& flag, const std::string& optionvalue)`, or
-alternatively `void {handler}(const std::string& flag)` if the `type` is `void`.
+well as enums specified by `mode`. A custom handler function needs to be a 
+member function of `options::OptionsHandler` with signature
+`{type} {handler}(const std::string& flag, const std::string& optionvalue)`.
 The parameter `flag` holds the actually used option name, which may be an alias
 name, and should only be used in user messages.
 
@@ -92,16 +90,14 @@ name, and should only be used in user messages.
 Predicate functions
 -------------------
 
-Predicate functions are used to check whether an option value is valid after it
-has been parsed by a (standard or custom) handler function. Like a handler
-function, a predicate function needs to be a member function of
-`options::OptionsHandler` with signature
+Predicate functions are called after an option value has been parsed by a
+(standard or custom) handler function. They usually either check whether the
+parsed option value is valid, or to trigger some action (e.g. print some
+message or set another option). Like a handler function, a predicate function
+needs to be a member function of `options::OptionsHandler` with signature
 `void {predicate}(const std::string& flag, {type} value)`.
-If the check fails, the predicate should raise an `OptionException`.
-
-Note that a predicate function may not only check the value, but may also
-trigger some other action. Examples include enabling trace tags or enforcing
-dependencies between several options.
+A predicate function is expected to raise an `OptionException` if the option
+value is not valid for some reason.
 
 
 Mode options
@@ -144,15 +140,15 @@ Generated code
 The entire options setup heavily relies on generating a lot of code from the
 information retrieved from the `*_options.toml` files. After code generation,
 files related to options live either in `src/options/` (if not changed) or in
-`build/src/options/` (if automatically generated). After all code has been
-generated, the entire options setup consists of the following components:
+`build/src/options/` (if automatically generated). Additionally, code that is
+only needed when using cvc5 on the command line lives in `src/main/` and
+`build/src/main`. After all code has been generated, the entire options setup
+consists of the following components:
 
-* `options.h`: core `Options` class
-* `options_api.h`: utility methods used by the API (`parse()`, `set()`, `get()`,
-  ...)
-* `options_public.h`: utility methods used to access options from outside of
-  libcvc5
-* `{module}_options.h`: specifics for one single options module
+* `options/options.h`: core `Options` class
+* `options/options_public.h`: utility methods used by the API (`getNames()`, `get()`, `set()` and `getInfo()`)
+* `options/{module}_options.h`: specifics for one single options module
+* `main/options.h`: utility methods used by the CLI (`parse()` and `printUsage()`)
 
 
 `Options` class
@@ -172,20 +168,13 @@ Option modules
 --------------
 
 Every option module declares an "option holder" class, which is a simple struct
-that has two members for every option (that is not declared as `type = void`):
+that has two members for every option (that specifies a `name`):
 the actual option value as `{option.type} {option.name}` and a Boolean flag
-`bool {option.name}__setByUser` that indicates whether the option value was
+`bool {option.name}WasSetByUser` that indicates whether the option value was
 explicitly set by the user. If any of the options of a module is a mode option,
 the option module also defines an enum class that corresponds to the mode,
 including `operator<<()` and `stringTo{mode type}`.
 
-For convenience, the option modules also provide methods `void
-{module.id}::setDefault{option.name}(Options& opts, {option.type} value)`. Each
-such method sets the option value to the given value, if the option was not yet
-set by the user, i.e., the `__setByUser` flag is false. Additionally, every
-option module exports the `long` option name as `static constexpr const char*
-{module.id}::{option.name}__name`.
-
 
 Full Example
 ============
@@ -218,6 +207,5 @@ with `--decision-mode=justification`, and similarly from an SMT-LIB input with
 `(set-option :decision internal)` and `(set-option :decision-mode
 justification)`. The command-line help for this option looks as follows:
 
-    --output-lang=LANG | --output-language=LANG
-                           force output language (default is "auto"; see
-                           --output-lang help)
+    --decision=MODE | --decision-mode=MODE
+                           choose decision mode, see --decision=help
diff --git a/src/options/base_options.toml b/src/options/base_options.toml
index 8255da027..9c40442b7 100644
--- a/src/options/base_options.toml
+++ b/src/options/base_options.toml
@@ -63,16 +63,18 @@ name   = "Base"
   category   = "common"
   short      = "v"
   long       = "verbose"
-  type       = "void"
-  handler    = "increaseVerbosity"
+  type       = "bool"
+  alternate  = false
+  predicates = ["increaseVerbosity"]
   help       = "increase verbosity (may be repeated)"
 
 [[option]]
   category   = "common"
   short      = "q"
   long       = "quiet"
-  type       = "void"
-  handler    = "decreaseVerbosity"
+  type       = "bool"
+  alternate  = false
+  predicates = ["decreaseVerbosity"]
   help       = "decrease verbosity (may be repeated)"
 
 [[option]]
@@ -136,7 +138,7 @@ name   = "Base"
   short      = "t"
   long       = "trace=TAG"
   type       = "std::string"
-  handler    = "enableTraceTag"
+  predicates = ["enableTraceTag"]
   help       = "trace something (e.g. -t pushpop), can repeat"
 
 [[option]]
@@ -144,16 +146,15 @@ name   = "Base"
   short      = "d"
   long       = "debug=TAG"
   type       = "std::string"
-  handler    = "enableDebugTag"
+  predicates = ["enableDebugTag"]
   help       = "debug something (e.g. -d arith), can repeat"
 
 [[option]]
-  name       = "outputTag"
   short      = "o"
   long       = "output=TAG"
   type       = "OutputTag"
   default    = "NONE"
-  handler    = "enableOutputTag"
+  predicates = ["enableOutputTag"]
   category   = "regular"
   help       = "Enable output tag."
   help_mode  = "Output tags."
@@ -241,7 +242,7 @@ name   = "Base"
   category   = "expert"
   long       = "rweight=VAL=N"
   type       = "std::string"
-  handler    = "setResourceWeight"
+  predicates = ["setResourceWeight"]
   help       = "set a single resource weight"
 
 [[option]]
diff --git a/src/options/mkoptions.py b/src/options/mkoptions.py
index 3022c5d4b..8a7dbf605 100644
--- a/src/options/mkoptions.py
+++ b/src/options/mkoptions.py
@@ -287,16 +287,13 @@ def generate_get_impl(modules):
             ret = '{{ std::stringstream s; s << options.{}.{}; return s.str(); }}'.format(
                 module.id, option.name)
         res.append('if ({}) {}'.format(cond, ret))
-    return '\n  '.join(res)
+    return '\n    '.join(res)
 
 
 def _set_handlers(option):
     """Render handler call for options::set()."""
     if option.handler:
-        if option.type == 'void':
-            return 'opts.handler().{}(name)'.format(option.handler)
-        else:
-            return 'opts.handler().{}(name, optionarg)'.format(option.handler)
+        return 'opts.handler().{}(name, optionarg)'.format(option.handler)
     elif option.mode:
         return 'stringTo{}(optionarg)'.format(option.type)
     return 'handlers::handleOption<{}>(name, optionarg)'.format(option.type)
@@ -304,9 +301,6 @@ def _set_handlers(option):
 
 def _set_predicates(option):
     """Render predicate calls for options::set()."""
-    if option.type == 'void':
-        return []
-    assert option.type != 'void'
     res = []
     if option.minimum:
         res.append(
@@ -317,20 +311,11 @@ def _set_predicates(option):
             'opts.handler().checkMaximum(name, value, static_cast<{}>({}));'
             .format(option.type, option.maximum))
     res += [
-        'opts.handler().{}(name, value);'.format(x)
-        for x in option.predicates
+        'opts.handler().{}(name, value);'.format(x) for x in option.predicates
     ]
     return res
 
 
-TPL_SET = '''    opts.{module}.{name} = {handler};
-    opts.{module}.{name}WasSetByUser = true;'''
-TPL_SET_PRED = '''    auto value = {handler};
-    {predicates}
-    opts.{module}.{name} = value;
-    opts.{module}.{name}WasSetByUser = true;'''
-
-
 def generate_set_impl(modules):
     """Generates the implementation for options::set()."""
     res = []
@@ -338,31 +323,19 @@ def generate_set_impl(modules):
         if not option.long:
             continue
         cond = ' || '.join(['name == "{}"'.format(x) for x in option.names])
-        predicates = _set_predicates(option)
         if res:
-            res.append('  }} else if ({}) {{'.format(cond))
+            res.append('}} else if ({}) {{'.format(cond))
         else:
             res.append('if ({}) {{'.format(cond))
-        if option.name and not (option.handler and option.mode):
-            if predicates:
-                res.append(
-                    TPL_SET_PRED.format(module=module.id,
-                                        name=option.name,
-                                        handler=_set_handlers(option),
-                                        predicates='\n    '.join(predicates)))
-            else:
-                res.append(
-                    TPL_SET.format(module=module.id,
-                                   name=option.name,
-                                   handler=_set_handlers(option)))
-        elif option.handler:
-            h = '  opts.handler().{handler}(name'
-            if option.type not in ['bool', 'void']:
-                h += ', optionarg'
-            h += ');'
-            res.append(
-                h.format(handler=option.handler, smtname=option.long_name))
-    return '\n'.join(res)
+        res.append('  auto value = {};'.format(_set_handlers(option)))
+        for pred in _set_predicates(option):
+            res.append('  {}'.format(pred))
+        if option.name:
+            res.append('  opts.{module}.{name} = value;'.format(
+                module=module.id, name=option.name))
+            res.append('  opts.{module}.{name}WasSetByUser = true;'.format(
+                module=module.id, name=option.name))
+    return '\n    '.join(res)
 
 
 def generate_getinfo_impl(modules):
@@ -431,7 +404,7 @@ def generate_module_mode_decl(module):
     """Generates the declarations of mode enums and utility functions."""
     res = []
     for option in module.options:
-        if option.name is None or not option.mode:
+        if not option.mode:
             continue
         values = list(option.mode.keys())
         res.append(
@@ -523,12 +496,12 @@ def generate_module_mode_impl(module):
     """Generates the declarations of mode enums and utility functions."""
     res = []
     for option in module.options:
-        if option.name is None or not option.mode:
+        if not option.mode:
             continue
         cases = [
             'case {type}::{enum}: return os << "{name}";'.format(
                 type=option.type, enum=enum, name=info[0]['name'])
-            for enum,info in option.mode.items()
+            for enum, info in option.mode.items()
         ]
         res.append(
             TPL_MODE_STREAM_OPERATOR.format(type=option.type,
@@ -566,7 +539,7 @@ def generate_module_mode_impl(module):
 def _add_cmdoption(option, name, opts, next_id):
     fmt = {
         'name': name,
-        'arg': 'no' if option.type in ['bool', 'void'] else 'required',
+        'arg': 'no' if option.type == 'bool' else 'required',
         'next_id': next_id
     }
     opts.append(
@@ -590,7 +563,7 @@ def generate_parsing(modules):
             needs_impl = True
             code.append("case '{0}': // -{0}".format(option.short))
             short += option.short
-            if option.type not in ['bool', 'void']:
+            if option.type != 'bool':
                 short += ':'
         if option.long:  # long option
             needs_impl = True
@@ -609,9 +582,6 @@ def generate_parsing(modules):
             if option.type == 'bool':
                 code.append('  solver.setOption("{}", "true"); break;'.format(
                     option.long_name))
-            elif option.type == 'void':
-                code.append('  solver.setOption("{}", ""); break;'.format(
-                    option.long_name))
             else:
                 code.append(
                     '  solver.setOption("{}", optionarg); break;'.format(
@@ -824,14 +794,14 @@ def generate_sphinx_help(modules):
 def generate_sphinx_output_tags(modules, src_dir, build_dir):
     """Render help for the --output option for sphinx."""
     base = next(filter(lambda m: m.id == 'base', modules))
-    opt = next(filter(lambda o: o.name == 'outputTag', base.options))
+    opt = next(filter(lambda o: o.long == 'output=TAG', base.options))
 
     # The programoutput extension has weird semantics about the cwd:
     # https://sphinxcontrib-programoutput.readthedocs.io/en/latest/#usage
     cwd = '/' + os.path.relpath(build_dir, src_dir)
 
     res = []
-    for name,info in opt.mode.items():
+    for name, info in opt.mode.items():
         info = info[0]
         if 'description' not in info:
             continue
@@ -1002,9 +972,9 @@ class Checker:
             self.__check_option_long(o, o.long_name)
             if o.alternate:
                 self.__check_option_long(o, 'no-' + o.long_name)
-            if o.type in ['bool', 'void'] and '=' in o.long:
-                self.perr('must not have an argument description', option=o)
-            if o.type not in ['bool', 'void'] and not '=' in o.long:
+            if o.type == 'bool' and '=' in o.long:
+                self.perr('bool options must not have an argument description', option=o)
+            if o.type != 'bool' and not '=' in o.long:
                 self.perr("needs argument description ('{}=...')",
                           o.long,
                           option=o)
diff --git a/src/options/module_template.h b/src/options/module_template.h
index c613c1cba..00bf7c0ca 100644
--- a/src/options/module_template.h
+++ b/src/options/module_template.h
@@ -42,7 +42,7 @@ ${modes_decl}$
 struct Holder${id_cap}$
 {
 // clang-format off
-${holder_decl}$
+  ${holder_decl}$
 // clang-format on
 };
 
diff --git a/src/options/options_handler.cpp b/src/options/options_handler.cpp
index 7af82df42..50b3ec0a9 100644
--- a/src/options/options_handler.cpp
+++ b/src/options/options_handler.cpp
@@ -142,13 +142,13 @@ void OptionsHandler::setVerbosity(const std::string& flag, int value)
   }
 }
 
-void OptionsHandler::decreaseVerbosity(const std::string& flag)
+void OptionsHandler::decreaseVerbosity(const std::string& flag, bool value)
 {
   d_options->base.verbosity -= 1;
   setVerbosity(flag, d_options->base.verbosity);
 }
 
-void OptionsHandler::increaseVerbosity(const std::string& flag)
+void OptionsHandler::increaseVerbosity(const std::string& flag, bool value)
 {
   d_options->base.verbosity += 1;
   setVerbosity(flag, d_options->base.verbosity);
@@ -247,9 +247,9 @@ void OptionsHandler::enableDebugTag(const std::string& flag,
 }
 
 void OptionsHandler::enableOutputTag(const std::string& flag,
-                                     const std::string& optarg)
+                                     OutputTag optarg)
 {
-  size_t tagid = static_cast<size_t>(stringToOutputTag(optarg));
+  size_t tagid = static_cast<size_t>(optarg);
   Assert(d_options->base.outputTagHolder.size() > tagid)
       << "Output tag is larger than the bitset that holds it.";
   d_options->base.outputTagHolder.set(tagid);
diff --git a/src/options/options_handler.h b/src/options/options_handler.h
index 6f5016c6c..a70a46a4a 100644
--- a/src/options/options_handler.h
+++ b/src/options/options_handler.h
@@ -22,6 +22,7 @@
 #include <sstream>
 #include <string>
 
+#include "options/base_options.h"
 #include "options/bv_options.h"
 #include "options/decision_options.h"
 #include "options/language.h"
@@ -83,9 +84,9 @@ class OptionsHandler
   /** Apply verbosity to the different output channels */
   void setVerbosity(const std::string& flag, int value);
   /** Decrease verbosity and call setVerbosity */
-  void decreaseVerbosity(const std::string& flag);
+  void decreaseVerbosity(const std::string& flag, bool value);
   /** Increase verbosity and call setVerbosity */
-  void increaseVerbosity(const std::string& flag);
+  void increaseVerbosity(const std::string& flag, bool value);
   /** If statistics are disabled, disable statistics sub-options */
   void setStats(const std::string& flag, bool value);
   /** If statistics sub-option is disabled, enable statistics */
@@ -95,7 +96,7 @@ class OptionsHandler
   /** Enable a particular debug tag */
   void enableDebugTag(const std::string& flag, const std::string& optarg);
   /** Enable a particular output tag */
-  void enableOutputTag(const std::string& flag, const std::string& optarg);
+  void enableOutputTag(const std::string& flag, OutputTag optarg);
   /** Apply print success flag to the different output channels */
   void setPrintSuccess(const std::string& flag, bool value);
   /** Pass the resource weight specification to the resource manager */
diff --git a/src/options/options_public_template.cpp b/src/options/options_public_template.cpp
index a6ab6efde..952b4c7f8 100644
--- a/src/options/options_public_template.cpp
+++ b/src/options/options_public_template.cpp
@@ -206,7 +206,7 @@ namespace cvc5::options
     Trace("options") << "set option " << name << " = " << optionarg
                      << std::endl;
     // clang-format off
-  ${set_impl}$
+    ${set_impl}$
     // clang-format on
   }
   else
diff --git a/test/unit/api/cpp/solver_black.cpp b/test/unit/api/cpp/solver_black.cpp
index 36b669bca..6e5c14257 100644
--- a/test/unit/api/cpp/solver_black.cpp
+++ b/test/unit/api/cpp/solver_black.cpp
@@ -1443,13 +1443,16 @@ TEST_F(TestApiBlackSolver, getOptionInfo)
   }
   {
     // mode option
-    api::OptionInfo info = d_solver.getOptionInfo("output");
-    EXPECT_EQ("output", info.name);
-    EXPECT_EQ(std::vector<std::string>{}, info.aliases);
+    api::OptionInfo info = d_solver.getOptionInfo("simplification");
+    EXPECT_EQ("simplification", info.name);
+    EXPECT_EQ(std::vector<std::string>{"simplification-mode"}, info.aliases);
     EXPECT_TRUE(std::holds_alternative<OptionInfo::ModeInfo>(info.valueInfo));
     auto modeInfo = std::get<OptionInfo::ModeInfo>(info.valueInfo);
-    EXPECT_EQ("none", modeInfo.defaultValue);
-    EXPECT_EQ("none", modeInfo.currentValue);
+    EXPECT_EQ("batch", modeInfo.defaultValue);
+    EXPECT_EQ("batch", modeInfo.currentValue);
+    EXPECT_EQ(2, modeInfo.modes.size());
+    EXPECT_TRUE(std::find(modeInfo.modes.begin(), modeInfo.modes.end(), "batch")
+                != modeInfo.modes.end());
     EXPECT_TRUE(std::find(modeInfo.modes.begin(), modeInfo.modes.end(), "none")
                 != modeInfo.modes.end());
   }
diff --git a/test/unit/api/java/SolverTest.java b/test/unit/api/java/SolverTest.java
index ed2f7491d..5d651e82a 100644
--- a/test/unit/api/java/SolverTest.java
+++ b/test/unit/api/java/SolverTest.java
@@ -1428,15 +1428,17 @@ class SolverTest
     }
     {
       // mode option
-      OptionInfo info = d_solver.getOptionInfo("output");
+      OptionInfo info = d_solver.getOptionInfo("simplification");
       assertions.clear();
-      assertions.add(() -> assertEquals("output", info.getName()));
+      assertions.add(() -> assertEquals("simplification", info.getName()));
       assertions.add(
-          () -> assertEquals(Arrays.asList(new String[] {}), Arrays.asList(info.getAliases())));
+          () -> assertEquals(Arrays.asList(new String[] {"simplification-mode"}), Arrays.asList(info.getAliases())));
       assertions.add(() -> assertTrue(info.getBaseInfo().getClass() == OptionInfo.ModeInfo.class));
       OptionInfo.ModeInfo modeInfo = (OptionInfo.ModeInfo) info.getBaseInfo();
-      assertions.add(() -> assertEquals("none", modeInfo.getDefaultValue()));
-      assertions.add(() -> assertEquals("none", modeInfo.getCurrentValue()));
+      assertions.add(() -> assertEquals("batch", modeInfo.getDefaultValue()));
+      assertions.add(() -> assertEquals("batch", modeInfo.getCurrentValue()));
+      assertions.add(() -> assertEquals(2, modeInfo.getModes().length));
+      assertions.add(() -> assertTrue(Arrays.asList(modeInfo.getModes()).contains("batch")));
       assertions.add(() -> assertTrue(Arrays.asList(modeInfo.getModes()).contains("none")));
     }
     assertAll(assertions);