diff options
| -rw-r--r-- | src/options/README.md | 56 | ||||
| -rw-r--r-- | src/options/base_options.toml | 19 | ||||
| -rw-r--r-- | src/options/mkoptions.py | 76 | ||||
| -rw-r--r-- | src/options/module_template.h | 2 | ||||
| -rw-r--r-- | src/options/options_handler.cpp | 8 | ||||
| -rw-r--r-- | src/options/options_handler.h | 7 | ||||
| -rw-r--r-- | src/options/options_public_template.cpp | 2 | ||||
| -rw-r--r-- | test/unit/api/cpp/solver_black.cpp | 13 | ||||
| -rw-r--r-- | test/unit/api/java/SolverTest.java | 12 |
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); |