diff options
Diffstat (limited to 'src/options/base_options')
| -rw-r--r-- | src/options/base_options | 126 |
1 files changed, 101 insertions, 25 deletions
diff --git a/src/options/base_options b/src/options/base_options index edbef801d..7346641c7 100644 --- a/src/options/base_options +++ b/src/options/base_options @@ -3,31 +3,34 @@ # # This is essentially a shell script interpreted with special commands. # -# Lines starting with whitespace are special. They are passed in their entirety (minus -# the first whitespace char) to the "doc" command. Lines starting with a single slash -# are stripped of this initial character and interpreted by the "doc-alt" command. A period -# "." in the first column of a line, followed optionally by whitespace but without any other -# content on the line, is interpreted as an empty string passed to doc. (This allows -# multi-paragraph documentation for options.) Lines may be continued with a backslash (\) -# at the end of a line. +# Lines starting with whitespace are special. They are passed in their entirety +# (minus the first whitespace char) to the "doc" command. Lines starting with a +# single slash are stripped of this initial character and interpreted by the +# "doc-alt" command. A period "." in the first column of a line, followed +# optionally by whitespace but without any other content on the line, is +# interpreted as an empty string passed to doc. (This allows multi-paragraph +# documentation for options.) Lines may be continued with a backslash (\) at the +# end of a line. # # commands are: # # module ID "include-file" name # -# Identifies the module. Must be the first command in the file. ID is a suitable -# identifier for a preprocessor definition, and should be unique; name is a "pretty" -# name used for the benefit of the end CVC4 user in, e.g., option listings. +# Identifies the module. Must be the first command in the file. ID is a +# suitable identifier for a preprocessor definition, and should be unique; +# name is a "pretty" name used for the benefit of the end CVC4 user in, e.g., +# option listings. # # common-option SPECIFICATION # option SPECIFICATION # expert-option SPECIFICATION # undocumented-option SPECIFICATION # -# These commands declare (respectively) common options presented first to the user, -# standard options that the user might want to see with "--help" documentation, -# expert options that should be marked as expert-only, and options that should not -# appear in normal option documentation (even if documentation is included here). +# These commands declare (respectively) common options presented first to the +# user, standard options that the user might want to see with "--help" +# documentation, expert options that should be marked as expert-only, and +# options that should not appear in normal option documentation (even if +# documentation is included here). # # SPECIFICATIONs take this form: # @@ -36,9 +39,13 @@ # | :default C++-expression # | :handler custom-option-handlers.. # | :handler-include include-files.. +# | :predicate custom-option-handlers.. +# | :predicate-include include-files.. +# | :notify custom-option-notifications.. # | :read-only # | :read-write # | :link linked-options.. +# | :link-smt linked-option [value] # # common-alias ALIAS_SPECIFICATION # alias ALIAS_SPECIFICATION @@ -74,7 +81,76 @@ # # endmodule # -# This file should end with the "endmodule" command, and nothing should follow it. +# This file should end with the "endmodule" command, and nothing should +# follow it. +# +# +# The options/ package supports a wide range of operations for responding to +# an option being set. Roughly the three major concepts are: +# - :handler is to parse an option before setting its value. +# - :predicate is to reject bad values for the option. +# - :notify is used for dynamic dispatch after an option is assigned. +# +# More details on each class of custom handlers. +# :handler custom-option-handler +# Handlers provide support for parsing custom types and parsing for options. +# 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. +# +# :predicate custom-predicate +# Predicates provide support for checking whether or not the value of an +# 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. +# +# :notify custom-notification +# 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. # module BASE "options/base_options.h" Base @@ -85,9 +161,9 @@ option in std::istream* :default &std::cin :include <iosfwd> option out std::ostream* :default &std::cout :include <iosfwd> option err std::ostream* :default &std::cerr :include <iosfwd> -common-option inputLanguage input-language -L --lang=LANG InputLanguage :handler CVC4::options::stringToInputLanguage :include "options/language.h" :default language::input::LANG_AUTO :read-write +common-option inputLanguage input-language -L --lang=LANG InputLanguage :handler stringToInputLanguage :include "options/language.h" :default language::input::LANG_AUTO :read-write force input language (default is "auto"; see --lang help) -common-option outputLanguage output-language --output-lang=LANG OutputLanguage :handler CVC4::options::stringToOutputLanguage :include "options/language.h" :default language::output::LANG_AUTO :read-write +common-option outputLanguage output-language --output-lang=LANG OutputLanguage :handler stringToOutputLanguage :include "options/language.h" :default language::output::LANG_AUTO :read-write force output language (default is "auto"; see --output-lang help) option languageHelp bool @@ -96,18 +172,18 @@ option languageHelp bool undocumented-alias --language=L = --lang=L undocumented-alias --output-language=L = --output-lang=L -option verbosity verbosity int :read-write :default 0 :predicate CVC4::options::setVerbosity :predicate-include "options/base_handlers.h" +option verbosity verbosity int :read-write :default 0 :predicate setVerbosity the verbosity level of CVC4 -common-option - -v --verbose void :handler CVC4::options::increaseVerbosity +common-option - -v --verbose void :handler increaseVerbosity increase verbosity (may be repeated) -common-option - -q --quiet void :handler CVC4::options::decreaseVerbosity +common-option - -q --quiet void :handler decreaseVerbosity decrease verbosity (may be repeated) -common-option statistics statistics --stats bool :predicate CVC4::options::statsEnabledBuild :predicate-include "options/options_handler_interface.h" +common-option statistics statistics --stats bool :predicate statsEnabledBuild give statistics on exit undocumented-alias --statistics = --stats undocumented-alias --no-statistics = --no-stats -option statsEveryQuery --stats-every-query bool :default false :link --stats +option statsEveryQuery --stats-every-query bool :default false :link --stats :link-smt statistics in incremental mode, print stats after every satisfiability or validity query undocumented-alias --statistics-every-query = --stats-every-query undocumented-alias --no-statistics-every-query = --no-stats-every-query @@ -123,12 +199,12 @@ option parseOnly parse-only --parse-only bool :read-write option preprocessOnly preprocess-only --preprocess-only bool exit after preprocessing input -option - trace -t --trace=TAG argument :handler CVC4::options::addTraceTag +option - trace -t --trace=TAG argument :handler addTraceTag trace something (e.g. -t pushpop), can repeat -option - debug -d --debug=TAG argument :handler CVC4::options::addDebugTag +option - debug -d --debug=TAG argument :handler addDebugTag debug something (e.g. -d arith), can repeat -option printSuccess print-success --print-success bool :predicate CVC4::options::setPrintSuccess :predicate-include "options/options_handler_interface.h" +option printSuccess print-success --print-success bool :notify notifyPrintSuccess print the "success" output required of SMT-LIBv2 alias --smtlib-strict = --lang=smt2 --output-lang=smt2 --strict-parsing --default-expr-depth=-1 --print-success --incremental --abstract-values |