Remove options::X__numValues (#7419)

This PR removes yet another special purpose options detail that is only used in a single place: X__numValues currently holds the number of modes for an option, that is the number of elements of the respective enums. It is solely used to obtain the size of the std::bitset used to store the flags passed to the -o option. However, it can easily be replaced using the last mode.

This PR also improves a bit on options-related documentation.

diff --git a/src/options/README.md b/src/options/README.md
index b0b0261660e9a2ddaaef458a011a000637a504ec..54d7d48788cf5525a57ad06e02c860e5d288e4a0 100644 (file)
--- a/src/options/README.md
+++ b/src/options/README.md
@@ -5,17 +5,10 @@ Every options module, that is a group of options that belong together in some
 way, is declared in its own file in `options/{module name}_options.toml`. Each
 options module starts with the following required attributes:
 
-* `id` (string): ID of the module (e.g., `"arith"`)
+* `id` (string): ID of the module (e.g., `"ARITH"`)
 * `name` (string): name of the module (e.g., `"Arithmetic Theory"`)
 
-Additional, a module can optionally be defined to be public. A public module
-includes `cvc5_public.h` instead of `cvc5_private.h` can thus be included from
-"external" code like the parser or the main driver.
-
-* `public` (bool): make option module public
-
-A module defines 0 or more options.
-
+A module defines zero or more options.
 In general, each attribute/value pair is required to be in one line. Comments
 start with # and are not allowed in attribute/value lines.
 
@@ -34,7 +27,7 @@ Options can be defined within a module file with the `[[option]]` tag, the
 required attributes for an option are:
 
 * `category` (string): one of `common`, `expert`, `regular`, or `undocumented`
-* `type` (string): the C++ type of the option value
+* `type` (string): the C++ type of the option value, see below for more details.
 
 Optional attributes are:
 
@@ -58,27 +51,42 @@ Optional attributes are:
   value is valid, more details below
 * `includes` (list): additional header files required by handler or predicate
   functions
+* `minimum` (numeric): impose a minimum value on this option.
+* `maximum` (numeric): impose a maximum value on this option.
 * `help` (string): documentation string (required, unless the `category` is
   `undocumented`)
 * `help_mode` (string): documentation for the mode enum (required if `mode` is
   given)
 
 
+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;
+mode options should use a fresh type name for the auto-generated enum as
+detailed below.
+
+While other C++ types are allowed, they should only be used in special cases
+when the above types are not sufficient.
+
+
 Handler functions
 -----------------
 
-Custom handler functions are used to turn the option value from a `std::string`
+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`, integer types and floating point types) as
+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& option, const std::string& flag, const std::string& optionvalue)`,
-or alternatively `void {handler}(const std::string& option, const std::string&
-flag)` if the `type` is `void`. The two parameters `option` and `flag` hold the
-canonical and the actually used option names, respectively, and they may differ
-if an alternative name (from `alias`) was used. While `option` should be used to
-identify an option (e.g. by comparing against `*__name`), `flag` should be
-usually used in user messages.
+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`.
+The parameter `flag` holds the actually used option name, which may be an alias
+name, and should only be used in user messages.
 
 
 Predicate functions
@@ -87,9 +95,13 @@ 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 `void {predicate}(const std::string&
-option, const std::string& flag, {type} value)`. If the check fails, the
-predicate should raise an `OptionException`.
+`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.
 
 
 Mode options

diff --git a/src/options/base_options.toml b/src/options/base_options.toml
index 69e0a853be0598fde7bf3147438d67b538e027c4..d59d9cdea2f5cf244cedc9dec9458c560d1d8299 100644 (file)
--- a/src/options/base_options.toml
+++ b/src/options/base_options.toml
@@ -185,7 +185,7 @@ name   = "Base"
   name       = "outputTagHolder"
   category   = "undocumented"
   includes   = ["<bitset>"]
-  type       = "std::bitset<OutputTag__numValues>"
+  type       = "std::bitset<static_cast<size_t>(OutputTag::RAW_BENCHMARK)+1>"
 
 [[option]]
   name       = "printSuccess"

diff --git a/src/options/mkoptions.py b/src/options/mkoptions.py
index 70eb138cc7cb5ba0d5c7d51a78294031623fed0d..dfd48d7f42a54f69da84f25fc2b128515b2215ae 100644 (file)
--- a/src/options/mkoptions.py
+++ b/src/options/mkoptions.py
@@ -421,7 +421,6 @@ TPL_MODE_DECL = '''enum class {type}
 {{
   {values}
 }};
-static constexpr size_t {type}__numValues = {nvalues};
 std::ostream& operator<<(std::ostream& os, {type} mode);
 {type} stringTo{type}(const std::string& optarg);
 '''
@@ -436,8 +435,7 @@ def generate_module_mode_decl(module):
         res.append(
             TPL_MODE_DECL.format(type=option.type,
                                  values=wrap_line(
-                                     ', '.join(option.mode.keys()), 2),
-                                 nvalues=len(option.mode)))
+                                     ', '.join(option.mode.keys()), 2)))
     return '\n'.join(res)
 
 
@@ -791,7 +789,7 @@ def generate_sphinx_help(modules):
     common = []
     others = {}
     for module, option in all_options(modules, False):
-        if option.type == 'undocumented':
+        if option.category == 'undocumented':
             continue
         if not option.long and not option.short:
             continue

diff --git a/src/options/options_handler.cpp b/src/options/options_handler.cpp
index fe0e1d96194955f1990eabe8e5228420f08b15be..063145ea8ee0c4ee7338f64609a5a45511252244 100644 (file)
--- a/src/options/options_handler.cpp
+++ b/src/options/options_handler.cpp
@@ -267,8 +267,11 @@ void OptionsHandler::enableDebugTag(const std::string& flag,
 void OptionsHandler::enableOutputTag(const std::string& flag,
                                      const std::string& optarg)
 {
-  d_options->base.outputTagHolder.set(
-      static_cast<size_t>(stringToOutputTag(optarg)));
+  size_t tagid = static_cast<size_t>(stringToOutputTag(optarg));
+  Assert(d_options->base.outputTagHolder.size() > tagid)
+      << "Trying to enable an output tag whose value is larger than the bitset "
+         "that holds it. Maybe someone forgot to update the bitset size?";
+  d_options->base.outputTagHolder.set(tagid);
 }
 
 void OptionsHandler::setPrintSuccess(const std::string& flag, bool value)