diff options
Diffstat (limited to 'src/options/README')
| -rw-r--r-- | src/options/README | 229 |
1 files changed, 229 insertions, 0 deletions
diff --git a/src/options/README b/src/options/README new file mode 100644 index 000000000..ac371e835 --- /dev/null +++ b/src/options/README @@ -0,0 +1,229 @@ +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 and/or aliases. + + 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/notifies + notifies ... (list) notifications to call when option is set + links ... (list) additional options to set after this option is set + read_only ... (bool) true: option should not provide a ::set method, + false (default): option should provide a ::set + method to set the option value + 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, predicates and notifies 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"] + notifies = [] + links = [] + read_only = false + help = "force output language (default is \"auto\"; see --output-lang help)" + + + If an alternate option is generated, the linked options defined via attribute + links are not considered. If you want to define links for an alternate option + --no-<long> for an existing option <long>, you can define an alias with long + option no-<long>. This overwrites the default --no-<long> behaviour and + creates the linked options. + + +Aliases +======= + + Aliases can be defined with the [[alias]] tag, which creates a new long + option and binds it to the list of long options specified via the 'links' + attributes. + + + The required attributes are: + + category ... (string) common | expert | regular | undocumented + long ... (string) long option name + links ... (list) list of long options to set + + Optional attributes are: + + help ... (string) documentation (only option for category undocumented) + + + Example: + + [[alias]] + category = "regular" + long = "smtlib-strict" + links = ["--lang=smt2", "--output-lang=smt2", "--strict-parsing", "--default-expr-depth=-1", "--print-success", "--incremental", "--abstract-values"] + help = "SMT-LIBv2 compliance mode (implies other options)" + + + This example creates a regular option with the long option name + 'smtlib-strict', which links to the long options given as a list 'links'. + Calling + + --smtlib-strict + + is equivalent to specifying the options + + --lang=smt2 --output-lang=smt2 --strict-parsing --default-expr-depth=-1 --print-success --incremental --abstract-values + + + It's also possible to pass an argument through to another option. + + Example: + + [[alias]] + category = "undocumented" + long = "output-language=L" + links = ["--output-lang=L"] + + This alias makes --output-language synonymous with --output-lang and passes + argument L through to --output-lang. The placeholer name (in this example + 'L') of the argument can be arbitrarily chosen and can be referenced multiple + times in 'links'. + + + +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. + - notifies for dynamic dispatch after an option is assigned. + + 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 and notifications. + 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. Use :notify to + achieve dynamic dispatch outside of base/, lib/, and options/. 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 and before + notifications. + 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 and before notifications. 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. Use :notify to + achieve dynamic dispatch outside of base/, lib/, and options/. + Predicates are expected to reject bad value for the option by throwing an + OptionsException. + + - notifies = [...] + + This allows for the installation of custom post-processing callbacks using + the Listener infrastructure. custom-option-notification is a C++ function + that is called after the assignment of the option is updated. + The normal usage of an notify is to call a Listener that is registered for + this specific option. This is how dynamic dispatch outside of the + liboptions package should always be done. + The signature of custom-option-notification should take an option name as + well as an OptionsHandler*. + + void custom-notification( + const std::string& option, CVC4::options::OptionsHandler* handler); + + The name is provided so multiple options can use the same notification + implementation. + This is called after all handlers and predicates have been run. + Formally, this is always placed at the end of either the generated + Options::assign or Options::assignBool function for the option. + Because of this :notify cannot be used with void type options. + Users of this feature should *always* check the code generated in + builds/src/options/options.cpp for the correctness of the placement of the + generated code. The Listener notify() function is allowed to throw + an arbitrary std::exception. |