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__BV_H |
22 |
|
#define CVC5__OPTIONS__BV_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 BitblastMode |
36 |
|
{ |
37 |
|
LAZY, |
38 |
|
EAGER |
39 |
|
}; |
40 |
|
std::ostream& operator<<(std::ostream& os, BitblastMode mode); |
41 |
|
BitblastMode stringToBitblastMode(const std::string& optarg); |
42 |
|
enum class BoolToBVMode |
43 |
|
{ |
44 |
|
ALL, |
45 |
|
ITE, |
46 |
|
OFF |
47 |
|
}; |
48 |
|
std::ostream& operator<<(std::ostream& os, BoolToBVMode mode); |
49 |
|
BoolToBVMode stringToBoolToBVMode(const std::string& optarg); |
50 |
|
enum class SatSolverMode |
51 |
|
{ |
52 |
|
KISSAT, |
53 |
|
MINISAT, |
54 |
|
CRYPTOMINISAT, |
55 |
|
CADICAL |
56 |
|
}; |
57 |
|
std::ostream& operator<<(std::ostream& os, SatSolverMode mode); |
58 |
|
SatSolverMode stringToSatSolverMode(const std::string& optarg); |
59 |
|
enum class BVSolver |
60 |
|
{ |
61 |
|
LAZY, |
62 |
|
BITBLAST, |
63 |
|
SIMPLE |
64 |
|
}; |
65 |
|
std::ostream& operator<<(std::ostream& os, BVSolver mode); |
66 |
|
BVSolver stringToBVSolver(const std::string& optarg); |
67 |
|
// clang-format on |
68 |
|
|
69 |
|
#if defined(CVC5_MUZZLED) || defined(CVC5_COMPETITION_MODE) |
70 |
|
# define DO_SEMANTIC_CHECKS_BY_DEFAULT false |
71 |
|
#else /* CVC5_MUZZLED || CVC5_COMPETITION_MODE */ |
72 |
|
# define DO_SEMANTIC_CHECKS_BY_DEFAULT true |
73 |
|
#endif /* CVC5_MUZZLED || CVC5_COMPETITION_MODE */ |
74 |
|
|
75 |
63271 |
struct HolderBV |
76 |
|
{ |
77 |
|
// clang-format off |
78 |
|
bool bitvectorAig = false;\ |
79 |
|
bool bitvectorAig__setByUser__ = false; |
80 |
|
BitblastMode bitblastMode = BitblastMode::LAZY;\ |
81 |
|
bool bitblastMode__setByUser__ = false; |
82 |
|
bool bitwiseEq = true;\ |
83 |
|
bool bitwiseEq__setByUser__ = false; |
84 |
|
BoolToBVMode boolToBitvector = BoolToBVMode::OFF;\ |
85 |
|
bool boolToBitvector__setByUser__ = false; |
86 |
|
bool bvAbstraction = false;\ |
87 |
|
bool bvAbstraction__setByUser__ = false; |
88 |
|
std::string bitvectorAigSimplifications = "balance;drw";\ |
89 |
|
bool bitvectorAigSimplifications__setByUser__ = false; |
90 |
|
bool bvAlgExtf = true;\ |
91 |
|
bool bvAlgExtf__setByUser__ = false; |
92 |
|
unsigned bitvectorAlgebraicBudget = 1500;\ |
93 |
|
bool bitvectorAlgebraicBudget__setByUser__ = false; |
94 |
|
bool bitvectorAlgebraicSolver = false;\ |
95 |
|
bool bitvectorAlgebraicSolver__setByUser__ = false; |
96 |
|
bool bvAssertInput = false;\ |
97 |
|
bool bvAssertInput__setByUser__ = false; |
98 |
|
bool bvEagerExplanations = false;\ |
99 |
|
bool bvEagerExplanations__setByUser__ = false; |
100 |
|
bool bitvectorEqualitySolver = true;\ |
101 |
|
bool bitvectorEqualitySolver__setByUser__ = false; |
102 |
|
bool bvExtractArithRewrite = false;\ |
103 |
|
bool bvExtractArithRewrite__setByUser__ = false; |
104 |
|
bool bvGaussElim = false;\ |
105 |
|
bool bvGaussElim__setByUser__ = false; |
106 |
|
bool bitvectorInequalitySolver = true;\ |
107 |
|
bool bitvectorInequalitySolver__setByUser__ = false; |
108 |
|
bool bvIntroducePow2 = false;\ |
109 |
|
bool bvIntroducePow2__setByUser__ = false; |
110 |
|
bool bvLazyReduceExtf = false;\ |
111 |
|
bool bvLazyReduceExtf__setByUser__ = false; |
112 |
|
bool bvLazyRewriteExtf = true;\ |
113 |
|
bool bvLazyRewriteExtf__setByUser__ = false; |
114 |
|
unsigned bvNumFunc = 1;\ |
115 |
|
bool bvNumFunc__setByUser__ = false; |
116 |
|
bool bvPrintConstsAsIndexedSymbols = false;\ |
117 |
|
bool bvPrintConstsAsIndexedSymbols__setByUser__ = false; |
118 |
|
bool bitvectorPropagate = true;\ |
119 |
|
bool bitvectorPropagate__setByUser__ = false; |
120 |
|
bool bitvectorQuickXplain = false;\ |
121 |
|
bool bitvectorQuickXplain__setByUser__ = false; |
122 |
|
SatSolverMode bvSatSolver = SatSolverMode::MINISAT;\ |
123 |
|
bool bvSatSolver__setByUser__ = false; |
124 |
|
bool skolemizeArguments = false;\ |
125 |
|
bool skolemizeArguments__setByUser__ = false; |
126 |
|
BVSolver bvSolver = BVSolver::LAZY;\ |
127 |
|
bool bvSolver__setByUser__ = false; |
128 |
|
bool bitvectorToBool = false;\ |
129 |
|
bool bitvectorToBool__setByUser__ = false; |
130 |
|
// clang-format on |
131 |
|
}; |
132 |
|
|
133 |
|
#undef DO_SEMANTIC_CHECKS_BY_DEFAULT |
134 |
|
|
135 |
|
// clang-format off |
136 |
|
extern struct bitvectorAig__option_t |
137 |
|
{ |
138 |
|
typedef bool type; |
139 |
|
type operator()() const; |
140 |
|
} thread_local bitvectorAig; |
141 |
|
extern struct bitblastMode__option_t |
142 |
|
{ |
143 |
|
typedef BitblastMode type; |
144 |
|
type operator()() const; |
145 |
|
} thread_local bitblastMode; |
146 |
|
extern struct bitwiseEq__option_t |
147 |
|
{ |
148 |
|
typedef bool type; |
149 |
|
type operator()() const; |
150 |
|
} thread_local bitwiseEq; |
151 |
|
extern struct boolToBitvector__option_t |
152 |
|
{ |
153 |
|
typedef BoolToBVMode type; |
154 |
|
type operator()() const; |
155 |
|
} thread_local boolToBitvector; |
156 |
|
extern struct bvAbstraction__option_t |
157 |
|
{ |
158 |
|
typedef bool type; |
159 |
|
type operator()() const; |
160 |
|
} thread_local bvAbstraction; |
161 |
|
extern struct bitvectorAigSimplifications__option_t |
162 |
|
{ |
163 |
|
typedef std::string type; |
164 |
|
type operator()() const; |
165 |
|
} thread_local bitvectorAigSimplifications; |
166 |
|
extern struct bvAlgExtf__option_t |
167 |
|
{ |
168 |
|
typedef bool type; |
169 |
|
type operator()() const; |
170 |
|
} thread_local bvAlgExtf; |
171 |
|
extern struct bitvectorAlgebraicBudget__option_t |
172 |
|
{ |
173 |
|
typedef unsigned type; |
174 |
|
type operator()() const; |
175 |
|
} thread_local bitvectorAlgebraicBudget; |
176 |
|
extern struct bitvectorAlgebraicSolver__option_t |
177 |
|
{ |
178 |
|
typedef bool type; |
179 |
|
type operator()() const; |
180 |
|
} thread_local bitvectorAlgebraicSolver; |
181 |
|
extern struct bvAssertInput__option_t |
182 |
|
{ |
183 |
|
typedef bool type; |
184 |
|
type operator()() const; |
185 |
|
} thread_local bvAssertInput; |
186 |
|
extern struct bvEagerExplanations__option_t |
187 |
|
{ |
188 |
|
typedef bool type; |
189 |
|
type operator()() const; |
190 |
|
} thread_local bvEagerExplanations; |
191 |
|
extern struct bitvectorEqualitySolver__option_t |
192 |
|
{ |
193 |
|
typedef bool type; |
194 |
|
type operator()() const; |
195 |
|
} thread_local bitvectorEqualitySolver; |
196 |
|
extern struct bvExtractArithRewrite__option_t |
197 |
|
{ |
198 |
|
typedef bool type; |
199 |
|
type operator()() const; |
200 |
|
} thread_local bvExtractArithRewrite; |
201 |
|
extern struct bvGaussElim__option_t |
202 |
|
{ |
203 |
|
typedef bool type; |
204 |
|
type operator()() const; |
205 |
|
} thread_local bvGaussElim; |
206 |
|
extern struct bitvectorInequalitySolver__option_t |
207 |
|
{ |
208 |
|
typedef bool type; |
209 |
|
type operator()() const; |
210 |
|
} thread_local bitvectorInequalitySolver; |
211 |
|
extern struct bvIntroducePow2__option_t |
212 |
|
{ |
213 |
|
typedef bool type; |
214 |
|
type operator()() const; |
215 |
|
} thread_local bvIntroducePow2; |
216 |
|
extern struct bvLazyReduceExtf__option_t |
217 |
|
{ |
218 |
|
typedef bool type; |
219 |
|
type operator()() const; |
220 |
|
} thread_local bvLazyReduceExtf; |
221 |
|
extern struct bvLazyRewriteExtf__option_t |
222 |
|
{ |
223 |
|
typedef bool type; |
224 |
|
type operator()() const; |
225 |
|
} thread_local bvLazyRewriteExtf; |
226 |
|
extern struct bvNumFunc__option_t |
227 |
|
{ |
228 |
|
typedef unsigned type; |
229 |
|
type operator()() const; |
230 |
|
} thread_local bvNumFunc; |
231 |
|
extern struct bvPrintConstsAsIndexedSymbols__option_t |
232 |
|
{ |
233 |
|
typedef bool type; |
234 |
|
type operator()() const; |
235 |
|
} thread_local bvPrintConstsAsIndexedSymbols; |
236 |
|
extern struct bitvectorPropagate__option_t |
237 |
|
{ |
238 |
|
typedef bool type; |
239 |
|
type operator()() const; |
240 |
|
} thread_local bitvectorPropagate; |
241 |
|
extern struct bitvectorQuickXplain__option_t |
242 |
|
{ |
243 |
|
typedef bool type; |
244 |
|
type operator()() const; |
245 |
|
} thread_local bitvectorQuickXplain; |
246 |
|
extern struct bvSatSolver__option_t |
247 |
|
{ |
248 |
|
typedef SatSolverMode type; |
249 |
|
type operator()() const; |
250 |
|
} thread_local bvSatSolver; |
251 |
|
extern struct skolemizeArguments__option_t |
252 |
|
{ |
253 |
|
typedef bool type; |
254 |
|
type operator()() const; |
255 |
|
} thread_local skolemizeArguments; |
256 |
|
extern struct bvSolver__option_t |
257 |
|
{ |
258 |
|
typedef BVSolver type; |
259 |
|
type operator()() const; |
260 |
|
} thread_local bvSolver; |
261 |
|
extern struct bitvectorToBool__option_t |
262 |
|
{ |
263 |
|
typedef bool type; |
264 |
|
type operator()() const; |
265 |
|
} thread_local bitvectorToBool; |
266 |
|
// clang-format on |
267 |
|
|
268 |
|
namespace bv |
269 |
|
{ |
270 |
|
// clang-format off |
271 |
|
static constexpr const char* bitvectorAig__name = "bitblast-aig"; |
272 |
|
static constexpr const char* bitblastMode__name = "bitblast"; |
273 |
|
static constexpr const char* bitwiseEq__name = "bitwise-eq"; |
274 |
|
static constexpr const char* boolToBitvector__name = "bool-to-bv"; |
275 |
|
static constexpr const char* bvAbstraction__name = "bv-abstraction"; |
276 |
|
static constexpr const char* bitvectorAigSimplifications__name = "bv-aig-simp"; |
277 |
|
static constexpr const char* bvAlgExtf__name = "bv-alg-extf"; |
278 |
|
static constexpr const char* bitvectorAlgebraicBudget__name = "bv-algebraic-budget"; |
279 |
|
static constexpr const char* bitvectorAlgebraicSolver__name = "bv-algebraic-solver"; |
280 |
|
static constexpr const char* bvAssertInput__name = "bv-assert-input"; |
281 |
|
static constexpr const char* bvEagerExplanations__name = "bv-eager-explanations"; |
282 |
|
static constexpr const char* bitvectorEqualitySolver__name = "bv-eq-solver"; |
283 |
|
static constexpr const char* bvExtractArithRewrite__name = "bv-extract-arith"; |
284 |
|
static constexpr const char* bvGaussElim__name = "bv-gauss-elim"; |
285 |
|
static constexpr const char* bitvectorInequalitySolver__name = "bv-inequality-solver"; |
286 |
|
static constexpr const char* bvIntroducePow2__name = "bv-intro-pow2"; |
287 |
|
static constexpr const char* bvLazyReduceExtf__name = "bv-lazy-reduce-extf"; |
288 |
|
static constexpr const char* bvLazyRewriteExtf__name = "bv-lazy-rewrite-extf"; |
289 |
|
static constexpr const char* bvNumFunc__name = "bv-num-func"; |
290 |
|
static constexpr const char* bvPrintConstsAsIndexedSymbols__name = "bv-print-consts-as-indexed-symbols"; |
291 |
|
static constexpr const char* bitvectorPropagate__name = "bv-propagate"; |
292 |
|
static constexpr const char* bitvectorQuickXplain__name = "bv-quick-xplain"; |
293 |
|
static constexpr const char* bvSatSolver__name = "bv-sat-solver"; |
294 |
|
static constexpr const char* skolemizeArguments__name = "bv-skolemize"; |
295 |
|
static constexpr const char* bvSolver__name = "bv-solver"; |
296 |
|
static constexpr const char* bitvectorToBool__name = "bv-to-bool"; |
297 |
|
// clang-format on |
298 |
|
} |
299 |
|
|
300 |
|
} // namespace options |
301 |
|
|
302 |
|
// clang-format off |
303 |
|
template <> options::bitvectorAig__option_t::type& Options::ref( |
304 |
|
options::bitvectorAig__option_t); |
305 |
|
template <> const options::bitvectorAig__option_t::type& Options::operator[]( |
306 |
|
options::bitvectorAig__option_t) const; |
307 |
|
template <> bool Options::wasSetByUser(options::bitvectorAig__option_t) const; |
308 |
|
template <> options::bitblastMode__option_t::type& Options::ref( |
309 |
|
options::bitblastMode__option_t); |
310 |
|
template <> const options::bitblastMode__option_t::type& Options::operator[]( |
311 |
|
options::bitblastMode__option_t) const; |
312 |
|
template <> bool Options::wasSetByUser(options::bitblastMode__option_t) const; |
313 |
|
template <> options::bitwiseEq__option_t::type& Options::ref( |
314 |
|
options::bitwiseEq__option_t); |
315 |
|
template <> const options::bitwiseEq__option_t::type& Options::operator[]( |
316 |
|
options::bitwiseEq__option_t) const; |
317 |
|
template <> bool Options::wasSetByUser(options::bitwiseEq__option_t) const; |
318 |
|
template <> options::boolToBitvector__option_t::type& Options::ref( |
319 |
|
options::boolToBitvector__option_t); |
320 |
|
template <> const options::boolToBitvector__option_t::type& Options::operator[]( |
321 |
|
options::boolToBitvector__option_t) const; |
322 |
|
template <> bool Options::wasSetByUser(options::boolToBitvector__option_t) const; |
323 |
|
template <> options::bvAbstraction__option_t::type& Options::ref( |
324 |
|
options::bvAbstraction__option_t); |
325 |
|
template <> const options::bvAbstraction__option_t::type& Options::operator[]( |
326 |
|
options::bvAbstraction__option_t) const; |
327 |
|
template <> bool Options::wasSetByUser(options::bvAbstraction__option_t) const; |
328 |
|
template <> options::bitvectorAigSimplifications__option_t::type& Options::ref( |
329 |
|
options::bitvectorAigSimplifications__option_t); |
330 |
|
template <> const options::bitvectorAigSimplifications__option_t::type& Options::operator[]( |
331 |
|
options::bitvectorAigSimplifications__option_t) const; |
332 |
|
template <> bool Options::wasSetByUser(options::bitvectorAigSimplifications__option_t) const; |
333 |
|
template <> options::bvAlgExtf__option_t::type& Options::ref( |
334 |
|
options::bvAlgExtf__option_t); |
335 |
|
template <> const options::bvAlgExtf__option_t::type& Options::operator[]( |
336 |
|
options::bvAlgExtf__option_t) const; |
337 |
|
template <> bool Options::wasSetByUser(options::bvAlgExtf__option_t) const; |
338 |
|
template <> options::bitvectorAlgebraicBudget__option_t::type& Options::ref( |
339 |
|
options::bitvectorAlgebraicBudget__option_t); |
340 |
|
template <> const options::bitvectorAlgebraicBudget__option_t::type& Options::operator[]( |
341 |
|
options::bitvectorAlgebraicBudget__option_t) const; |
342 |
|
template <> bool Options::wasSetByUser(options::bitvectorAlgebraicBudget__option_t) const; |
343 |
|
template <> options::bitvectorAlgebraicSolver__option_t::type& Options::ref( |
344 |
|
options::bitvectorAlgebraicSolver__option_t); |
345 |
|
template <> const options::bitvectorAlgebraicSolver__option_t::type& Options::operator[]( |
346 |
|
options::bitvectorAlgebraicSolver__option_t) const; |
347 |
|
template <> bool Options::wasSetByUser(options::bitvectorAlgebraicSolver__option_t) const; |
348 |
|
template <> options::bvAssertInput__option_t::type& Options::ref( |
349 |
|
options::bvAssertInput__option_t); |
350 |
|
template <> const options::bvAssertInput__option_t::type& Options::operator[]( |
351 |
|
options::bvAssertInput__option_t) const; |
352 |
|
template <> bool Options::wasSetByUser(options::bvAssertInput__option_t) const; |
353 |
|
template <> options::bvEagerExplanations__option_t::type& Options::ref( |
354 |
|
options::bvEagerExplanations__option_t); |
355 |
|
template <> const options::bvEagerExplanations__option_t::type& Options::operator[]( |
356 |
|
options::bvEagerExplanations__option_t) const; |
357 |
|
template <> bool Options::wasSetByUser(options::bvEagerExplanations__option_t) const; |
358 |
|
template <> options::bitvectorEqualitySolver__option_t::type& Options::ref( |
359 |
|
options::bitvectorEqualitySolver__option_t); |
360 |
|
template <> const options::bitvectorEqualitySolver__option_t::type& Options::operator[]( |
361 |
|
options::bitvectorEqualitySolver__option_t) const; |
362 |
|
template <> bool Options::wasSetByUser(options::bitvectorEqualitySolver__option_t) const; |
363 |
|
template <> options::bvExtractArithRewrite__option_t::type& Options::ref( |
364 |
|
options::bvExtractArithRewrite__option_t); |
365 |
|
template <> const options::bvExtractArithRewrite__option_t::type& Options::operator[]( |
366 |
|
options::bvExtractArithRewrite__option_t) const; |
367 |
|
template <> bool Options::wasSetByUser(options::bvExtractArithRewrite__option_t) const; |
368 |
|
template <> options::bvGaussElim__option_t::type& Options::ref( |
369 |
|
options::bvGaussElim__option_t); |
370 |
|
template <> const options::bvGaussElim__option_t::type& Options::operator[]( |
371 |
|
options::bvGaussElim__option_t) const; |
372 |
|
template <> bool Options::wasSetByUser(options::bvGaussElim__option_t) const; |
373 |
|
template <> options::bitvectorInequalitySolver__option_t::type& Options::ref( |
374 |
|
options::bitvectorInequalitySolver__option_t); |
375 |
|
template <> const options::bitvectorInequalitySolver__option_t::type& Options::operator[]( |
376 |
|
options::bitvectorInequalitySolver__option_t) const; |
377 |
|
template <> bool Options::wasSetByUser(options::bitvectorInequalitySolver__option_t) const; |
378 |
|
template <> options::bvIntroducePow2__option_t::type& Options::ref( |
379 |
|
options::bvIntroducePow2__option_t); |
380 |
|
template <> const options::bvIntroducePow2__option_t::type& Options::operator[]( |
381 |
|
options::bvIntroducePow2__option_t) const; |
382 |
|
template <> bool Options::wasSetByUser(options::bvIntroducePow2__option_t) const; |
383 |
|
template <> options::bvLazyReduceExtf__option_t::type& Options::ref( |
384 |
|
options::bvLazyReduceExtf__option_t); |
385 |
|
template <> const options::bvLazyReduceExtf__option_t::type& Options::operator[]( |
386 |
|
options::bvLazyReduceExtf__option_t) const; |
387 |
|
template <> bool Options::wasSetByUser(options::bvLazyReduceExtf__option_t) const; |
388 |
|
template <> options::bvLazyRewriteExtf__option_t::type& Options::ref( |
389 |
|
options::bvLazyRewriteExtf__option_t); |
390 |
|
template <> const options::bvLazyRewriteExtf__option_t::type& Options::operator[]( |
391 |
|
options::bvLazyRewriteExtf__option_t) const; |
392 |
|
template <> bool Options::wasSetByUser(options::bvLazyRewriteExtf__option_t) const; |
393 |
|
template <> options::bvNumFunc__option_t::type& Options::ref( |
394 |
|
options::bvNumFunc__option_t); |
395 |
|
template <> const options::bvNumFunc__option_t::type& Options::operator[]( |
396 |
|
options::bvNumFunc__option_t) const; |
397 |
|
template <> bool Options::wasSetByUser(options::bvNumFunc__option_t) const; |
398 |
|
template <> options::bvPrintConstsAsIndexedSymbols__option_t::type& Options::ref( |
399 |
|
options::bvPrintConstsAsIndexedSymbols__option_t); |
400 |
|
template <> const options::bvPrintConstsAsIndexedSymbols__option_t::type& Options::operator[]( |
401 |
|
options::bvPrintConstsAsIndexedSymbols__option_t) const; |
402 |
|
template <> bool Options::wasSetByUser(options::bvPrintConstsAsIndexedSymbols__option_t) const; |
403 |
|
template <> options::bitvectorPropagate__option_t::type& Options::ref( |
404 |
|
options::bitvectorPropagate__option_t); |
405 |
|
template <> const options::bitvectorPropagate__option_t::type& Options::operator[]( |
406 |
|
options::bitvectorPropagate__option_t) const; |
407 |
|
template <> bool Options::wasSetByUser(options::bitvectorPropagate__option_t) const; |
408 |
|
template <> options::bitvectorQuickXplain__option_t::type& Options::ref( |
409 |
|
options::bitvectorQuickXplain__option_t); |
410 |
|
template <> const options::bitvectorQuickXplain__option_t::type& Options::operator[]( |
411 |
|
options::bitvectorQuickXplain__option_t) const; |
412 |
|
template <> bool Options::wasSetByUser(options::bitvectorQuickXplain__option_t) const; |
413 |
|
template <> options::bvSatSolver__option_t::type& Options::ref( |
414 |
|
options::bvSatSolver__option_t); |
415 |
|
template <> const options::bvSatSolver__option_t::type& Options::operator[]( |
416 |
|
options::bvSatSolver__option_t) const; |
417 |
|
template <> bool Options::wasSetByUser(options::bvSatSolver__option_t) const; |
418 |
|
template <> options::skolemizeArguments__option_t::type& Options::ref( |
419 |
|
options::skolemizeArguments__option_t); |
420 |
|
template <> const options::skolemizeArguments__option_t::type& Options::operator[]( |
421 |
|
options::skolemizeArguments__option_t) const; |
422 |
|
template <> bool Options::wasSetByUser(options::skolemizeArguments__option_t) const; |
423 |
|
template <> options::bvSolver__option_t::type& Options::ref( |
424 |
|
options::bvSolver__option_t); |
425 |
|
template <> const options::bvSolver__option_t::type& Options::operator[]( |
426 |
|
options::bvSolver__option_t) const; |
427 |
|
template <> bool Options::wasSetByUser(options::bvSolver__option_t) const; |
428 |
|
template <> options::bitvectorToBool__option_t::type& Options::ref( |
429 |
|
options::bitvectorToBool__option_t); |
430 |
|
template <> const options::bitvectorToBool__option_t::type& Options::operator[]( |
431 |
|
options::bitvectorToBool__option_t) const; |
432 |
|
template <> bool Options::wasSetByUser(options::bitvectorToBool__option_t) const; |
433 |
|
// clang-format on |
434 |
|
|
435 |
|
namespace options { |
436 |
|
// clang-format off |
437 |
2453 |
inline bitvectorAig__option_t::type bitvectorAig__option_t::operator()() const |
438 |
|
{ |
439 |
2453 |
return Options::current()[*this]; |
440 |
|
} |
441 |
1659696 |
inline bitblastMode__option_t::type bitblastMode__option_t::operator()() const |
442 |
|
{ |
443 |
1659696 |
return Options::current()[*this]; |
444 |
|
} |
445 |
315684 |
inline bitwiseEq__option_t::type bitwiseEq__option_t::operator()() const |
446 |
|
{ |
447 |
315684 |
return Options::current()[*this]; |
448 |
|
} |
449 |
39552 |
inline boolToBitvector__option_t::type boolToBitvector__option_t::operator()() const |
450 |
|
{ |
451 |
39552 |
return Options::current()[*this]; |
452 |
|
} |
453 |
1988693 |
inline bvAbstraction__option_t::type bvAbstraction__option_t::operator()() const |
454 |
|
{ |
455 |
1988693 |
return Options::current()[*this]; |
456 |
|
} |
457 |
|
inline bitvectorAigSimplifications__option_t::type bitvectorAigSimplifications__option_t::operator()() const |
458 |
|
{ |
459 |
|
return Options::current()[*this]; |
460 |
|
} |
461 |
127 |
inline bvAlgExtf__option_t::type bvAlgExtf__option_t::operator()() const |
462 |
|
{ |
463 |
127 |
return Options::current()[*this]; |
464 |
|
} |
465 |
|
inline bitvectorAlgebraicBudget__option_t::type bitvectorAlgebraicBudget__option_t::operator()() const |
466 |
|
{ |
467 |
|
return Options::current()[*this]; |
468 |
|
} |
469 |
9405 |
inline bitvectorAlgebraicSolver__option_t::type bitvectorAlgebraicSolver__option_t::operator()() const |
470 |
|
{ |
471 |
9405 |
return Options::current()[*this]; |
472 |
|
} |
473 |
|
inline bvAssertInput__option_t::type bvAssertInput__option_t::operator()() const |
474 |
|
{ |
475 |
|
return Options::current()[*this]; |
476 |
|
} |
477 |
2379321 |
inline bvEagerExplanations__option_t::type bvEagerExplanations__option_t::operator()() const |
478 |
|
{ |
479 |
2379321 |
return Options::current()[*this]; |
480 |
|
} |
481 |
18864 |
inline bitvectorEqualitySolver__option_t::type bitvectorEqualitySolver__option_t::operator()() const |
482 |
|
{ |
483 |
18864 |
return Options::current()[*this]; |
484 |
|
} |
485 |
139735 |
inline bvExtractArithRewrite__option_t::type bvExtractArithRewrite__option_t::operator()() const |
486 |
|
{ |
487 |
139735 |
return Options::current()[*this]; |
488 |
|
} |
489 |
12883 |
inline bvGaussElim__option_t::type bvGaussElim__option_t::operator()() const |
490 |
|
{ |
491 |
12883 |
return Options::current()[*this]; |
492 |
|
} |
493 |
9405 |
inline bitvectorInequalitySolver__option_t::type bitvectorInequalitySolver__option_t::operator()() const |
494 |
|
{ |
495 |
9405 |
return Options::current()[*this]; |
496 |
|
} |
497 |
15295 |
inline bvIntroducePow2__option_t::type bvIntroducePow2__option_t::operator()() const |
498 |
|
{ |
499 |
15295 |
return Options::current()[*this]; |
500 |
|
} |
501 |
57 |
inline bvLazyReduceExtf__option_t::type bvLazyReduceExtf__option_t::operator()() const |
502 |
|
{ |
503 |
57 |
return Options::current()[*this]; |
504 |
|
} |
505 |
1200 |
inline bvLazyRewriteExtf__option_t::type bvLazyRewriteExtf__option_t::operator()() const |
506 |
|
{ |
507 |
1200 |
return Options::current()[*this]; |
508 |
|
} |
509 |
|
inline bvNumFunc__option_t::type bvNumFunc__option_t::operator()() const |
510 |
|
{ |
511 |
|
return Options::current()[*this]; |
512 |
|
} |
513 |
202 |
inline bvPrintConstsAsIndexedSymbols__option_t::type bvPrintConstsAsIndexedSymbols__option_t::operator()() const |
514 |
|
{ |
515 |
202 |
return Options::current()[*this]; |
516 |
|
} |
517 |
9405 |
inline bitvectorPropagate__option_t::type bitvectorPropagate__option_t::operator()() const |
518 |
|
{ |
519 |
9405 |
return Options::current()[*this]; |
520 |
|
} |
521 |
23814 |
inline bitvectorQuickXplain__option_t::type bitvectorQuickXplain__option_t::operator()() const |
522 |
|
{ |
523 |
23814 |
return Options::current()[*this]; |
524 |
|
} |
525 |
31 |
inline bvSatSolver__option_t::type bvSatSolver__option_t::operator()() const |
526 |
|
{ |
527 |
31 |
return Options::current()[*this]; |
528 |
|
} |
529 |
4 |
inline skolemizeArguments__option_t::type skolemizeArguments__option_t::operator()() const |
530 |
|
{ |
531 |
4 |
return Options::current()[*this]; |
532 |
|
} |
533 |
41455 |
inline bvSolver__option_t::type bvSolver__option_t::operator()() const |
534 |
|
{ |
535 |
41455 |
return Options::current()[*this]; |
536 |
|
} |
537 |
15295 |
inline bitvectorToBool__option_t::type bitvectorToBool__option_t::operator()() const |
538 |
|
{ |
539 |
15295 |
return Options::current()[*this]; |
540 |
|
} |
541 |
|
// clang-format on |
542 |
|
|
543 |
|
} // namespace options |
544 |
|
} // namespace cvc5 |
545 |
|
|
546 |
|
#endif /* CVC5__OPTIONS__BV_H */ |