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
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
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", "--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 --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, CVC5::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.
|
