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.
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;
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.
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
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
--------------
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
============
`(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
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]]
short = "t"
long = "trace=TAG"
type = "std::string"
- handler = "enableTraceTag"
+ predicates = ["enableTraceTag"]
help = "trace something (e.g. -t pushpop), can repeat"
[[option]]
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."
category = "expert"
long = "rweight=VAL=N"
type = "std::string"
- handler = "setResourceWeight"
+ predicates = ["setResourceWeight"]
help = "set a single resource weight"
[[option]]
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)
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(
'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 = []
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):
"""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(
"""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,
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(
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
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(
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
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)
struct Holder${id_cap}$
{
// clang-format off
-${holder_decl}$
+ ${holder_decl}$
// clang-format on
};
}
}
-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);
}
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);
#include <sstream>
#include <string>
+#include "options/base_options.h"
#include "options/bv_options.h"
#include "options/decision_options.h"
#include "options/language.h"
/** 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 */
/** 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 */
Trace("options") << "set option " << name << " = " << optionarg
<< std::endl;
// clang-format off
- ${set_impl}$
+ ${set_impl}$
// clang-format on
}
else
}
{
// 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());
}
}
{
// 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);
projects / cvc5.git / commitdiff