1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
|
#
# Option specification file for CVC4
#
# 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.
#
# 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.
#
# 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).
#
# SPECIFICATIONs take this form:
#
# SPECIFICATION ::= (internal-name | -) [smt-option-name] [-short-option/-alternate-short-option] [--long-option/--alternate-long-option] C++-type [ATTRIBUTEs...]
# ATTRIBUTE ::= :include include-files..
# | :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
# expert-alias ALIAS_SPECIFICATION
# undocumented-alias ALIAS_SPECIFICATION
#
# ALIAS_SPECIFICATION ::= (-short-option | --long-option) = (-option[=argument] | --long-option[=argument])+
# | (-short-option=ARG | --long-option=ARG) = (-option[=ARG|argument] | --long-option[=ARG|argument])+
#
# The alias command creates a new short or long option, and binds it
# to act the same way as if the options to the right of "=" were passed.
# For example, if there are options to --disable-warning-1 and
# --disable-warning-2, etc., a useful alias might be:
#
# alias --disable-all-warnings = --disable-warning-1 --disable-warning-2
#
# It's also possible to pass an argument through to another option.
# This alias makes "--output-language" synonymous with "--output-lang".
# Without the "=L" parts, --output-language would not take an argument,
# and option processing would fail (because --output-lang expects one).
#
# alias --output-language=L = --output-lang=L
#
# You can also ignore such an argument:
#
# alias --some-option=VALUE = --other-option --option2=foo --option3=bar
#
# or use it for multiple options on the right-hand side, etc.
#
# warning message
#
# Warn about something during processing (like a FIXME).
#
# endmodule
#
# 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
option binary_name std::string
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 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 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
# Allow also --language and --output-language, it's a common mistake to
# type these, but no need to document it.
undocumented-alias --language=L = --lang=L
undocumented-alias --output-language=L = --output-lang=L
option verbosity verbosity int :read-write :default 0 :predicate setVerbosity
the verbosity level of CVC4
common-option - -v --verbose void :handler increaseVerbosity
increase verbosity (may be repeated)
common-option - -q --quiet void :handler decreaseVerbosity
decrease verbosity (may be repeated)
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 :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
option statsHideZeros --stats-hide-zeros/--stats-show-zeros bool :default false
hide statistics which are zero
/show statistics even when they are zero (default)
undocumented-alias --hide-zero-stats = --stats-hide-zeros
undocumented-alias --show-zero-stats = --stats-show-zeros
option parseOnly parse-only --parse-only bool :read-write
exit after parsing input
option preprocessOnly preprocess-only --preprocess-only bool
exit after preprocessing input
option - trace -t --trace=TAG argument :handler addTraceTag
trace something (e.g. -t pushpop), can repeat
option - debug -d --debug=TAG argument :handler addDebugTag
debug something (e.g. -d arith), can repeat
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
SMT-LIBv2 compliance mode (implies other options)
endmodule
|
