1 |
|
/****************************************************************************** |
2 |
|
* Top contributors (to current version): |
3 |
|
* Mathias Preiner, Aina Niemetz |
4 |
|
* |
5 |
|
* This file is part of the cvc5 project. |
6 |
|
* |
7 |
|
* Copyright (c) 2009-2021 by the authors listed in the file AUTHORS |
8 |
|
* in the top-level source directory and their institutional affiliations. |
9 |
|
* All rights reserved. See the file COPYING in the top-level source |
10 |
|
* directory for licensing information. |
11 |
|
* **************************************************************************** |
12 |
|
* |
13 |
|
* Contains code for handling command-line options. |
14 |
|
* |
15 |
|
* For each <module>_options.toml configuration file, mkoptions.py |
16 |
|
* expands this template and generates a <module>_options.h file. |
17 |
|
*/ |
18 |
|
|
19 |
|
#include "cvc5_private.h" |
20 |
|
|
21 |
|
#ifndef CVC5__OPTIONS__DATATYPES_H |
22 |
|
#define CVC5__OPTIONS__DATATYPES_H |
23 |
|
|
24 |
|
#include "options/options.h" |
25 |
|
|
26 |
|
// clang-format off |
27 |
|
|
28 |
|
// clang-format on |
29 |
|
|
30 |
|
namespace cvc5 { |
31 |
|
namespace options { |
32 |
|
|
33 |
|
// clang-format off |
34 |
|
|
35 |
|
enum class SygusFairMode |
36 |
|
{ |
37 |
|
NONE, |
38 |
|
DT_HEIGHT_PRED, |
39 |
|
DT_SIZE, |
40 |
|
DT_SIZE_PRED, |
41 |
|
DIRECT |
42 |
|
}; |
43 |
|
std::ostream& operator<<(std::ostream& os, SygusFairMode mode); |
44 |
|
SygusFairMode stringToSygusFairMode(const std::string& optarg); |
45 |
|
// clang-format on |
46 |
|
|
47 |
|
#if defined(CVC5_MUZZLED) || defined(CVC5_COMPETITION_MODE) |
48 |
|
# define DO_SEMANTIC_CHECKS_BY_DEFAULT false |
49 |
|
#else /* CVC5_MUZZLED || CVC5_COMPETITION_MODE */ |
50 |
|
# define DO_SEMANTIC_CHECKS_BY_DEFAULT true |
51 |
|
#endif /* CVC5_MUZZLED || CVC5_COMPETITION_MODE */ |
52 |
|
|
53 |
25268 |
struct HolderDATATYPES |
54 |
|
{ |
55 |
|
// clang-format off |
56 |
|
bool cdtBisimilar = true;\ |
57 |
|
bool cdtBisimilar__setByUser__ = false; |
58 |
|
bool dtBinarySplit = false;\ |
59 |
|
bool dtBinarySplit__setByUser__ = false; |
60 |
|
bool dtBlastSplits = false;\ |
61 |
|
bool dtBlastSplits__setByUser__ = false; |
62 |
|
bool dtCyclic = true;\ |
63 |
|
bool dtCyclic__setByUser__ = false; |
64 |
|
bool dtForceAssignment = false;\ |
65 |
|
bool dtForceAssignment__setByUser__ = false; |
66 |
|
bool dtInferAsLemmas = false;\ |
67 |
|
bool dtInferAsLemmas__setByUser__ = false; |
68 |
|
bool dtNestedRec = false;\ |
69 |
|
bool dtNestedRec__setByUser__ = false; |
70 |
|
bool dtPoliteOptimize = true;\ |
71 |
|
bool dtPoliteOptimize__setByUser__ = false; |
72 |
|
bool dtRewriteErrorSel = false;\ |
73 |
|
bool dtRewriteErrorSel__setByUser__ = false; |
74 |
|
bool dtSharedSelectors = true;\ |
75 |
|
bool dtSharedSelectors__setByUser__ = false; |
76 |
|
int sygusAbortSize = -1;\ |
77 |
|
bool sygusAbortSize__setByUser__ = false; |
78 |
|
bool sygusFairMax = true;\ |
79 |
|
bool sygusFairMax__setByUser__ = false; |
80 |
|
SygusFairMode sygusFair = SygusFairMode::DT_SIZE;\ |
81 |
|
bool sygusFair__setByUser__ = false; |
82 |
|
bool sygusSymBreak = true;\ |
83 |
|
bool sygusSymBreak__setByUser__ = false; |
84 |
|
bool sygusSymBreakAgg = true;\ |
85 |
|
bool sygusSymBreakAgg__setByUser__ = false; |
86 |
|
bool sygusSymBreakDynamic = true;\ |
87 |
|
bool sygusSymBreakDynamic__setByUser__ = false; |
88 |
|
bool sygusSymBreakLazy = true;\ |
89 |
|
bool sygusSymBreakLazy__setByUser__ = false; |
90 |
|
bool sygusSymBreakPbe = true;\ |
91 |
|
bool sygusSymBreakPbe__setByUser__ = false; |
92 |
|
bool sygusSymBreakRlv = true;\ |
93 |
|
bool sygusSymBreakRlv__setByUser__ = false; |
94 |
|
// clang-format on |
95 |
|
}; |
96 |
|
|
97 |
|
#undef DO_SEMANTIC_CHECKS_BY_DEFAULT |
98 |
|
|
99 |
|
// clang-format off |
100 |
|
extern struct cdtBisimilar__option_t |
101 |
|
{ |
102 |
|
typedef bool type; |
103 |
|
type operator()() const; |
104 |
|
} thread_local cdtBisimilar; |
105 |
|
extern struct dtBinarySplit__option_t |
106 |
|
{ |
107 |
|
typedef bool type; |
108 |
|
type operator()() const; |
109 |
|
} thread_local dtBinarySplit; |
110 |
|
extern struct dtBlastSplits__option_t |
111 |
|
{ |
112 |
|
typedef bool type; |
113 |
|
type operator()() const; |
114 |
|
} thread_local dtBlastSplits; |
115 |
|
extern struct dtCyclic__option_t |
116 |
|
{ |
117 |
|
typedef bool type; |
118 |
|
type operator()() const; |
119 |
|
} thread_local dtCyclic; |
120 |
|
extern struct dtForceAssignment__option_t |
121 |
|
{ |
122 |
|
typedef bool type; |
123 |
|
type operator()() const; |
124 |
|
} thread_local dtForceAssignment; |
125 |
|
extern struct dtInferAsLemmas__option_t |
126 |
|
{ |
127 |
|
typedef bool type; |
128 |
|
type operator()() const; |
129 |
|
} thread_local dtInferAsLemmas; |
130 |
|
extern struct dtNestedRec__option_t |
131 |
|
{ |
132 |
|
typedef bool type; |
133 |
|
type operator()() const; |
134 |
|
} thread_local dtNestedRec; |
135 |
|
extern struct dtPoliteOptimize__option_t |
136 |
|
{ |
137 |
|
typedef bool type; |
138 |
|
type operator()() const; |
139 |
|
} thread_local dtPoliteOptimize; |
140 |
|
extern struct dtRewriteErrorSel__option_t |
141 |
|
{ |
142 |
|
typedef bool type; |
143 |
|
type operator()() const; |
144 |
|
} thread_local dtRewriteErrorSel; |
145 |
|
extern struct dtSharedSelectors__option_t |
146 |
|
{ |
147 |
|
typedef bool type; |
148 |
|
type operator()() const; |
149 |
|
} thread_local dtSharedSelectors; |
150 |
|
extern struct sygusAbortSize__option_t |
151 |
|
{ |
152 |
|
typedef int type; |
153 |
|
type operator()() const; |
154 |
|
} thread_local sygusAbortSize; |
155 |
|
extern struct sygusFairMax__option_t |
156 |
|
{ |
157 |
|
typedef bool type; |
158 |
|
type operator()() const; |
159 |
|
} thread_local sygusFairMax; |
160 |
|
extern struct sygusFair__option_t |
161 |
|
{ |
162 |
|
typedef SygusFairMode type; |
163 |
|
type operator()() const; |
164 |
|
} thread_local sygusFair; |
165 |
|
extern struct sygusSymBreak__option_t |
166 |
|
{ |
167 |
|
typedef bool type; |
168 |
|
type operator()() const; |
169 |
|
} thread_local sygusSymBreak; |
170 |
|
extern struct sygusSymBreakAgg__option_t |
171 |
|
{ |
172 |
|
typedef bool type; |
173 |
|
type operator()() const; |
174 |
|
} thread_local sygusSymBreakAgg; |
175 |
|
extern struct sygusSymBreakDynamic__option_t |
176 |
|
{ |
177 |
|
typedef bool type; |
178 |
|
type operator()() const; |
179 |
|
} thread_local sygusSymBreakDynamic; |
180 |
|
extern struct sygusSymBreakLazy__option_t |
181 |
|
{ |
182 |
|
typedef bool type; |
183 |
|
type operator()() const; |
184 |
|
} thread_local sygusSymBreakLazy; |
185 |
|
extern struct sygusSymBreakPbe__option_t |
186 |
|
{ |
187 |
|
typedef bool type; |
188 |
|
type operator()() const; |
189 |
|
} thread_local sygusSymBreakPbe; |
190 |
|
extern struct sygusSymBreakRlv__option_t |
191 |
|
{ |
192 |
|
typedef bool type; |
193 |
|
type operator()() const; |
194 |
|
} thread_local sygusSymBreakRlv; |
195 |
|
// clang-format on |
196 |
|
|
197 |
|
namespace datatypes |
198 |
|
{ |
199 |
|
// clang-format off |
200 |
|
static constexpr const char* cdtBisimilar__name = "cdt-bisimilar"; |
201 |
|
static constexpr const char* dtBinarySplit__name = "dt-binary-split"; |
202 |
|
static constexpr const char* dtBlastSplits__name = "dt-blast-splits"; |
203 |
|
static constexpr const char* dtCyclic__name = "dt-cyclic"; |
204 |
|
static constexpr const char* dtForceAssignment__name = "dt-force-assignment"; |
205 |
|
static constexpr const char* dtInferAsLemmas__name = "dt-infer-as-lemmas"; |
206 |
|
static constexpr const char* dtNestedRec__name = "dt-nested-rec"; |
207 |
|
static constexpr const char* dtPoliteOptimize__name = "dt-polite-optimize"; |
208 |
|
static constexpr const char* dtRewriteErrorSel__name = "dt-rewrite-error-sel"; |
209 |
|
static constexpr const char* dtSharedSelectors__name = "dt-share-sel"; |
210 |
|
static constexpr const char* sygusAbortSize__name = "sygus-abort-size"; |
211 |
|
static constexpr const char* sygusFairMax__name = "sygus-fair-max"; |
212 |
|
static constexpr const char* sygusFair__name = "sygus-fair"; |
213 |
|
static constexpr const char* sygusSymBreak__name = "sygus-sym-break"; |
214 |
|
static constexpr const char* sygusSymBreakAgg__name = "sygus-sym-break-agg"; |
215 |
|
static constexpr const char* sygusSymBreakDynamic__name = "sygus-sym-break-dynamic"; |
216 |
|
static constexpr const char* sygusSymBreakLazy__name = "sygus-sym-break-lazy"; |
217 |
|
static constexpr const char* sygusSymBreakPbe__name = "sygus-sym-break-pbe"; |
218 |
|
static constexpr const char* sygusSymBreakRlv__name = "sygus-sym-break-rlv"; |
219 |
|
// clang-format on |
220 |
|
} |
221 |
|
|
222 |
|
} // namespace options |
223 |
|
|
224 |
|
// clang-format off |
225 |
|
template <> options::cdtBisimilar__option_t::type& Options::ref( |
226 |
|
options::cdtBisimilar__option_t); |
227 |
|
template <> const options::cdtBisimilar__option_t::type& Options::operator[]( |
228 |
|
options::cdtBisimilar__option_t) const; |
229 |
|
template <> bool Options::wasSetByUser(options::cdtBisimilar__option_t) const; |
230 |
|
template <> options::dtBinarySplit__option_t::type& Options::ref( |
231 |
|
options::dtBinarySplit__option_t); |
232 |
|
template <> const options::dtBinarySplit__option_t::type& Options::operator[]( |
233 |
|
options::dtBinarySplit__option_t) const; |
234 |
|
template <> bool Options::wasSetByUser(options::dtBinarySplit__option_t) const; |
235 |
|
template <> options::dtBlastSplits__option_t::type& Options::ref( |
236 |
|
options::dtBlastSplits__option_t); |
237 |
|
template <> const options::dtBlastSplits__option_t::type& Options::operator[]( |
238 |
|
options::dtBlastSplits__option_t) const; |
239 |
|
template <> bool Options::wasSetByUser(options::dtBlastSplits__option_t) const; |
240 |
|
template <> options::dtCyclic__option_t::type& Options::ref( |
241 |
|
options::dtCyclic__option_t); |
242 |
|
template <> const options::dtCyclic__option_t::type& Options::operator[]( |
243 |
|
options::dtCyclic__option_t) const; |
244 |
|
template <> bool Options::wasSetByUser(options::dtCyclic__option_t) const; |
245 |
|
template <> options::dtForceAssignment__option_t::type& Options::ref( |
246 |
|
options::dtForceAssignment__option_t); |
247 |
|
template <> const options::dtForceAssignment__option_t::type& Options::operator[]( |
248 |
|
options::dtForceAssignment__option_t) const; |
249 |
|
template <> bool Options::wasSetByUser(options::dtForceAssignment__option_t) const; |
250 |
|
template <> options::dtInferAsLemmas__option_t::type& Options::ref( |
251 |
|
options::dtInferAsLemmas__option_t); |
252 |
|
template <> const options::dtInferAsLemmas__option_t::type& Options::operator[]( |
253 |
|
options::dtInferAsLemmas__option_t) const; |
254 |
|
template <> bool Options::wasSetByUser(options::dtInferAsLemmas__option_t) const; |
255 |
|
template <> options::dtNestedRec__option_t::type& Options::ref( |
256 |
|
options::dtNestedRec__option_t); |
257 |
|
template <> const options::dtNestedRec__option_t::type& Options::operator[]( |
258 |
|
options::dtNestedRec__option_t) const; |
259 |
|
template <> bool Options::wasSetByUser(options::dtNestedRec__option_t) const; |
260 |
|
template <> options::dtPoliteOptimize__option_t::type& Options::ref( |
261 |
|
options::dtPoliteOptimize__option_t); |
262 |
|
template <> const options::dtPoliteOptimize__option_t::type& Options::operator[]( |
263 |
|
options::dtPoliteOptimize__option_t) const; |
264 |
|
template <> bool Options::wasSetByUser(options::dtPoliteOptimize__option_t) const; |
265 |
|
template <> options::dtRewriteErrorSel__option_t::type& Options::ref( |
266 |
|
options::dtRewriteErrorSel__option_t); |
267 |
|
template <> const options::dtRewriteErrorSel__option_t::type& Options::operator[]( |
268 |
|
options::dtRewriteErrorSel__option_t) const; |
269 |
|
template <> bool Options::wasSetByUser(options::dtRewriteErrorSel__option_t) const; |
270 |
|
template <> options::dtSharedSelectors__option_t::type& Options::ref( |
271 |
|
options::dtSharedSelectors__option_t); |
272 |
|
template <> const options::dtSharedSelectors__option_t::type& Options::operator[]( |
273 |
|
options::dtSharedSelectors__option_t) const; |
274 |
|
template <> bool Options::wasSetByUser(options::dtSharedSelectors__option_t) const; |
275 |
|
template <> options::sygusAbortSize__option_t::type& Options::ref( |
276 |
|
options::sygusAbortSize__option_t); |
277 |
|
template <> const options::sygusAbortSize__option_t::type& Options::operator[]( |
278 |
|
options::sygusAbortSize__option_t) const; |
279 |
|
template <> bool Options::wasSetByUser(options::sygusAbortSize__option_t) const; |
280 |
|
template <> options::sygusFairMax__option_t::type& Options::ref( |
281 |
|
options::sygusFairMax__option_t); |
282 |
|
template <> const options::sygusFairMax__option_t::type& Options::operator[]( |
283 |
|
options::sygusFairMax__option_t) const; |
284 |
|
template <> bool Options::wasSetByUser(options::sygusFairMax__option_t) const; |
285 |
|
template <> options::sygusFair__option_t::type& Options::ref( |
286 |
|
options::sygusFair__option_t); |
287 |
|
template <> const options::sygusFair__option_t::type& Options::operator[]( |
288 |
|
options::sygusFair__option_t) const; |
289 |
|
template <> bool Options::wasSetByUser(options::sygusFair__option_t) const; |
290 |
|
template <> options::sygusSymBreak__option_t::type& Options::ref( |
291 |
|
options::sygusSymBreak__option_t); |
292 |
|
template <> const options::sygusSymBreak__option_t::type& Options::operator[]( |
293 |
|
options::sygusSymBreak__option_t) const; |
294 |
|
template <> bool Options::wasSetByUser(options::sygusSymBreak__option_t) const; |
295 |
|
template <> options::sygusSymBreakAgg__option_t::type& Options::ref( |
296 |
|
options::sygusSymBreakAgg__option_t); |
297 |
|
template <> const options::sygusSymBreakAgg__option_t::type& Options::operator[]( |
298 |
|
options::sygusSymBreakAgg__option_t) const; |
299 |
|
template <> bool Options::wasSetByUser(options::sygusSymBreakAgg__option_t) const; |
300 |
|
template <> options::sygusSymBreakDynamic__option_t::type& Options::ref( |
301 |
|
options::sygusSymBreakDynamic__option_t); |
302 |
|
template <> const options::sygusSymBreakDynamic__option_t::type& Options::operator[]( |
303 |
|
options::sygusSymBreakDynamic__option_t) const; |
304 |
|
template <> bool Options::wasSetByUser(options::sygusSymBreakDynamic__option_t) const; |
305 |
|
template <> options::sygusSymBreakLazy__option_t::type& Options::ref( |
306 |
|
options::sygusSymBreakLazy__option_t); |
307 |
|
template <> const options::sygusSymBreakLazy__option_t::type& Options::operator[]( |
308 |
|
options::sygusSymBreakLazy__option_t) const; |
309 |
|
template <> bool Options::wasSetByUser(options::sygusSymBreakLazy__option_t) const; |
310 |
|
template <> options::sygusSymBreakPbe__option_t::type& Options::ref( |
311 |
|
options::sygusSymBreakPbe__option_t); |
312 |
|
template <> const options::sygusSymBreakPbe__option_t::type& Options::operator[]( |
313 |
|
options::sygusSymBreakPbe__option_t) const; |
314 |
|
template <> bool Options::wasSetByUser(options::sygusSymBreakPbe__option_t) const; |
315 |
|
template <> options::sygusSymBreakRlv__option_t::type& Options::ref( |
316 |
|
options::sygusSymBreakRlv__option_t); |
317 |
|
template <> const options::sygusSymBreakRlv__option_t::type& Options::operator[]( |
318 |
|
options::sygusSymBreakRlv__option_t) const; |
319 |
|
template <> bool Options::wasSetByUser(options::sygusSymBreakRlv__option_t) const; |
320 |
|
// clang-format on |
321 |
|
|
322 |
|
namespace options { |
323 |
|
// clang-format off |
324 |
86 |
inline cdtBisimilar__option_t::type cdtBisimilar__option_t::operator()() const |
325 |
|
{ |
326 |
86 |
return Options::current()[*this]; |
327 |
|
} |
328 |
1162 |
inline dtBinarySplit__option_t::type dtBinarySplit__option_t::operator()() const |
329 |
|
{ |
330 |
1162 |
return Options::current()[*this]; |
331 |
|
} |
332 |
1162 |
inline dtBlastSplits__option_t::type dtBlastSplits__option_t::operator()() const |
333 |
|
{ |
334 |
1162 |
return Options::current()[*this]; |
335 |
|
} |
336 |
194719 |
inline dtCyclic__option_t::type dtCyclic__option_t::operator()() const |
337 |
|
{ |
338 |
194719 |
return Options::current()[*this]; |
339 |
|
} |
340 |
28124 |
inline dtForceAssignment__option_t::type dtForceAssignment__option_t::operator()() const |
341 |
|
{ |
342 |
28124 |
return Options::current()[*this]; |
343 |
|
} |
344 |
294823 |
inline dtInferAsLemmas__option_t::type dtInferAsLemmas__option_t::operator()() const |
345 |
|
{ |
346 |
294823 |
return Options::current()[*this]; |
347 |
|
} |
348 |
67632 |
inline dtNestedRec__option_t::type dtNestedRec__option_t::operator()() const |
349 |
|
{ |
350 |
67632 |
return Options::current()[*this]; |
351 |
|
} |
352 |
109027 |
inline dtPoliteOptimize__option_t::type dtPoliteOptimize__option_t::operator()() const |
353 |
|
{ |
354 |
109027 |
return Options::current()[*this]; |
355 |
|
} |
356 |
3866 |
inline dtRewriteErrorSel__option_t::type dtRewriteErrorSel__option_t::operator()() const |
357 |
|
{ |
358 |
3866 |
return Options::current()[*this]; |
359 |
|
} |
360 |
680772 |
inline dtSharedSelectors__option_t::type dtSharedSelectors__option_t::operator()() const |
361 |
|
{ |
362 |
680772 |
return Options::current()[*this]; |
363 |
|
} |
364 |
650 |
inline sygusAbortSize__option_t::type sygusAbortSize__option_t::operator()() const |
365 |
|
{ |
366 |
650 |
return Options::current()[*this]; |
367 |
|
} |
368 |
424 |
inline sygusFairMax__option_t::type sygusFairMax__option_t::operator()() const |
369 |
|
{ |
370 |
424 |
return Options::current()[*this]; |
371 |
|
} |
372 |
86795 |
inline sygusFair__option_t::type sygusFair__option_t::operator()() const |
373 |
|
{ |
374 |
86795 |
return Options::current()[*this]; |
375 |
|
} |
376 |
2871 |
inline sygusSymBreak__option_t::type sygusSymBreak__option_t::operator()() const |
377 |
|
{ |
378 |
2871 |
return Options::current()[*this]; |
379 |
|
} |
380 |
177 |
inline sygusSymBreakAgg__option_t::type sygusSymBreakAgg__option_t::operator()() const |
381 |
|
{ |
382 |
177 |
return Options::current()[*this]; |
383 |
|
} |
384 |
63470 |
inline sygusSymBreakDynamic__option_t::type sygusSymBreakDynamic__option_t::operator()() const |
385 |
|
{ |
386 |
63470 |
return Options::current()[*this]; |
387 |
|
} |
388 |
293242 |
inline sygusSymBreakLazy__option_t::type sygusSymBreakLazy__option_t::operator()() const |
389 |
|
{ |
390 |
293242 |
return Options::current()[*this]; |
391 |
|
} |
392 |
4963 |
inline sygusSymBreakPbe__option_t::type sygusSymBreakPbe__option_t::operator()() const |
393 |
|
{ |
394 |
4963 |
return Options::current()[*this]; |
395 |
|
} |
396 |
75332 |
inline sygusSymBreakRlv__option_t::type sygusSymBreakRlv__option_t::operator()() const |
397 |
|
{ |
398 |
75332 |
return Options::current()[*this]; |
399 |
|
} |
400 |
|
// clang-format on |
401 |
|
|
402 |
|
} // namespace options |
403 |
|
} // namespace cvc5 |
404 |
|
|
405 |
|
#endif /* CVC5__OPTIONS__DATATYPES_H */ |