diff options
| -rw-r--r-- | src/options/CMakeLists.txt | 1 | ||||
| -rw-r--r-- | src/options/README | 127 | ||||
| -rw-r--r-- | src/options/README.md | 211 | ||||
| -rw-r--r-- | src/options/base_handlers.h | 87 | ||||
| -rw-r--r-- | src/options/mkoptions.py | 51 | ||||
| -rw-r--r-- | src/options/options_handler.cpp | 117 | ||||
| -rw-r--r-- | src/options/options_handler.h | 144 | ||||
| -rw-r--r-- | src/options/options_template.cpp | 91 | ||||
| -rw-r--r-- | src/options/prop_options.toml | 8 |
9 files changed, 468 insertions, 369 deletions
diff --git a/src/options/CMakeLists.txt b/src/options/CMakeLists.txt index 26ced1a24..cc7b621a8 100644 --- a/src/options/CMakeLists.txt +++ b/src/options/CMakeLists.txt @@ -17,7 +17,6 @@ check_python_module("toml") libcvc5_add_sources( - base_handlers.h decision_weight.h didyoumean.cpp didyoumean.h diff --git a/src/options/README b/src/options/README deleted file mode 100644 index 868690b85..000000000 --- a/src/options/README +++ /dev/null @@ -1,127 +0,0 @@ -Modules -======= - - Each options module starts with the following required attributes: - - id ... (string) ID of the module (e.g., "ARITH") - name ... (string) name of the module (e.g., "Arithmetic Theory") - header ... (string) name of the options header to generated (e.g., "options/arith_options.h") - - A module defines 0 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. - - -Options -======= - - Options can be defined with the [[option]] tag, the required attributes for - an option are: - - category ... (string) common | expert | regular | undocumented - type ... (string) C++ type of the option value - - Optional attributes are: - - name ... (string) option name that is used to access via - options::<name>() - smt_name ... (string) alternative name to access option via - set-option/get-option commands - short ... (string) short option name consisting of one character - (no '-' prefix required) - long ... (string) long option name (required if short is specified, - no '--' prefix required). - long option names may have a suffix '=XXX' where - 'XXX' can be used to indicate the type of the - option value, e.g., '=MODE', '=LANG', '=N', ... - default ... (string) default value of type 'type' - handler ... (string) handler for parsing option values before setting - option - predicates ... (list) functions that check whether given option value is - valid - includes ... (list) header files required by handler/predicates - alternate ... (bool) true (default): add --no-<long> alternative option - false: omit --no-<long> alternative option - help ... (string) documentation (required if category is not - undocumented) - - Note that if an option defines a long option name with type 'bool', - mkoptions.py automatically generates a --no-<long> option to set the option - to false. - This behaviour can be explicitely disabled for options with attribute - alternate = false. - More information on how to use handler and predicates can be found - at the end of the README. - - - Example: - - [[option]] - name = "outputLanguage" - smt_name = "output-language" - category = "common" - short = "" - long = "output-lang=LANG" - type = "OutputLanguage" - default = "language::output::LANG_AUTO" - handler = "stringToOutputLanguage" - predicates = [] - includes = ["options/language.h"] - help = "force output language (default is \"auto\"; see --output-lang help)" - - -Further information (the old option package) -============================================ - - The options/ package supports a wide range of operations for responding to - an option being set. Roughly the three major concepts are: - - - handler to parse an option before setting its value. - - predicates to reject bad values for the option. - - More details on each class of custom handlers. - - - handler = "" - - Handlers provide support for parsing custom option types. - The signature for a handler call is: - - T custom-option-handler(std::string option, std::string optarg, - OptionsHandler* handler); - - where T is the type of the option. The suggested implementation is to - implement custom-handler as a dispatch into a function on handler with the - signature: - - T OptionsHandler::custom-option-handler(std::string option, - std::string optarg); - - The handlers are run before predicates. - Having multiple handlers is considered bad practice and is unsupported. - Handlers may have arbitrary side effects, but should call no code - inaccessible to liboptions. For side effects that are not required in order - to parse the option, using :predicate is recommended. Memory - management done by a handler needs to either be encapsulated by the type - and the destructor for the type or should *always* be owned by handler. - More elaborate memory management schemes are not currently supported. - - - predicates = [...] - - Predicates provide support for checking whether or not the value of an - option is acceptable. Predicates are run after handlers. - The signature for a predicate call is: - - void custom-predicate(std::string option, T value, - OptionsHandler* handler); - - where T is the type of the option. The suggested implementation is to - implement custom-predicate as a dispatch into a function on handler with - the signature: - - void OptionsHandler::custom-predicate(std::string option, T value); - - The predicates are run after handlers. Multiple - predicates may be defined for the same option, but the order they are run - is not guaranteed. Predicates may have arbitrary side effects, but should - call no code inaccessible to liboptions. diff --git a/src/options/README.md b/src/options/README.md new file mode 100644 index 000000000..df5686abc --- /dev/null +++ b/src/options/README.md @@ -0,0 +1,211 @@ +Specifying Modules +================== + +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"`) +* `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. + +In general, each attribute/value pair is required to be in one line. Comments +start with # and are not allowed in attribute/value lines. + +After parsing, a module is extended to have the following attributes: + +* `id`: lower-case version of the parsed `id` +* `id_cap`: upper-case version of `id` (used for the `Holder{id_cap}` class) +* `filename`: base filename for generated files (`"{id}_options"`) +* `header`: generated header name (`"options/{filename}.h"`) + + +Specifying Options +================== + +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 + +Optional attributes are: + +* `name` (string): the option name used to access the option internally + (`d_option.{module.id}.{name}`) +* `long` (string): long option name (without `--` prefix). Long option names may + have a suffix `=XXX` where `XXX` can be used to indicate the type of the + option value, e.g., `=MODE`, `=LANG`, `=N`, ... +* `short` (string): short option name consisting of one character (no `-` prefix + required), can be given if `long` is specified +* `alias` (list): alternative names that can be used instead of `long` +* `default` (string): default value, needs to be a valid C++ expression of type + `type` +* `alternate` (bool, default `true`): if `true`, adds `--no-{long}` alternative + option +* `mode` (list): used to define options whose type shall be an auto-generated + enum, more details below +* `handler` (string): alternate parsing routine for option types not covered by + the default parsers, more details below +* `predicates` (list): custom validation function to check whether an option + value is valid, more details below +* `includes` (list): additional header files required by handler or predicate + functions +* `help` (string): documentation string (required, unless the `category` is + `undocumented`) +* `help_mode` (string): documentation for the mode enum (required if `mode` is + given) + + +Handler functions +----------------- + +Custom handler functions are used to turn the option value from a `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 +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. + + +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`. + + +Mode options +------------ + +An option can be defined to hold one of a given set of values we call modes. +Doing so automatically defines an `enum class` for the set of modes and makes +the option accept one of the values from the enum. The enum class will be called +`{type}` and methods `operator<<` and `stringTo{enum}` are automatically +generated. A mode is defined by specifying `[[option.mode.{NAME}]]` after the +main `[[option]]` section with the following attributes: + +* `name` (string): the string value that corresponds to the enum value +* `help` (string): documentation about this mode + +Example: + + [[option]] + name = "bitblastMode" + category = "regular" + long = "bitblast=MODE" + type = "BitblastMode" + default = "LAZY" + help = "choose bitblasting mode, see --bitblast=help" + help_mode = "Bit-blasting modes." + [[option.mode.LAZY]] + name = "lazy" + help = "Separate boolean structure and term reasoning between the core SAT solver and the bit-vector SAT solver." + [[option.mode.EAGER]] + name = "eager" + help = "Bitblast eagerly to bit-vector SAT solver." + +The option can now be set with `--bitblast=lazy`, `(set-option :bitblast +eager)`, or `options::set("bitblast", "eager")`. + + +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: + +* `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` class +--------------- + +The `Options` class is the central entry point for regular usage of options. It +holds a `std::unique_ptr` to an "option holder" for every option module, that +can be accessed using references `{module}` (either as `const&` or `&`). These +holders hold the actual option data for the specific module. + +The holder types are forward declared and can thus only be accessed if one also +includes the appropriate `{module}_options.h`, which contains the proper +declaration for the holder class. + + +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`): +the actual option value as `{option.type} {option.name}` and a Boolean flag +`bool {option.name}__setByUser` 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 +============ + + [[option]] + category = "regular" + name = "decisionMode" + long = "decision=MODE" + alias = ["decision-mode"] + type = "DecisionMode" + default = "INTERNAL" + predicates = ["setDecisionModeStopOnly"] + help = "choose decision mode, see --decision=help" + help_mode = "Decision modes." + [[option.mode.INTERNAL]] + name = "internal" + help = "Use the internal decision heuristics of the SAT solver." + [[option.mode.JUSTIFICATION]] + name = "justification" + help = "An ATGP-inspired justification heuristic." + [[option.mode.RELEVANCY]] + name = "justification-stoponly" + help = "Use the justification heuristic only to stop early, not for decisions." + +This defines a new option that is accessible via +`d_options.{module.id}.decisionMode` and stores an automatically generated mode +`DecisionMode`, an enum class with the values `INTERNAL`, `JUSTIFICATION` and +`RELEVANCY`. From the outside, it can be set by `--decision=internal`, but also +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) diff --git a/src/options/base_handlers.h b/src/options/base_handlers.h deleted file mode 100644 index 86112a907..000000000 --- a/src/options/base_handlers.h +++ /dev/null @@ -1,87 +0,0 @@ -/****************************************************************************** - * Top contributors (to current version): - * Morgan Deters, Tim King, Mathias Preiner - * - * This file is part of the cvc5 project. - * - * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS - * in the top-level source directory and their institutional affiliations. - * All rights reserved. See the file COPYING in the top-level source - * directory for licensing information. - * **************************************************************************** - * - * [[ Add one-line brief description here ]] - * - * [[ Add lengthier description here ]] - * \todo document this file - */ - -#include "cvc5_private.h" - -#ifndef CVC5__BASE_HANDLERS_H -#define CVC5__BASE_HANDLERS_H - -#include <iostream> -#include <string> -#include <sstream> - -#include "options/option_exception.h" - -namespace cvc5 { -namespace options { - -template <template <class U> class Cmp> -class comparator { - long d_lbound; - double d_dbound; - bool d_hasLbound; - - public: - comparator(int i) : d_lbound(i), d_dbound(0.0), d_hasLbound(true) {} - comparator(long l) : d_lbound(l), d_dbound(0.0), d_hasLbound(true) {} - comparator(double d) : d_lbound(0), d_dbound(d), d_hasLbound(false) {} - template <class T> - void operator()(std::string option, const T& value) { - if((d_hasLbound && !(Cmp<T>()(value, T(d_lbound)))) || - (!d_hasLbound && !(Cmp<T>()(value, T(d_dbound))))) { - std::stringstream ss; - ss << option << ": " << value << " is not a legal setting"; - throw OptionException(ss.str()); - } - } -};/* class comparator */ - -struct greater : public comparator<std::greater> { - greater(int i) : comparator<std::greater>(i) {} - greater(long l) : comparator<std::greater>(l) {} - greater(double d) : comparator<std::greater>(d) {} -};/* struct greater */ - -struct greater_equal : public comparator<std::greater_equal> { - greater_equal(int i) : comparator<std::greater_equal>(i) {} - greater_equal(long l) : comparator<std::greater_equal>(l) {} - greater_equal(double d) : comparator<std::greater_equal>(d) {} -};/* struct greater_equal */ - -struct less : public comparator<std::less> { - less(int i) : comparator<std::less>(i) {} - less(long l) : comparator<std::less>(l) {} - less(double d) : comparator<std::less>(d) {} -};/* struct less */ - -struct less_equal : public comparator<std::less_equal> { - less_equal(int i) : comparator<std::less_equal>(i) {} - less_equal(long l) : comparator<std::less_equal>(l) {} - less_equal(double d) : comparator<std::less_equal>(d) {} -};/* struct less_equal */ - -struct not_equal : public comparator<std::not_equal_to> { - not_equal(int i) : comparator<std::not_equal_to>(i) {} - not_equal(long l) : comparator<std::not_equal_to>(l) {} - not_equal(double d) : comparator<std::not_equal_to>(d) {} -};/* struct not_equal_to */ - -} // namespace options -} // namespace cvc5 - -#endif /* CVC5__BASE_HANDLERS_H */ diff --git a/src/options/mkoptions.py b/src/options/mkoptions.py index 7e1cf68e4..e2fbd4cf1 100644 --- a/src/options/mkoptions.py +++ b/src/options/mkoptions.py @@ -210,6 +210,30 @@ def get_holder_ref_decls(modules): return concat_format(' options::Holder{id_cap}& {id};', modules) +def get_handler(option): + """Render handler call for assignment functions""" + optname = option.long_name if option.long else "" + if option.handler: + if option.type == 'void': + return 'opts.handler().{}("{}", option)'.format(option.handler, optname) + else: + return 'opts.handler().{}("{}", option, optionarg)'.format(option.handler, optname) + elif option.mode: + return 'stringTo{}(optionarg)'.format(option.type) + elif option.type != 'bool': + return 'handleOption<{}>("{}", option, optionarg)'.format(option.type, optname) + return None + + +def get_predicates(option): + """Render predicate calls for assignment functions""" + if not option.predicates: + return [] + optname = option.long_name if option.long else "" + assert option.type != 'void' + return ['opts.handler().{}("{}", option, value);'.format(x, optname) + for x in option.predicates] + class Module(object): """Options module. @@ -713,31 +737,10 @@ def codegen_all_modules(modules, build_dir, dst_dir, tpl_options_h, tpl_options_ sphinxgen.add(module, option) # Generate handler call - handler = None - if option.handler: - if option.type == 'void': - handler = 'opts.handler().{}(option)'.format(option.handler) - else: - handler = \ - 'opts.handler().{}(option, optionarg)'.format(option.handler) - elif option.mode: - handler = 'stringTo{}(optionarg)'.format(option.type) - elif option.type != 'bool': - handler = \ - 'handleOption<{}>(option, optionarg)'.format(option.type) + handler = get_handler(option) # Generate predicate calls - predicates = [] - if option.predicates: - if option.type == 'bool': - predicates = \ - ['opts.handler().{}(option, value);'.format(x) \ - for x in option.predicates] - else: - assert option.type != 'void' - predicates = \ - ['opts.handler().{}(option, value);'.format(x) \ - for x in option.predicates] + predicates = get_predicates(option) # Generate options_handler and getopt_long cases = [] @@ -813,7 +816,7 @@ def codegen_all_modules(modules, build_dir, dst_dir, tpl_options_h, tpl_options_ name=option.name, option='key')) elif option.handler: - h = 'handler->{handler}("{smtname}"' + h = 'handler->{handler}("{smtname}", key' if argument_req: h += ', optionarg' h += ');' diff --git a/src/options/options_handler.cpp b/src/options/options_handler.cpp index 1ac5ec56d..e109ab44c 100644 --- a/src/options/options_handler.cpp +++ b/src/options/options_handler.cpp @@ -67,10 +67,11 @@ void throwLazyBBUnsupported(options::SatSolverMode m) OptionsHandler::OptionsHandler(Options* options) : d_options(options) { } -unsigned long OptionsHandler::limitHandler(std::string option, - std::string optarg) +uint64_t OptionsHandler::limitHandler(const std::string& option, + const std::string& flag, + const std::string& optarg) { - unsigned long ms; + uint64_t ms; std::istringstream convert(optarg); if (!(convert >> ms)) { @@ -80,14 +81,18 @@ unsigned long OptionsHandler::limitHandler(std::string option, return ms; } -void OptionsHandler::setResourceWeight(std::string option, std::string optarg) +void OptionsHandler::setResourceWeight(const std::string& option, + const std::string& flag, + const std::string& optarg) { d_options->base.resourceWeightHolder.emplace_back(optarg); } // theory/quantifiers/options_handlers.h -void OptionsHandler::checkInstWhenMode(std::string option, InstWhenMode mode) +void OptionsHandler::checkInstWhenMode(const std::string& option, + const std::string& flag, + InstWhenMode mode) { if (mode == InstWhenMode::PRE_FULL) { @@ -97,7 +102,9 @@ void OptionsHandler::checkInstWhenMode(std::string option, InstWhenMode mode) } // theory/bv/options_handlers.h -void OptionsHandler::abcEnabledBuild(std::string option, bool value) +void OptionsHandler::abcEnabledBuild(const std::string& option, + const std::string& flag, + bool value) { #ifndef CVC5_USE_ABC if(value) { @@ -110,7 +117,9 @@ void OptionsHandler::abcEnabledBuild(std::string option, bool value) #endif /* CVC5_USE_ABC */ } -void OptionsHandler::abcEnabledBuild(std::string option, std::string value) +void OptionsHandler::abcEnabledBuild(const std::string& option, + const std::string& flag, + const std::string& value) { #ifndef CVC5_USE_ABC if(!value.empty()) { @@ -123,7 +132,9 @@ void OptionsHandler::abcEnabledBuild(std::string option, std::string value) #endif /* CVC5_USE_ABC */ } -void OptionsHandler::checkBvSatSolver(std::string option, SatSolverMode m) +void OptionsHandler::checkBvSatSolver(const std::string& option, + const std::string& flag, + SatSolverMode m) { if (m == SatSolverMode::CRYPTOMINISAT && !Configuration::isBuiltWithCryptominisat()) @@ -166,7 +177,9 @@ void OptionsHandler::checkBvSatSolver(std::string option, SatSolverMode m) } } -void OptionsHandler::checkBitblastMode(std::string option, BitblastMode m) +void OptionsHandler::checkBitblastMode(const std::string& option, + const std::string& flag, + BitblastMode m) { if (m == options::BitblastMode::LAZY) { @@ -185,7 +198,9 @@ void OptionsHandler::checkBitblastMode(std::string option, BitblastMode m) } } -void OptionsHandler::setBitblastAig(std::string option, bool arg) +void OptionsHandler::setBitblastAig(const std::string& option, + const std::string& flag, + bool arg) { if(arg) { if (d_options->bv.bitblastModeWasSetByUser) { @@ -211,8 +226,9 @@ szs\n\ + Print instantiations as SZS compliant proof.\n\ "; -InstFormatMode OptionsHandler::stringToInstFormatMode(std::string option, - std::string optarg) +InstFormatMode OptionsHandler::stringToInstFormatMode(const std::string& option, + const std::string& flag, + const std::string& optarg) { if(optarg == "default") { return InstFormatMode::DEFAULT; @@ -228,24 +244,30 @@ InstFormatMode OptionsHandler::stringToInstFormatMode(std::string option, } // decision/options_handlers.h -void OptionsHandler::setDecisionModeStopOnly(std::string option, DecisionMode m) +void OptionsHandler::setDecisionModeStopOnly(const std::string& option, + const std::string& flag, + DecisionMode m) { d_options->decision.decisionStopOnly = (m == DecisionMode::RELEVANCY); } -void OptionsHandler::setProduceAssertions(std::string option, bool value) +void OptionsHandler::setProduceAssertions(const std::string& option, + const std::string& flag, + bool value) { d_options->smt.produceAssertions = value; d_options->smt.interactiveMode = value; } -void OptionsHandler::setStats(const std::string& option, bool value) +void OptionsHandler::setStats(const std::string& option, + const std::string& flag, + bool value) { #ifndef CVC5_STATISTICS_ON if (value) { std::stringstream ss; - ss << "option `" << option + ss << "option `" << flag << "' requires a statistics-enabled build of cvc5; this binary was not " "built with statistics support"; throw OptionException(ss.str()); @@ -282,18 +304,25 @@ void OptionsHandler::setStats(const std::string& option, bool value) } } -void OptionsHandler::threadN(std::string option) { - throw OptionException(option + " is not a real option by itself. Use e.g. --thread0=\"--random-seed=10 --random-freq=0.02\" --thread1=\"--random-seed=20 --random-freq=0.05\""); +void OptionsHandler::threadN(const std::string& option, const std::string& flag) +{ + throw OptionException(flag + " is not a real option by itself. Use e.g. --thread0=\"--random-seed=10 --random-freq=0.02\" --thread1=\"--random-seed=20 --random-freq=0.05\""); } // expr/options_handlers.h -void OptionsHandler::setDefaultExprDepthPredicate(std::string option, int depth) { +void OptionsHandler::setDefaultExprDepthPredicate(const std::string& option, + const std::string& flag, + int depth) +{ if(depth < -1) { throw OptionException("--expr-depth requires a positive argument, or -1."); } } -void OptionsHandler::setDefaultDagThreshPredicate(std::string option, int dag) { +void OptionsHandler::setDefaultDagThreshPredicate(const std::string& option, + const std::string& flag, + int dag) +{ if(dag < 0) { throw OptionException("--dag-thresh requires a nonnegative argument."); } @@ -312,12 +341,16 @@ static void print_config_cond (const char * str, bool cond = false) { print_config(str, cond ? "yes" : "no"); } -void OptionsHandler::copyright(std::string option) { +void OptionsHandler::copyright(const std::string& option, + const std::string& flag) +{ std::cout << Configuration::copyright() << std::endl; exit(0); } -void OptionsHandler::showConfiguration(std::string option) { +void OptionsHandler::showConfiguration(const std::string& option, + const std::string& flag) +{ std::cout << Configuration::about() << std::endl; print_config ("version", Configuration::getVersionString()); @@ -385,7 +418,8 @@ static void printTags(unsigned ntags, char const* const* tags) std::cout << std::endl; } -void OptionsHandler::showDebugTags(std::string option) +void OptionsHandler::showDebugTags(const std::string& option, + const std::string& flag) { if (!Configuration::isDebugBuild()) { @@ -399,7 +433,8 @@ void OptionsHandler::showDebugTags(std::string option) exit(0); } -void OptionsHandler::showTraceTags(std::string option) +void OptionsHandler::showTraceTags(const std::string& option, + const std::string& flag) { if (!Configuration::isTracingBuild()) { @@ -431,7 +466,9 @@ static std::string suggestTags(char const* const* validTags, return didYouMean.getMatchAsString(inputTag); } -void OptionsHandler::enableTraceTag(std::string option, std::string optarg) +void OptionsHandler::enableTraceTag(const std::string& option, + const std::string& flag, + const std::string& optarg) { if(!Configuration::isTracingBuild()) { @@ -453,7 +490,9 @@ void OptionsHandler::enableTraceTag(std::string option, std::string optarg) Trace.on(optarg); } -void OptionsHandler::enableDebugTag(std::string option, std::string optarg) +void OptionsHandler::enableDebugTag(const std::string& option, + const std::string& flag, + const std::string& optarg) { if (!Configuration::isDebugBuild()) { @@ -484,8 +523,9 @@ void OptionsHandler::enableDebugTag(std::string option, std::string optarg) Trace.on(optarg); } -OutputLanguage OptionsHandler::stringToOutputLanguage(std::string option, - std::string optarg) +OutputLanguage OptionsHandler::stringToOutputLanguage(const std::string& option, + const std::string& flag, + const std::string& optarg) { if(optarg == "help") { d_options->base.languageHelp = true; @@ -502,8 +542,9 @@ OutputLanguage OptionsHandler::stringToOutputLanguage(std::string option, Unreachable(); } -InputLanguage OptionsHandler::stringToInputLanguage(std::string option, - std::string optarg) +InputLanguage OptionsHandler::stringToInputLanguage(const std::string& option, + const std::string& flag, + const std::string& optarg) { if(optarg == "help") { d_options->base.languageHelp = true; @@ -520,7 +561,9 @@ InputLanguage OptionsHandler::stringToInputLanguage(std::string option, } /* options/base_options_handlers.h */ -void OptionsHandler::setVerbosity(std::string option, int value) +void OptionsHandler::setVerbosity(const std::string& option, + const std::string& flag, + int value) { if(Configuration::isMuzzledBuild()) { DebugChannel.setStream(&cvc5::null_os); @@ -550,14 +593,18 @@ void OptionsHandler::setVerbosity(std::string option, int value) } } -void OptionsHandler::increaseVerbosity(std::string option) { +void OptionsHandler::increaseVerbosity(const std::string& option, + const std::string& flag) +{ d_options->base.verbosity += 1; - setVerbosity(option, options::verbosity()); + setVerbosity(option, flag, d_options->base.verbosity); } -void OptionsHandler::decreaseVerbosity(std::string option) { +void OptionsHandler::decreaseVerbosity(const std::string& option, + const std::string& flag) +{ d_options->base.verbosity -= 1; - setVerbosity(option, options::verbosity()); + setVerbosity(option, flag, d_options->base.verbosity); } } // namespace options diff --git a/src/options/options_handler.h b/src/options/options_handler.h index 4b9b1c0ae..9aee1df22 100644 --- a/src/options/options_handler.h +++ b/src/options/options_handler.h @@ -19,9 +19,9 @@ #define CVC5__OPTIONS__OPTIONS_HANDLER_H #include <ostream> +#include <sstream> #include <string> -#include "options/base_handlers.h" #include "options/bv_options.h" #include "options/decision_options.h" #include "options/language.h" @@ -44,72 +44,122 @@ class OptionsHandler { public: OptionsHandler(Options* options); - void unsignedGreater0(const std::string& option, unsigned value) { - options::greater(0)(option, value); + template <typename T> + void geqZero(const std::string& option, + const std::string& flag, + T value) const + { + if (value < 0) + { + std::stringstream ss; + ss << flag << ": " << value << " is not a legal setting, should be " + << value << " >= 0."; + throw OptionException(ss.str()); + } } - - void unsignedLessEqual2(const std::string& option, unsigned value) { - options::less_equal(2)(option, value); - } - - void doubleGreaterOrEqual0(const std::string& option, double value) { - options::greater_equal(0.0)(option, value); - } - - void doubleLessOrEqual1(const std::string& option, double value) { - options::less_equal(1.0)(option, value); + template <typename T> + void betweenZeroAndOne(const std::string& option, + const std::string& flag, + T value) const + { + if (value < 0 || value > 1) + { + std::stringstream ss; + ss << flag << ": " << value + << " is not a legal setting, should be 0 <= " << flag << " <= 1."; + throw OptionException(ss.str()); + } } // theory/quantifiers/options_handlers.h - void checkInstWhenMode(std::string option, InstWhenMode mode); + void checkInstWhenMode(const std::string& option, + const std::string& flag, + InstWhenMode mode); // theory/bv/options_handlers.h - void abcEnabledBuild(std::string option, bool value); - void abcEnabledBuild(std::string option, std::string value); - - template<class T> void checkSatSolverEnabled(std::string option, T m); - - void checkBvSatSolver(std::string option, SatSolverMode m); - void checkBitblastMode(std::string option, BitblastMode m); - - void setBitblastAig(std::string option, bool arg); + void abcEnabledBuild(const std::string& option, + const std::string& flag, + bool value); + void abcEnabledBuild(const std::string& option, + const std::string& flag, + const std::string& value); + + template <class T> + void checkSatSolverEnabled(const std::string& option, + const std::string& flag, + T m); + + void checkBvSatSolver(const std::string& option, + const std::string& flag, + SatSolverMode m); + void checkBitblastMode(const std::string& option, + const std::string& flag, + BitblastMode m); + + void setBitblastAig(const std::string& option, + const std::string& flag, + bool arg); // printer/options_handlers.h - InstFormatMode stringToInstFormatMode(std::string option, std::string optarg); + InstFormatMode stringToInstFormatMode(const std::string& option, + const std::string& flag, + const std::string& optarg); // decision/options_handlers.h - void setDecisionModeStopOnly(std::string option, DecisionMode m); + void setDecisionModeStopOnly(const std::string& option, + const std::string& flag, + DecisionMode m); /** * Throws a ModalException if this option is being set after final * initialization. */ - void setProduceAssertions(std::string option, bool value); + void setProduceAssertions(const std::string& option, + const std::string& flag, + bool value); - void setStats(const std::string& option, bool value); + void setStats(const std::string& option, const std::string& flag, bool value); - unsigned long limitHandler(std::string option, std::string optarg); - void setResourceWeight(std::string option, std::string optarg); + uint64_t limitHandler(const std::string& option, + const std::string& flag, + const std::string& optarg); + void setResourceWeight(const std::string& option, + const std::string& flag, + const std::string& optarg); /* expr/options_handlers.h */ - void setDefaultExprDepthPredicate(std::string option, int depth); - void setDefaultDagThreshPredicate(std::string option, int dag); + void setDefaultExprDepthPredicate(const std::string& option, + const std::string& flag, + int depth); + void setDefaultDagThreshPredicate(const std::string& option, + const std::string& flag, + int dag); /* main/options_handlers.h */ - void copyright(std::string option); - void showConfiguration(std::string option); - void showDebugTags(std::string option); - void showTraceTags(std::string option); - void threadN(std::string option); + void copyright(const std::string& option, const std::string& flag); + void showConfiguration(const std::string& option, const std::string& flag); + void showDebugTags(const std::string& option, const std::string& flag); + void showTraceTags(const std::string& option, const std::string& flag); + void threadN(const std::string& option, const std::string& flag); /* options/base_options_handlers.h */ - void setVerbosity(std::string option, int value); - void increaseVerbosity(std::string option); - void decreaseVerbosity(std::string option); - OutputLanguage stringToOutputLanguage(std::string option, std::string optarg); - InputLanguage stringToInputLanguage(std::string option, std::string optarg); - void enableTraceTag(std::string option, std::string optarg); - void enableDebugTag(std::string option, std::string optarg); + void setVerbosity(const std::string& option, + const std::string& flag, + int value); + void increaseVerbosity(const std::string& option, const std::string& flag); + void decreaseVerbosity(const std::string& option, const std::string& flag); + OutputLanguage stringToOutputLanguage(const std::string& option, + const std::string& flag, + const std::string& optarg); + InputLanguage stringToInputLanguage(const std::string& option, + const std::string& flag, + const std::string& optarg); + void enableTraceTag(const std::string& option, + const std::string& flag, + const std::string& optarg); + void enableDebugTag(const std::string& option, + const std::string& flag, + const std::string& optarg); private: @@ -121,8 +171,10 @@ public: }; /* class OptionHandler */ -template<class T> -void OptionsHandler::checkSatSolverEnabled(std::string option, T m) +template <class T> +void OptionsHandler::checkSatSolverEnabled(const std::string& option, + const std::string& flag, + T m) { #if !defined(CVC5_USE_CRYPTOMINISAT) && !defined(CVC5_USE_CADICAL) \ && !defined(CVC5_USE_KISSAT) diff --git a/src/options/options_template.cpp b/src/options/options_template.cpp index e909a5f0a..2c22065c2 100644 --- a/src/options/options_template.cpp +++ b/src/options/options_template.cpp @@ -58,7 +58,6 @@ extern int optreset; ${headers_module}$ #include "base/cvc5config.h" -#include "options/base_handlers.h" ${headers_handler}$ @@ -82,7 +81,9 @@ thread_local Options* Options::s_current = NULL; */ template <class T, bool is_numeric, bool is_integer> struct OptionHandler { - static T handle(std::string option, std::string optionarg); + static T handle(const std::string& option, + const std::string& flag, + const std::string& optionarg); };/* struct OptionHandler<> */ /** Variant for integral C++ types */ @@ -99,32 +100,35 @@ struct OptionHandler<T, true, true> { return str.find('-') != std::string::npos; } - static T handle(const std::string& option, const std::string& optionarg) { + static T handle(const std::string& option, + const std::string& flag, + const std::string& optionarg) + { try { T i; bool success = stringToInt(i, optionarg); if(!success){ - throw OptionException(option + ": failed to parse "+ optionarg + - " as an integer of the appropriate type."); + throw OptionException(flag + ": failed to parse " + optionarg + + " as an integer of the appropriate type."); } // Depending in the platform unsigned numbers with '-' signs may parse. // Reject these by looking for any minus if it is not signed. if( (! std::numeric_limits<T>::is_signed) && containsMinus(optionarg) ) { // unsigned type but user gave negative argument - throw OptionException(option + " requires a nonnegative argument"); + throw OptionException(flag + " requires a nonnegative argument"); } else if(i < std::numeric_limits<T>::min()) { // negative overflow for type std::stringstream ss; - ss << option << " requires an argument >= " - << std::numeric_limits<T>::min(); + ss << flag + << " requires an argument >= " << std::numeric_limits<T>::min(); throw OptionException(ss.str()); } else if(i > std::numeric_limits<T>::max()) { // positive overflow for type std::stringstream ss; - ss << option << " requires an argument <= " - << std::numeric_limits<T>::max(); + ss << flag + << " requires an argument <= " << std::numeric_limits<T>::max(); throw OptionException(ss.str()); } @@ -137,7 +141,7 @@ struct OptionHandler<T, true, true> { // } } catch(std::invalid_argument&) { // user gave something other than an integer - throw OptionException(option + " requires an integer argument"); + throw OptionException(flag + " requires an integer argument"); } } };/* struct OptionHandler<T, true, true> */ @@ -145,29 +149,33 @@ struct OptionHandler<T, true, true> { /** Variant for numeric but non-integral C++ types */ template <class T> struct OptionHandler<T, true, false> { - static T handle(std::string option, std::string optionarg) { - std::stringstream in(optionarg); + static T handle(const std::string& option, + const std::string& flag, + const std::string& optionarg) + { + std::stringstream inss(optionarg); long double r; - in >> r; - if(! in.eof()) { + inss >> r; + if (!inss.eof()) + { // we didn't consume the whole string (junk at end) - throw OptionException(option + " requires a numeric argument"); + throw OptionException(flag + " requires a numeric argument"); } if(! std::numeric_limits<T>::is_signed && r < 0.0) { // unsigned type but user gave negative value - throw OptionException(option + " requires a nonnegative argument"); + throw OptionException(flag + " requires a nonnegative argument"); } else if(r < -std::numeric_limits<T>::max()) { // negative overflow for type std::stringstream ss; - ss << option << " requires an argument >= " - << -std::numeric_limits<T>::max(); + ss << flag + << " requires an argument >= " << -std::numeric_limits<T>::max(); throw OptionException(ss.str()); } else if(r > std::numeric_limits<T>::max()) { // positive overflow for type std::stringstream ss; - ss << option << " requires an argument <= " - << std::numeric_limits<T>::max(); + ss << flag + << " requires an argument <= " << std::numeric_limits<T>::max(); throw OptionException(ss.str()); } @@ -178,7 +186,10 @@ struct OptionHandler<T, true, false> { /** Variant for non-numeric C++ types */ template <class T> struct OptionHandler<T, false, false> { - static T handle(std::string option, std::string optionarg) { + static T handle(const std::string& option, + const std::string& flag, + const std::string& optionarg) + { T::unsupported_handleOption_call___please_write_me; // The above line causes a compiler error if this version of the template // is ever instantiated (meaning that a specialization is missing). So @@ -191,36 +202,26 @@ struct OptionHandler<T, false, false> { /** Handle an option of type T in the default way. */ template <class T> -T handleOption(std::string option, std::string optionarg) { - return OptionHandler<T, std::numeric_limits<T>::is_specialized, std::numeric_limits<T>::is_integer>::handle(option, optionarg); +T handleOption(const std::string& option, + const std::string& flag, + const std::string& optionarg) +{ + return OptionHandler<T, + std::numeric_limits<T>::is_specialized, + std::numeric_limits<T>::is_integer>::handle(option, + flag, + optionarg); } /** Handle an option of type std::string in the default way. */ template <> -std::string handleOption<std::string>(std::string option, std::string optionarg) { +std::string handleOption<std::string>(const std::string& option, + const std::string& flag, + const std::string& optionarg) +{ return optionarg; } -/** - * Run handler, and any user-given predicates, for option T. - * If a user specifies a :handler or :predicates, it overrides this. - */ -template <class T> -typename T::type runHandlerAndPredicates(T, std::string option, std::string optionarg, options::OptionsHandler* handler) { - // By default, parse the option argument in a way appropriate for its type. - // E.g., for "unsigned int" options, ensure that the provided argument is - // a nonnegative integer that fits in the unsigned int type. - - return handleOption<typename T::type>(option, optionarg); -} - -template <class T> -void runBoolPredicates(T, std::string option, bool b, options::OptionsHandler* handler) { - // By default, nothing to do for bool. Users add things with - // :predicate in options files to provide custom checking routines - // that can throw exceptions. -} - Options::Options(OptionsListener* ol) : d_handler(new options::OptionsHandler(this)), // clang-format off diff --git a/src/options/prop_options.toml b/src/options/prop_options.toml index 26d7a451b..eda5ea963 100644 --- a/src/options/prop_options.toml +++ b/src/options/prop_options.toml @@ -8,7 +8,7 @@ name = "SAT Layer" long = "random-freq=P" type = "double" default = "0.0" - predicates = ["doubleGreaterOrEqual0", "doubleLessOrEqual1"] + predicates = ["betweenZeroAndOne"] help = "sets the frequency of random decisions in the sat solver (P=0.0 by default)" [[option]] @@ -24,7 +24,7 @@ name = "SAT Layer" category = "regular" type = "double" default = "0.95" - predicates = ["doubleGreaterOrEqual0", "doubleLessOrEqual1"] + predicates = ["betweenZeroAndOne"] help = "variable activity decay factor for Minisat" [[option]] @@ -32,7 +32,7 @@ name = "SAT Layer" category = "regular" type = "double" default = "0.999" - predicates = ["doubleGreaterOrEqual0", "doubleLessOrEqual1"] + predicates = ["betweenZeroAndOne"] help = "clause activity decay factor for Minisat" [[option]] @@ -49,7 +49,7 @@ name = "SAT Layer" long = "restart-int-inc=F" type = "double" default = "3.0" - predicates = ["doubleGreaterOrEqual0"] + predicates = ["geqZero"] help = "sets the restart interval increase factor for the sat solver (F=3.0 by default)" [[option]] |