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__STRINGS_H |
22 |
|
#define CVC5__OPTIONS__STRINGS_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 RegExpInterMode |
36 |
|
{ |
37 |
|
ONE_CONSTANT, |
38 |
|
ALL, |
39 |
|
NONE, |
40 |
|
CONSTANT |
41 |
|
}; |
42 |
|
std::ostream& operator<<(std::ostream& os, RegExpInterMode mode); |
43 |
|
RegExpInterMode stringToRegExpInterMode(const std::string& optarg); |
44 |
|
enum class ProcessLoopMode |
45 |
|
{ |
46 |
|
NONE, |
47 |
|
ABORT, |
48 |
|
SIMPLE_ABORT, |
49 |
|
FULL, |
50 |
|
SIMPLE |
51 |
|
}; |
52 |
|
std::ostream& operator<<(std::ostream& os, ProcessLoopMode mode); |
53 |
|
ProcessLoopMode stringToProcessLoopMode(const std::string& optarg); |
54 |
|
// clang-format on |
55 |
|
|
56 |
|
#if defined(CVC5_MUZZLED) || defined(CVC5_COMPETITION_MODE) |
57 |
|
# define DO_SEMANTIC_CHECKS_BY_DEFAULT false |
58 |
|
#else /* CVC5_MUZZLED || CVC5_COMPETITION_MODE */ |
59 |
|
# define DO_SEMANTIC_CHECKS_BY_DEFAULT true |
60 |
|
#endif /* CVC5_MUZZLED || CVC5_COMPETITION_MODE */ |
61 |
|
|
62 |
25268 |
struct HolderSTRINGS |
63 |
|
{ |
64 |
|
// clang-format off |
65 |
|
bool regExpElim = false;\ |
66 |
|
bool regExpElim__setByUser__ = false; |
67 |
|
bool regExpElimAgg = false;\ |
68 |
|
bool regExpElimAgg__setByUser__ = false; |
69 |
|
RegExpInterMode stringRegExpInterMode = RegExpInterMode::CONSTANT;\ |
70 |
|
bool stringRegExpInterMode__setByUser__ = false; |
71 |
|
bool stringCheckEntailLen = true;\ |
72 |
|
bool stringCheckEntailLen__setByUser__ = false; |
73 |
|
bool stringEager = false;\ |
74 |
|
bool stringEager__setByUser__ = false; |
75 |
|
bool stringEagerEval = true;\ |
76 |
|
bool stringEagerEval__setByUser__ = false; |
77 |
|
bool stringEagerLen = true;\ |
78 |
|
bool stringEagerLen__setByUser__ = false; |
79 |
|
bool stringExp = false;\ |
80 |
|
bool stringExp__setByUser__ = false; |
81 |
|
bool stringFlatForms = true;\ |
82 |
|
bool stringFlatForms__setByUser__ = false; |
83 |
|
bool stringFMF = false;\ |
84 |
|
bool stringFMF__setByUser__ = false; |
85 |
|
bool stringGuessModel = false;\ |
86 |
|
bool stringGuessModel__setByUser__ = false; |
87 |
|
bool stringInferAsLemmas = false;\ |
88 |
|
bool stringInferAsLemmas__setByUser__ = false; |
89 |
|
bool stringInferSym = true;\ |
90 |
|
bool stringInferSym__setByUser__ = false; |
91 |
|
bool stringIgnNegMembership = false;\ |
92 |
|
bool stringIgnNegMembership__setByUser__ = false; |
93 |
|
bool stringLazyPreproc = true;\ |
94 |
|
bool stringLazyPreproc__setByUser__ = false; |
95 |
|
bool stringLenNorm = true;\ |
96 |
|
bool stringLenNorm__setByUser__ = false; |
97 |
|
bool stringLenPropCsp = false;\ |
98 |
|
bool stringLenPropCsp__setByUser__ = false; |
99 |
|
bool stringMinPrefixExplain = true;\ |
100 |
|
bool stringMinPrefixExplain__setByUser__ = false; |
101 |
|
ProcessLoopMode stringProcessLoopMode = ProcessLoopMode::FULL;\ |
102 |
|
bool stringProcessLoopMode__setByUser__ = false; |
103 |
|
bool stringRExplainLemmas = true;\ |
104 |
|
bool stringRExplainLemmas__setByUser__ = false; |
105 |
|
bool stringUnifiedVSpt = true;\ |
106 |
|
bool stringUnifiedVSpt__setByUser__ = false; |
107 |
|
// clang-format on |
108 |
|
}; |
109 |
|
|
110 |
|
#undef DO_SEMANTIC_CHECKS_BY_DEFAULT |
111 |
|
|
112 |
|
// clang-format off |
113 |
|
extern struct regExpElim__option_t |
114 |
|
{ |
115 |
|
typedef bool type; |
116 |
|
type operator()() const; |
117 |
|
} thread_local regExpElim; |
118 |
|
extern struct regExpElimAgg__option_t |
119 |
|
{ |
120 |
|
typedef bool type; |
121 |
|
type operator()() const; |
122 |
|
} thread_local regExpElimAgg; |
123 |
|
extern struct stringRegExpInterMode__option_t |
124 |
|
{ |
125 |
|
typedef RegExpInterMode type; |
126 |
|
type operator()() const; |
127 |
|
} thread_local stringRegExpInterMode; |
128 |
|
extern struct stringCheckEntailLen__option_t |
129 |
|
{ |
130 |
|
typedef bool type; |
131 |
|
type operator()() const; |
132 |
|
} thread_local stringCheckEntailLen; |
133 |
|
extern struct stringEager__option_t |
134 |
|
{ |
135 |
|
typedef bool type; |
136 |
|
type operator()() const; |
137 |
|
} thread_local stringEager; |
138 |
|
extern struct stringEagerEval__option_t |
139 |
|
{ |
140 |
|
typedef bool type; |
141 |
|
type operator()() const; |
142 |
|
} thread_local stringEagerEval; |
143 |
|
extern struct stringEagerLen__option_t |
144 |
|
{ |
145 |
|
typedef bool type; |
146 |
|
type operator()() const; |
147 |
|
} thread_local stringEagerLen; |
148 |
|
extern struct stringExp__option_t |
149 |
|
{ |
150 |
|
typedef bool type; |
151 |
|
type operator()() const; |
152 |
|
} thread_local stringExp; |
153 |
|
extern struct stringFlatForms__option_t |
154 |
|
{ |
155 |
|
typedef bool type; |
156 |
|
type operator()() const; |
157 |
|
} thread_local stringFlatForms; |
158 |
|
extern struct stringFMF__option_t |
159 |
|
{ |
160 |
|
typedef bool type; |
161 |
|
type operator()() const; |
162 |
|
} thread_local stringFMF; |
163 |
|
extern struct stringGuessModel__option_t |
164 |
|
{ |
165 |
|
typedef bool type; |
166 |
|
type operator()() const; |
167 |
|
} thread_local stringGuessModel; |
168 |
|
extern struct stringInferAsLemmas__option_t |
169 |
|
{ |
170 |
|
typedef bool type; |
171 |
|
type operator()() const; |
172 |
|
} thread_local stringInferAsLemmas; |
173 |
|
extern struct stringInferSym__option_t |
174 |
|
{ |
175 |
|
typedef bool type; |
176 |
|
type operator()() const; |
177 |
|
} thread_local stringInferSym; |
178 |
|
extern struct stringIgnNegMembership__option_t |
179 |
|
{ |
180 |
|
typedef bool type; |
181 |
|
type operator()() const; |
182 |
|
} thread_local stringIgnNegMembership; |
183 |
|
extern struct stringLazyPreproc__option_t |
184 |
|
{ |
185 |
|
typedef bool type; |
186 |
|
type operator()() const; |
187 |
|
} thread_local stringLazyPreproc; |
188 |
|
extern struct stringLenNorm__option_t |
189 |
|
{ |
190 |
|
typedef bool type; |
191 |
|
type operator()() const; |
192 |
|
} thread_local stringLenNorm; |
193 |
|
extern struct stringLenPropCsp__option_t |
194 |
|
{ |
195 |
|
typedef bool type; |
196 |
|
type operator()() const; |
197 |
|
} thread_local stringLenPropCsp; |
198 |
|
extern struct stringMinPrefixExplain__option_t |
199 |
|
{ |
200 |
|
typedef bool type; |
201 |
|
type operator()() const; |
202 |
|
} thread_local stringMinPrefixExplain; |
203 |
|
extern struct stringProcessLoopMode__option_t |
204 |
|
{ |
205 |
|
typedef ProcessLoopMode type; |
206 |
|
type operator()() const; |
207 |
|
} thread_local stringProcessLoopMode; |
208 |
|
extern struct stringRExplainLemmas__option_t |
209 |
|
{ |
210 |
|
typedef bool type; |
211 |
|
type operator()() const; |
212 |
|
} thread_local stringRExplainLemmas; |
213 |
|
extern struct stringUnifiedVSpt__option_t |
214 |
|
{ |
215 |
|
typedef bool type; |
216 |
|
type operator()() const; |
217 |
|
} thread_local stringUnifiedVSpt; |
218 |
|
// clang-format on |
219 |
|
|
220 |
|
namespace strings |
221 |
|
{ |
222 |
|
// clang-format off |
223 |
|
static constexpr const char* regExpElim__name = "re-elim"; |
224 |
|
static constexpr const char* regExpElimAgg__name = "re-elim-agg"; |
225 |
|
static constexpr const char* stringRegExpInterMode__name = "re-inter-mode"; |
226 |
|
static constexpr const char* stringCheckEntailLen__name = "strings-check-entail-len"; |
227 |
|
static constexpr const char* stringEager__name = "strings-eager"; |
228 |
|
static constexpr const char* stringEagerEval__name = "strings-eager-eval"; |
229 |
|
static constexpr const char* stringEagerLen__name = "strings-eager-len"; |
230 |
|
static constexpr const char* stringExp__name = "strings-exp"; |
231 |
|
static constexpr const char* stringFlatForms__name = "strings-ff"; |
232 |
|
static constexpr const char* stringFMF__name = "strings-fmf"; |
233 |
|
static constexpr const char* stringGuessModel__name = "strings-guess-model"; |
234 |
|
static constexpr const char* stringInferAsLemmas__name = "strings-infer-as-lemmas"; |
235 |
|
static constexpr const char* stringInferSym__name = "strings-infer-sym"; |
236 |
|
static constexpr const char* stringIgnNegMembership__name = "strings-inm"; |
237 |
|
static constexpr const char* stringLazyPreproc__name = "strings-lazy-pp"; |
238 |
|
static constexpr const char* stringLenNorm__name = "strings-len-norm"; |
239 |
|
static constexpr const char* stringLenPropCsp__name = "strings-lprop-csp"; |
240 |
|
static constexpr const char* stringMinPrefixExplain__name = "strings-min-prefix-explain"; |
241 |
|
static constexpr const char* stringProcessLoopMode__name = "strings-process-loop-mode"; |
242 |
|
static constexpr const char* stringRExplainLemmas__name = "strings-rexplain-lemmas"; |
243 |
|
static constexpr const char* stringUnifiedVSpt__name = "strings-unified-vspt"; |
244 |
|
// clang-format on |
245 |
|
} |
246 |
|
|
247 |
|
} // namespace options |
248 |
|
|
249 |
|
// clang-format off |
250 |
|
template <> options::regExpElim__option_t::type& Options::ref( |
251 |
|
options::regExpElim__option_t); |
252 |
|
template <> const options::regExpElim__option_t::type& Options::operator[]( |
253 |
|
options::regExpElim__option_t) const; |
254 |
|
template <> bool Options::wasSetByUser(options::regExpElim__option_t) const; |
255 |
|
template <> options::regExpElimAgg__option_t::type& Options::ref( |
256 |
|
options::regExpElimAgg__option_t); |
257 |
|
template <> const options::regExpElimAgg__option_t::type& Options::operator[]( |
258 |
|
options::regExpElimAgg__option_t) const; |
259 |
|
template <> bool Options::wasSetByUser(options::regExpElimAgg__option_t) const; |
260 |
|
template <> options::stringRegExpInterMode__option_t::type& Options::ref( |
261 |
|
options::stringRegExpInterMode__option_t); |
262 |
|
template <> const options::stringRegExpInterMode__option_t::type& Options::operator[]( |
263 |
|
options::stringRegExpInterMode__option_t) const; |
264 |
|
template <> bool Options::wasSetByUser(options::stringRegExpInterMode__option_t) const; |
265 |
|
template <> options::stringCheckEntailLen__option_t::type& Options::ref( |
266 |
|
options::stringCheckEntailLen__option_t); |
267 |
|
template <> const options::stringCheckEntailLen__option_t::type& Options::operator[]( |
268 |
|
options::stringCheckEntailLen__option_t) const; |
269 |
|
template <> bool Options::wasSetByUser(options::stringCheckEntailLen__option_t) const; |
270 |
|
template <> options::stringEager__option_t::type& Options::ref( |
271 |
|
options::stringEager__option_t); |
272 |
|
template <> const options::stringEager__option_t::type& Options::operator[]( |
273 |
|
options::stringEager__option_t) const; |
274 |
|
template <> bool Options::wasSetByUser(options::stringEager__option_t) const; |
275 |
|
template <> options::stringEagerEval__option_t::type& Options::ref( |
276 |
|
options::stringEagerEval__option_t); |
277 |
|
template <> const options::stringEagerEval__option_t::type& Options::operator[]( |
278 |
|
options::stringEagerEval__option_t) const; |
279 |
|
template <> bool Options::wasSetByUser(options::stringEagerEval__option_t) const; |
280 |
|
template <> options::stringEagerLen__option_t::type& Options::ref( |
281 |
|
options::stringEagerLen__option_t); |
282 |
|
template <> const options::stringEagerLen__option_t::type& Options::operator[]( |
283 |
|
options::stringEagerLen__option_t) const; |
284 |
|
template <> bool Options::wasSetByUser(options::stringEagerLen__option_t) const; |
285 |
|
template <> options::stringExp__option_t::type& Options::ref( |
286 |
|
options::stringExp__option_t); |
287 |
|
template <> const options::stringExp__option_t::type& Options::operator[]( |
288 |
|
options::stringExp__option_t) const; |
289 |
|
template <> bool Options::wasSetByUser(options::stringExp__option_t) const; |
290 |
|
template <> options::stringFlatForms__option_t::type& Options::ref( |
291 |
|
options::stringFlatForms__option_t); |
292 |
|
template <> const options::stringFlatForms__option_t::type& Options::operator[]( |
293 |
|
options::stringFlatForms__option_t) const; |
294 |
|
template <> bool Options::wasSetByUser(options::stringFlatForms__option_t) const; |
295 |
|
template <> options::stringFMF__option_t::type& Options::ref( |
296 |
|
options::stringFMF__option_t); |
297 |
|
template <> const options::stringFMF__option_t::type& Options::operator[]( |
298 |
|
options::stringFMF__option_t) const; |
299 |
|
template <> bool Options::wasSetByUser(options::stringFMF__option_t) const; |
300 |
|
template <> options::stringGuessModel__option_t::type& Options::ref( |
301 |
|
options::stringGuessModel__option_t); |
302 |
|
template <> const options::stringGuessModel__option_t::type& Options::operator[]( |
303 |
|
options::stringGuessModel__option_t) const; |
304 |
|
template <> bool Options::wasSetByUser(options::stringGuessModel__option_t) const; |
305 |
|
template <> options::stringInferAsLemmas__option_t::type& Options::ref( |
306 |
|
options::stringInferAsLemmas__option_t); |
307 |
|
template <> const options::stringInferAsLemmas__option_t::type& Options::operator[]( |
308 |
|
options::stringInferAsLemmas__option_t) const; |
309 |
|
template <> bool Options::wasSetByUser(options::stringInferAsLemmas__option_t) const; |
310 |
|
template <> options::stringInferSym__option_t::type& Options::ref( |
311 |
|
options::stringInferSym__option_t); |
312 |
|
template <> const options::stringInferSym__option_t::type& Options::operator[]( |
313 |
|
options::stringInferSym__option_t) const; |
314 |
|
template <> bool Options::wasSetByUser(options::stringInferSym__option_t) const; |
315 |
|
template <> options::stringIgnNegMembership__option_t::type& Options::ref( |
316 |
|
options::stringIgnNegMembership__option_t); |
317 |
|
template <> const options::stringIgnNegMembership__option_t::type& Options::operator[]( |
318 |
|
options::stringIgnNegMembership__option_t) const; |
319 |
|
template <> bool Options::wasSetByUser(options::stringIgnNegMembership__option_t) const; |
320 |
|
template <> options::stringLazyPreproc__option_t::type& Options::ref( |
321 |
|
options::stringLazyPreproc__option_t); |
322 |
|
template <> const options::stringLazyPreproc__option_t::type& Options::operator[]( |
323 |
|
options::stringLazyPreproc__option_t) const; |
324 |
|
template <> bool Options::wasSetByUser(options::stringLazyPreproc__option_t) const; |
325 |
|
template <> options::stringLenNorm__option_t::type& Options::ref( |
326 |
|
options::stringLenNorm__option_t); |
327 |
|
template <> const options::stringLenNorm__option_t::type& Options::operator[]( |
328 |
|
options::stringLenNorm__option_t) const; |
329 |
|
template <> bool Options::wasSetByUser(options::stringLenNorm__option_t) const; |
330 |
|
template <> options::stringLenPropCsp__option_t::type& Options::ref( |
331 |
|
options::stringLenPropCsp__option_t); |
332 |
|
template <> const options::stringLenPropCsp__option_t::type& Options::operator[]( |
333 |
|
options::stringLenPropCsp__option_t) const; |
334 |
|
template <> bool Options::wasSetByUser(options::stringLenPropCsp__option_t) const; |
335 |
|
template <> options::stringMinPrefixExplain__option_t::type& Options::ref( |
336 |
|
options::stringMinPrefixExplain__option_t); |
337 |
|
template <> const options::stringMinPrefixExplain__option_t::type& Options::operator[]( |
338 |
|
options::stringMinPrefixExplain__option_t) const; |
339 |
|
template <> bool Options::wasSetByUser(options::stringMinPrefixExplain__option_t) const; |
340 |
|
template <> options::stringProcessLoopMode__option_t::type& Options::ref( |
341 |
|
options::stringProcessLoopMode__option_t); |
342 |
|
template <> const options::stringProcessLoopMode__option_t::type& Options::operator[]( |
343 |
|
options::stringProcessLoopMode__option_t) const; |
344 |
|
template <> bool Options::wasSetByUser(options::stringProcessLoopMode__option_t) const; |
345 |
|
template <> options::stringRExplainLemmas__option_t::type& Options::ref( |
346 |
|
options::stringRExplainLemmas__option_t); |
347 |
|
template <> const options::stringRExplainLemmas__option_t::type& Options::operator[]( |
348 |
|
options::stringRExplainLemmas__option_t) const; |
349 |
|
template <> bool Options::wasSetByUser(options::stringRExplainLemmas__option_t) const; |
350 |
|
template <> options::stringUnifiedVSpt__option_t::type& Options::ref( |
351 |
|
options::stringUnifiedVSpt__option_t); |
352 |
|
template <> const options::stringUnifiedVSpt__option_t::type& Options::operator[]( |
353 |
|
options::stringUnifiedVSpt__option_t) const; |
354 |
|
template <> bool Options::wasSetByUser(options::stringUnifiedVSpt__option_t) const; |
355 |
|
// clang-format on |
356 |
|
|
357 |
|
namespace options { |
358 |
|
// clang-format off |
359 |
89968 |
inline regExpElim__option_t::type regExpElim__option_t::operator()() const |
360 |
|
{ |
361 |
89968 |
return Options::current()[*this]; |
362 |
|
} |
363 |
9460 |
inline regExpElimAgg__option_t::type regExpElimAgg__option_t::operator()() const |
364 |
|
{ |
365 |
9460 |
return Options::current()[*this]; |
366 |
|
} |
367 |
1342 |
inline stringRegExpInterMode__option_t::type stringRegExpInterMode__option_t::operator()() const |
368 |
|
{ |
369 |
1342 |
return Options::current()[*this]; |
370 |
|
} |
371 |
2632 |
inline stringCheckEntailLen__option_t::type stringCheckEntailLen__option_t::operator()() const |
372 |
|
{ |
373 |
2632 |
return Options::current()[*this]; |
374 |
|
} |
375 |
18094 |
inline stringEager__option_t::type stringEager__option_t::operator()() const |
376 |
|
{ |
377 |
18094 |
return Options::current()[*this]; |
378 |
|
} |
379 |
9460 |
inline stringEagerEval__option_t::type stringEagerEval__option_t::operator()() const |
380 |
|
{ |
381 |
9460 |
return Options::current()[*this]; |
382 |
|
} |
383 |
46820 |
inline stringEagerLen__option_t::type stringEagerLen__option_t::operator()() const |
384 |
|
{ |
385 |
46820 |
return Options::current()[*this]; |
386 |
|
} |
387 |
132194 |
inline stringExp__option_t::type stringExp__option_t::operator()() const |
388 |
|
{ |
389 |
132194 |
return Options::current()[*this]; |
390 |
|
} |
391 |
9047 |
inline stringFlatForms__option_t::type stringFlatForms__option_t::operator()() const |
392 |
|
{ |
393 |
9047 |
return Options::current()[*this]; |
394 |
|
} |
395 |
101383 |
inline stringFMF__option_t::type stringFMF__option_t::operator()() const |
396 |
|
{ |
397 |
101383 |
return Options::current()[*this]; |
398 |
|
} |
399 |
8052 |
inline stringGuessModel__option_t::type stringGuessModel__option_t::operator()() const |
400 |
|
{ |
401 |
8052 |
return Options::current()[*this]; |
402 |
|
} |
403 |
15167 |
inline stringInferAsLemmas__option_t::type stringInferAsLemmas__option_t::operator()() const |
404 |
|
{ |
405 |
15167 |
return Options::current()[*this]; |
406 |
|
} |
407 |
81076 |
inline stringInferSym__option_t::type stringInferSym__option_t::operator()() const |
408 |
|
{ |
409 |
81076 |
return Options::current()[*this]; |
410 |
|
} |
411 |
364 |
inline stringIgnNegMembership__option_t::type stringIgnNegMembership__option_t::operator()() const |
412 |
|
{ |
413 |
364 |
return Options::current()[*this]; |
414 |
|
} |
415 |
21316 |
inline stringLazyPreproc__option_t::type stringLazyPreproc__option_t::operator()() const |
416 |
|
{ |
417 |
21316 |
return Options::current()[*this]; |
418 |
|
} |
419 |
9047 |
inline stringLenNorm__option_t::type stringLenNorm__option_t::operator()() const |
420 |
|
{ |
421 |
9047 |
return Options::current()[*this]; |
422 |
|
} |
423 |
|
inline stringLenPropCsp__option_t::type stringLenPropCsp__option_t::operator()() const |
424 |
|
{ |
425 |
|
return Options::current()[*this]; |
426 |
|
} |
427 |
19272 |
inline stringMinPrefixExplain__option_t::type stringMinPrefixExplain__option_t::operator()() const |
428 |
|
{ |
429 |
19272 |
return Options::current()[*this]; |
430 |
|
} |
431 |
1584 |
inline stringProcessLoopMode__option_t::type stringProcessLoopMode__option_t::operator()() const |
432 |
|
{ |
433 |
1584 |
return Options::current()[*this]; |
434 |
|
} |
435 |
15109 |
inline stringRExplainLemmas__option_t::type stringRExplainLemmas__option_t::operator()() const |
436 |
|
{ |
437 |
15109 |
return Options::current()[*this]; |
438 |
|
} |
439 |
5304 |
inline stringUnifiedVSpt__option_t::type stringUnifiedVSpt__option_t::operator()() const |
440 |
|
{ |
441 |
5304 |
return Options::current()[*this]; |
442 |
|
} |
443 |
|
// clang-format on |
444 |
|
|
445 |
|
} // namespace options |
446 |
|
} // namespace cvc5 |
447 |
|
|
448 |
|
#endif /* CVC5__OPTIONS__STRINGS_H */ |