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::() 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- 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, 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- for an existing option , you can define an alias with long option no-. This overwrites the default --no- 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.