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
|
Specifying Modules
==================
Every options module, that is a group of options that belong together in some
way, is declared in its own file in `options/{module name}_options.toml`. 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"`)
Additional, a module can optionally be defined to be public. A public module
includes `cvc5_public.h` instead of `cvc5_private.h` can thus be included from
"external" code like the parser or the main driver.
* `public` (bool): make option module public
A module defines 0 or more options.
In general, each attribute/value pair is required to be in one line. Comments
start with # and are not allowed in attribute/value lines.
After parsing, a module is extended to have the following attributes:
* `id`: lower-case version of the parsed `id`
* `id_cap`: upper-case version of `id` (used for the `Holder{id_cap}` class)
* `filename`: base filename for generated files (`"{id}_options"`)
* `header`: generated header name (`"options/{filename}.h"`)
Specifying Options
==================
Options can be defined within a module file with the `[[option]]` tag, the
required attributes for an option are:
* `category` (string): one of `common`, `expert`, `regular`, or `undocumented`
* `type` (string): the C++ type of the option value
Optional attributes are:
* `name` (string): the option name used to access the option internally
(`d_option.{module.id}.{name}`)
* `long` (string): long option name (without `--` prefix). 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`, ...
* `short` (string): short option name consisting of one character (no `-` prefix
required), can be given if `long` is specified
* `alias` (list): alternative names that can be used instead of `long`
* `default` (string): default value, needs to be a valid C++ expression of type
`type`
* `alternate` (bool, default `true`): if `true`, adds `--no-{long}` alternative
option
* `mode` (list): used to define options whose type shall be an auto-generated
enum, more details below
* `handler` (string): alternate parsing routine for option types not covered by
the default parsers, more details below
* `predicates` (list): custom validation function to check whether an option
value is valid, more details below
* `includes` (list): additional header files required by handler or predicate
functions
* `help` (string): documentation string (required, unless the `category` is
`undocumented`)
* `help_mode` (string): documentation for the mode enum (required if `mode` is
given)
Handler functions
-----------------
Custom handler functions are used to turn the option value from a `std::string`
into the type specified by `type`. Standard handler functions are provided for
basic types (`std::string`, `bool`, integer types and floating point types) as
well as enums specified by `mode`. A custom handler function needs to be member
function of `options::OptionsHandler` with signature `{type} {handler}(const
std::string& option, const std::string& flag, const std::string& optionvalue)`,
or alternatively `void {handler}(const std::string& option, const std::string&
flag)` if the `type` is `void`. The two parameters `option` and `flag` hold the
canonical and the actually used option names, respectively, and they may differ
if an alternative name (from `alias`) was used. While `option` should be used to
identify an option (e.g. by comparing against `*__name`), `flag` should be
usually used in user messages.
Predicate functions
-------------------
Predicate functions are used to check whether an option value is valid after it
has been parsed by a (standard or custom) handler function. Like a handler
function, a predicate function needs to be a member function of
`options::OptionsHandler` with signature `void {predicate}(const std::string&
option, const std::string& flag, {type} value)`. If the check fails, the
predicate should raise an `OptionException`.
Mode options
------------
An option can be defined to hold one of a given set of values we call modes.
Doing so automatically defines an `enum class` for the set of modes and makes
the option accept one of the values from the enum. The enum class will be called
`{type}` and methods `operator<<` and `stringTo{enum}` are automatically
generated. A mode is defined by specifying `[[option.mode.{NAME}]]` after the
main `[[option]]` section with the following attributes:
* `name` (string): the string value that corresponds to the enum value
* `help` (string): documentation about this mode
Example:
[[option]]
name = "bitblastMode"
category = "regular"
long = "bitblast=MODE"
type = "BitblastMode"
default = "LAZY"
help = "choose bitblasting mode, see --bitblast=help"
help_mode = "Bit-blasting modes."
[[option.mode.LAZY]]
name = "lazy"
help = "Separate boolean structure and term reasoning between the core SAT solver and the bit-vector SAT solver."
[[option.mode.EAGER]]
name = "eager"
help = "Bitblast eagerly to bit-vector SAT solver."
The option can now be set with `--bitblast=lazy`, `(set-option :bitblast
eager)`, or `options::set("bitblast", "eager")`.
Generated code
==============
The entire options setup heavily relies on generating a lot of code from the
information retrieved from the `*_options.toml` files. After code generation,
files related to options live either in `src/options/` (if not changed) or in
`build/src/options/` (if automatically generated). After all code has been
generated, the entire options setup consists of the following components:
* `options.h`: core `Options` class
* `options_api.h`: utility methods used by the API (`parse()`, `set()`, `get()`,
...)
* `options_public.h`: utility methods used to access options from outside of
libcvc5
* `{module}_options.h`: specifics for one single options module
`Options` class
---------------
The `Options` class is the central entry point for regular usage of options. It
holds a `std::unique_ptr` to an "option holder" for every option module, that
can be accessed using references `{module}` (either as `const&` or `&`). These
holders hold the actual option data for the specific module.
The holder types are forward declared and can thus only be accessed if one also
includes the appropriate `{module}_options.h`, which contains the proper
declaration for the holder class.
Option modules
--------------
Every option module declares an "option holder" class, which is a simple struct
that has two members for every option (that is not declared as `type = void`):
the actual option value as `{option.type} {option.name}` and a Boolean flag
`bool {option.name}__setByUser` that indicates whether the option value was
explicitly set by the user. If any of the options of a module is a mode option,
the option module also defines an enum class that corresponds to the mode,
including `operator<<()` and `stringTo{mode type}`.
For convenience, the option modules also provide methods `void
{module.id}::setDefault{option.name}(Options& opts, {option.type} value)`. Each
such method sets the option value to the given value, if the option was not yet
set by the user, i.e., the `__setByUser` flag is false. Additionally, every
option module exports the `long` option name as `static constexpr const char*
{module.id}::{option.name}__name`.
Full Example
============
[[option]]
category = "regular"
name = "decisionMode"
long = "decision=MODE"
alias = ["decision-mode"]
type = "DecisionMode"
default = "INTERNAL"
predicates = ["setDecisionModeStopOnly"]
help = "choose decision mode, see --decision=help"
help_mode = "Decision modes."
[[option.mode.INTERNAL]]
name = "internal"
help = "Use the internal decision heuristics of the SAT solver."
[[option.mode.JUSTIFICATION]]
name = "justification"
help = "An ATGP-inspired justification heuristic."
[[option.mode.STOPONLY]]
name = "justification-stoponly"
help = "Use the justification heuristic only to stop early, not for decisions."
This defines a new option that is accessible via
`d_options.{module.id}.decisionMode` and stores an automatically generated mode
`DecisionMode`, an enum class with the values `INTERNAL`, `JUSTIFICATION` and
`STOPONLY`. From the outside, it can be set by `--decision=internal`, but also
with `--decision-mode=justification`, and similarly from an SMT-LIB input with
`(set-option :decision internal)` and `(set-option :decision-mode
justification)`. The command-line help for this option looks as follows:
--output-lang=LANG | --output-language=LANG
force output language (default is "auto"; see
--output-lang help)
|
