From: Gereon Kremer Date: Wed, 16 Jun 2021 08:46:01 +0000 (+0200) Subject: Properly consider aliases in option handlers (#6683) X-Git-Tag: cvc5-1.0.0~1595 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=6ae5647e754925a5c963d2b92c7255d7e0de6b03;p=cvc5.git Properly consider aliases in option handlers (#6683) This PR makes sure that option handlers have access to both the canonical option name and the option name that was actually used. It also updates the options README and gets rid of the base_handlers.h of which only a fraction was used. --- 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::() - 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- alternative option - false: omit --no- 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- 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 -#include -#include - -#include "options/option_exception.h" - -namespace cvc5 { -namespace options { - -template