GCC Code Coverage Report
Directory: . Exec Total Coverage
File: build-coverage/src/options/bv_options.h Lines: 74 119 62.2 %
Date: 2021-03-22 Branches: 0 0 0.0 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file module_template.h
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Mathias Preiner
6
 ** This file is part of the CVC4 project.
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.\endverbatim
11
 **
12
 ** \brief Contains code for handling command-line options.
13
 **
14
 ** For each <module>_options.toml configuration file, mkoptions.py
15
 ** expands this template and generates a <module>_options.h file.
16
 **/
17
18
#include "cvc4_private.h"
19
20
#ifndef CVC4__OPTIONS__BV_H
21
#define CVC4__OPTIONS__BV_H
22
23
#include "options/options.h"
24
25
26
27
28
#define CVC4_OPTIONS__BV__FOR_OPTION_HOLDER \
29
  bitvectorAig__option_t::type bitvectorAig;\
30
  bool bitvectorAig__setByUser__; \
31
  bitblastMode__option_t::type bitblastMode;\
32
  bool bitblastMode__setByUser__; \
33
  bitwiseEq__option_t::type bitwiseEq;\
34
  bool bitwiseEq__setByUser__; \
35
  boolToBitvector__option_t::type boolToBitvector;\
36
  bool boolToBitvector__setByUser__; \
37
  bvAbstraction__option_t::type bvAbstraction;\
38
  bool bvAbstraction__setByUser__; \
39
  bitvectorAigSimplifications__option_t::type bitvectorAigSimplifications;\
40
  bool bitvectorAigSimplifications__setByUser__; \
41
  bvAlgExtf__option_t::type bvAlgExtf;\
42
  bool bvAlgExtf__setByUser__; \
43
  bitvectorAlgebraicBudget__option_t::type bitvectorAlgebraicBudget;\
44
  bool bitvectorAlgebraicBudget__setByUser__; \
45
  bitvectorAlgebraicSolver__option_t::type bitvectorAlgebraicSolver;\
46
  bool bitvectorAlgebraicSolver__setByUser__; \
47
  bvEagerExplanations__option_t::type bvEagerExplanations;\
48
  bool bvEagerExplanations__setByUser__; \
49
  bitvectorEqualitySolver__option_t::type bitvectorEqualitySolver;\
50
  bool bitvectorEqualitySolver__setByUser__; \
51
  bvExtractArithRewrite__option_t::type bvExtractArithRewrite;\
52
  bool bvExtractArithRewrite__setByUser__; \
53
  bvGaussElim__option_t::type bvGaussElim;\
54
  bool bvGaussElim__setByUser__; \
55
  bitvectorInequalitySolver__option_t::type bitvectorInequalitySolver;\
56
  bool bitvectorInequalitySolver__setByUser__; \
57
  bvIntroducePow2__option_t::type bvIntroducePow2;\
58
  bool bvIntroducePow2__setByUser__; \
59
  bvLazyReduceExtf__option_t::type bvLazyReduceExtf;\
60
  bool bvLazyReduceExtf__setByUser__; \
61
  bvLazyRewriteExtf__option_t::type bvLazyRewriteExtf;\
62
  bool bvLazyRewriteExtf__setByUser__; \
63
  bvNumFunc__option_t::type bvNumFunc;\
64
  bool bvNumFunc__setByUser__; \
65
  bvPrintConstsAsIndexedSymbols__option_t::type bvPrintConstsAsIndexedSymbols;\
66
  bool bvPrintConstsAsIndexedSymbols__setByUser__; \
67
  bitvectorPropagate__option_t::type bitvectorPropagate;\
68
  bool bitvectorPropagate__setByUser__; \
69
  bitvectorQuickXplain__option_t::type bitvectorQuickXplain;\
70
  bool bitvectorQuickXplain__setByUser__; \
71
  bvSatSolver__option_t::type bvSatSolver;\
72
  bool bvSatSolver__setByUser__; \
73
  skolemizeArguments__option_t::type skolemizeArguments;\
74
  bool skolemizeArguments__setByUser__; \
75
  bvSolver__option_t::type bvSolver;\
76
  bool bvSolver__setByUser__; \
77
  bitvectorToBool__option_t::type bitvectorToBool;\
78
  bool bitvectorToBool__setByUser__;
79
80
81
namespace CVC4 {
82
83
namespace options {
84
85
86
enum class BitblastMode
87
{
88
  EAGER,
89
  LAZY
90
};
91
std::ostream&
92
operator<<(std::ostream& os, BitblastMode mode);
93
BitblastMode
94
stringToBitblastMode(const std::string& option, const std::string& optarg);
95
enum class BoolToBVMode
96
{
97
  ITE,
98
  OFF,
99
  ALL
100
};
101
std::ostream&
102
operator<<(std::ostream& os, BoolToBVMode mode);
103
BoolToBVMode
104
stringToBoolToBVMode(const std::string& option, const std::string& optarg);
105
enum class SatSolverMode
106
{
107
  CRYPTOMINISAT,
108
  MINISAT,
109
  KISSAT,
110
  CADICAL
111
};
112
std::ostream&
113
operator<<(std::ostream& os, SatSolverMode mode);
114
SatSolverMode
115
stringToSatSolverMode(const std::string& option, const std::string& optarg);
116
enum class BVSolver
117
{
118
  SIMPLE,
119
  BITBLAST,
120
  LAZY
121
};
122
std::ostream&
123
operator<<(std::ostream& os, BVSolver mode);
124
BVSolver
125
stringToBVSolver(const std::string& option, const std::string& optarg);
126
127
extern struct bitvectorAig__option_t
128
{
129
  typedef bool type;
130
  type operator()() const;
131
  bool wasSetByUser() const;
132
  void set(const type& v);
133
  const char* getName() const;
134
} thread_local bitvectorAig;
135
extern struct bitblastMode__option_t
136
{
137
  typedef BitblastMode type;
138
  type operator()() const;
139
  bool wasSetByUser() const;
140
  void set(const type& v);
141
  const char* getName() const;
142
} thread_local bitblastMode;
143
extern struct bitwiseEq__option_t
144
{
145
  typedef bool type;
146
  type operator()() const;
147
  bool wasSetByUser() const;
148
  void set(const type& v);
149
  const char* getName() const;
150
} thread_local bitwiseEq;
151
extern struct boolToBitvector__option_t
152
{
153
  typedef BoolToBVMode type;
154
  type operator()() const;
155
  bool wasSetByUser() const;
156
  void set(const type& v);
157
  const char* getName() const;
158
} thread_local boolToBitvector;
159
extern struct bvAbstraction__option_t
160
{
161
  typedef bool type;
162
  type operator()() const;
163
  bool wasSetByUser() const;
164
  void set(const type& v);
165
  const char* getName() const;
166
} thread_local bvAbstraction;
167
extern struct bitvectorAigSimplifications__option_t
168
{
169
  typedef std::string type;
170
  type operator()() const;
171
  bool wasSetByUser() const;
172
  void set(const type& v);
173
  const char* getName() const;
174
} thread_local bitvectorAigSimplifications;
175
extern struct bvAlgExtf__option_t
176
{
177
  typedef bool type;
178
  type operator()() const;
179
  bool wasSetByUser() const;
180
  void set(const type& v);
181
  const char* getName() const;
182
} thread_local bvAlgExtf;
183
extern struct bitvectorAlgebraicBudget__option_t
184
{
185
  typedef unsigned type;
186
  type operator()() const;
187
  bool wasSetByUser() const;
188
  void set(const type& v);
189
  const char* getName() const;
190
} thread_local bitvectorAlgebraicBudget;
191
extern struct bitvectorAlgebraicSolver__option_t
192
{
193
  typedef bool type;
194
  type operator()() const;
195
  bool wasSetByUser() const;
196
  void set(const type& v);
197
  const char* getName() const;
198
} thread_local bitvectorAlgebraicSolver;
199
extern struct bvEagerExplanations__option_t
200
{
201
  typedef bool type;
202
  type operator()() const;
203
  bool wasSetByUser() const;
204
  void set(const type& v);
205
  const char* getName() const;
206
} thread_local bvEagerExplanations;
207
extern struct bitvectorEqualitySolver__option_t
208
{
209
  typedef bool type;
210
  type operator()() const;
211
  bool wasSetByUser() const;
212
  void set(const type& v);
213
  const char* getName() const;
214
} thread_local bitvectorEqualitySolver;
215
extern struct bvExtractArithRewrite__option_t
216
{
217
  typedef bool type;
218
  type operator()() const;
219
  bool wasSetByUser() const;
220
  void set(const type& v);
221
  const char* getName() const;
222
} thread_local bvExtractArithRewrite;
223
extern struct bvGaussElim__option_t
224
{
225
  typedef bool type;
226
  type operator()() const;
227
  bool wasSetByUser() const;
228
  const char* getName() const;
229
} thread_local bvGaussElim;
230
extern struct bitvectorInequalitySolver__option_t
231
{
232
  typedef bool type;
233
  type operator()() const;
234
  bool wasSetByUser() const;
235
  void set(const type& v);
236
  const char* getName() const;
237
} thread_local bitvectorInequalitySolver;
238
extern struct bvIntroducePow2__option_t
239
{
240
  typedef bool type;
241
  type operator()() const;
242
  bool wasSetByUser() const;
243
  void set(const type& v);
244
  const char* getName() const;
245
} thread_local bvIntroducePow2;
246
extern struct bvLazyReduceExtf__option_t
247
{
248
  typedef bool type;
249
  type operator()() const;
250
  bool wasSetByUser() const;
251
  void set(const type& v);
252
  const char* getName() const;
253
} thread_local bvLazyReduceExtf;
254
extern struct bvLazyRewriteExtf__option_t
255
{
256
  typedef bool type;
257
  type operator()() const;
258
  bool wasSetByUser() const;
259
  void set(const type& v);
260
  const char* getName() const;
261
} thread_local bvLazyRewriteExtf;
262
extern struct bvNumFunc__option_t
263
{
264
  typedef unsigned type;
265
  type operator()() const;
266
  bool wasSetByUser() const;
267
  const char* getName() const;
268
} thread_local bvNumFunc;
269
extern struct bvPrintConstsAsIndexedSymbols__option_t
270
{
271
  typedef bool type;
272
  type operator()() const;
273
  bool wasSetByUser() const;
274
  void set(const type& v);
275
  const char* getName() const;
276
} thread_local bvPrintConstsAsIndexedSymbols;
277
extern struct bitvectorPropagate__option_t
278
{
279
  typedef bool type;
280
  type operator()() const;
281
  bool wasSetByUser() const;
282
  void set(const type& v);
283
  const char* getName() const;
284
} thread_local bitvectorPropagate;
285
extern struct bitvectorQuickXplain__option_t
286
{
287
  typedef bool type;
288
  type operator()() const;
289
  bool wasSetByUser() const;
290
  const char* getName() const;
291
} thread_local bitvectorQuickXplain;
292
extern struct bvSatSolver__option_t
293
{
294
  typedef SatSolverMode type;
295
  type operator()() const;
296
  bool wasSetByUser() const;
297
  void set(const type& v);
298
  const char* getName() const;
299
} thread_local bvSatSolver;
300
extern struct skolemizeArguments__option_t
301
{
302
  typedef bool type;
303
  type operator()() const;
304
  bool wasSetByUser() const;
305
  void set(const type& v);
306
  const char* getName() const;
307
} thread_local skolemizeArguments;
308
extern struct bvSolver__option_t
309
{
310
  typedef BVSolver type;
311
  type operator()() const;
312
  bool wasSetByUser() const;
313
  void set(const type& v);
314
  const char* getName() const;
315
} thread_local bvSolver;
316
extern struct bitvectorToBool__option_t
317
{
318
  typedef bool type;
319
  type operator()() const;
320
  bool wasSetByUser() const;
321
  void set(const type& v);
322
  const char* getName() const;
323
} thread_local bitvectorToBool;
324
325
}  // namespace options
326
327
template <> void Options::set(
328
    options::bitvectorAig__option_t,
329
    const options::bitvectorAig__option_t::type& x);
330
template <> const options::bitvectorAig__option_t::type& Options::operator[](
331
    options::bitvectorAig__option_t) const;
332
template <> bool Options::wasSetByUser(options::bitvectorAig__option_t) const;
333
template <> void Options::assignBool(
334
    options::bitvectorAig__option_t,
335
    std::string option,
336
    bool value);
337
template <> void Options::set(
338
    options::bitblastMode__option_t,
339
    const options::bitblastMode__option_t::type& x);
340
template <> const options::bitblastMode__option_t::type& Options::operator[](
341
    options::bitblastMode__option_t) const;
342
template <> bool Options::wasSetByUser(options::bitblastMode__option_t) const;
343
template <> void Options::assign(
344
    options::bitblastMode__option_t,
345
    std::string option,
346
    std::string value);
347
template <> void Options::set(
348
    options::bitwiseEq__option_t,
349
    const options::bitwiseEq__option_t::type& x);
350
template <> const options::bitwiseEq__option_t::type& Options::operator[](
351
    options::bitwiseEq__option_t) const;
352
template <> bool Options::wasSetByUser(options::bitwiseEq__option_t) const;
353
template <> void Options::assignBool(
354
    options::bitwiseEq__option_t,
355
    std::string option,
356
    bool value);
357
template <> void Options::set(
358
    options::boolToBitvector__option_t,
359
    const options::boolToBitvector__option_t::type& x);
360
template <> const options::boolToBitvector__option_t::type& Options::operator[](
361
    options::boolToBitvector__option_t) const;
362
template <> bool Options::wasSetByUser(options::boolToBitvector__option_t) const;
363
template <> void Options::assign(
364
    options::boolToBitvector__option_t,
365
    std::string option,
366
    std::string value);
367
template <> void Options::set(
368
    options::bvAbstraction__option_t,
369
    const options::bvAbstraction__option_t::type& x);
370
template <> const options::bvAbstraction__option_t::type& Options::operator[](
371
    options::bvAbstraction__option_t) const;
372
template <> bool Options::wasSetByUser(options::bvAbstraction__option_t) const;
373
template <> void Options::assignBool(
374
    options::bvAbstraction__option_t,
375
    std::string option,
376
    bool value);
377
template <> void Options::set(
378
    options::bitvectorAigSimplifications__option_t,
379
    const options::bitvectorAigSimplifications__option_t::type& x);
380
template <> const options::bitvectorAigSimplifications__option_t::type& Options::operator[](
381
    options::bitvectorAigSimplifications__option_t) const;
382
template <> bool Options::wasSetByUser(options::bitvectorAigSimplifications__option_t) const;
383
template <> void Options::assign(
384
    options::bitvectorAigSimplifications__option_t,
385
    std::string option,
386
    std::string value);
387
template <> void Options::set(
388
    options::bvAlgExtf__option_t,
389
    const options::bvAlgExtf__option_t::type& x);
390
template <> const options::bvAlgExtf__option_t::type& Options::operator[](
391
    options::bvAlgExtf__option_t) const;
392
template <> bool Options::wasSetByUser(options::bvAlgExtf__option_t) const;
393
template <> void Options::assignBool(
394
    options::bvAlgExtf__option_t,
395
    std::string option,
396
    bool value);
397
template <> void Options::set(
398
    options::bitvectorAlgebraicBudget__option_t,
399
    const options::bitvectorAlgebraicBudget__option_t::type& x);
400
template <> const options::bitvectorAlgebraicBudget__option_t::type& Options::operator[](
401
    options::bitvectorAlgebraicBudget__option_t) const;
402
template <> bool Options::wasSetByUser(options::bitvectorAlgebraicBudget__option_t) const;
403
template <> void Options::assign(
404
    options::bitvectorAlgebraicBudget__option_t,
405
    std::string option,
406
    std::string value);
407
template <> void Options::set(
408
    options::bitvectorAlgebraicSolver__option_t,
409
    const options::bitvectorAlgebraicSolver__option_t::type& x);
410
template <> const options::bitvectorAlgebraicSolver__option_t::type& Options::operator[](
411
    options::bitvectorAlgebraicSolver__option_t) const;
412
template <> bool Options::wasSetByUser(options::bitvectorAlgebraicSolver__option_t) const;
413
template <> void Options::assignBool(
414
    options::bitvectorAlgebraicSolver__option_t,
415
    std::string option,
416
    bool value);
417
template <> void Options::set(
418
    options::bvEagerExplanations__option_t,
419
    const options::bvEagerExplanations__option_t::type& x);
420
template <> const options::bvEagerExplanations__option_t::type& Options::operator[](
421
    options::bvEagerExplanations__option_t) const;
422
template <> bool Options::wasSetByUser(options::bvEagerExplanations__option_t) const;
423
template <> void Options::assignBool(
424
    options::bvEagerExplanations__option_t,
425
    std::string option,
426
    bool value);
427
template <> void Options::set(
428
    options::bitvectorEqualitySolver__option_t,
429
    const options::bitvectorEqualitySolver__option_t::type& x);
430
template <> const options::bitvectorEqualitySolver__option_t::type& Options::operator[](
431
    options::bitvectorEqualitySolver__option_t) const;
432
template <> bool Options::wasSetByUser(options::bitvectorEqualitySolver__option_t) const;
433
template <> void Options::assignBool(
434
    options::bitvectorEqualitySolver__option_t,
435
    std::string option,
436
    bool value);
437
template <> void Options::set(
438
    options::bvExtractArithRewrite__option_t,
439
    const options::bvExtractArithRewrite__option_t::type& x);
440
template <> const options::bvExtractArithRewrite__option_t::type& Options::operator[](
441
    options::bvExtractArithRewrite__option_t) const;
442
template <> bool Options::wasSetByUser(options::bvExtractArithRewrite__option_t) const;
443
template <> void Options::assignBool(
444
    options::bvExtractArithRewrite__option_t,
445
    std::string option,
446
    bool value);
447
template <> const options::bvGaussElim__option_t::type& Options::operator[](
448
    options::bvGaussElim__option_t) const;
449
template <> bool Options::wasSetByUser(options::bvGaussElim__option_t) const;
450
template <> void Options::assignBool(
451
    options::bvGaussElim__option_t,
452
    std::string option,
453
    bool value);
454
template <> void Options::set(
455
    options::bitvectorInequalitySolver__option_t,
456
    const options::bitvectorInequalitySolver__option_t::type& x);
457
template <> const options::bitvectorInequalitySolver__option_t::type& Options::operator[](
458
    options::bitvectorInequalitySolver__option_t) const;
459
template <> bool Options::wasSetByUser(options::bitvectorInequalitySolver__option_t) const;
460
template <> void Options::assignBool(
461
    options::bitvectorInequalitySolver__option_t,
462
    std::string option,
463
    bool value);
464
template <> void Options::set(
465
    options::bvIntroducePow2__option_t,
466
    const options::bvIntroducePow2__option_t::type& x);
467
template <> const options::bvIntroducePow2__option_t::type& Options::operator[](
468
    options::bvIntroducePow2__option_t) const;
469
template <> bool Options::wasSetByUser(options::bvIntroducePow2__option_t) const;
470
template <> void Options::assignBool(
471
    options::bvIntroducePow2__option_t,
472
    std::string option,
473
    bool value);
474
template <> void Options::set(
475
    options::bvLazyReduceExtf__option_t,
476
    const options::bvLazyReduceExtf__option_t::type& x);
477
template <> const options::bvLazyReduceExtf__option_t::type& Options::operator[](
478
    options::bvLazyReduceExtf__option_t) const;
479
template <> bool Options::wasSetByUser(options::bvLazyReduceExtf__option_t) const;
480
template <> void Options::assignBool(
481
    options::bvLazyReduceExtf__option_t,
482
    std::string option,
483
    bool value);
484
template <> void Options::set(
485
    options::bvLazyRewriteExtf__option_t,
486
    const options::bvLazyRewriteExtf__option_t::type& x);
487
template <> const options::bvLazyRewriteExtf__option_t::type& Options::operator[](
488
    options::bvLazyRewriteExtf__option_t) const;
489
template <> bool Options::wasSetByUser(options::bvLazyRewriteExtf__option_t) const;
490
template <> void Options::assignBool(
491
    options::bvLazyRewriteExtf__option_t,
492
    std::string option,
493
    bool value);
494
template <> const options::bvNumFunc__option_t::type& Options::operator[](
495
    options::bvNumFunc__option_t) const;
496
template <> bool Options::wasSetByUser(options::bvNumFunc__option_t) const;
497
template <> void Options::assign(
498
    options::bvNumFunc__option_t,
499
    std::string option,
500
    std::string value);
501
template <> void Options::set(
502
    options::bvPrintConstsAsIndexedSymbols__option_t,
503
    const options::bvPrintConstsAsIndexedSymbols__option_t::type& x);
504
template <> const options::bvPrintConstsAsIndexedSymbols__option_t::type& Options::operator[](
505
    options::bvPrintConstsAsIndexedSymbols__option_t) const;
506
template <> bool Options::wasSetByUser(options::bvPrintConstsAsIndexedSymbols__option_t) const;
507
template <> void Options::assignBool(
508
    options::bvPrintConstsAsIndexedSymbols__option_t,
509
    std::string option,
510
    bool value);
511
template <> void Options::set(
512
    options::bitvectorPropagate__option_t,
513
    const options::bitvectorPropagate__option_t::type& x);
514
template <> const options::bitvectorPropagate__option_t::type& Options::operator[](
515
    options::bitvectorPropagate__option_t) const;
516
template <> bool Options::wasSetByUser(options::bitvectorPropagate__option_t) const;
517
template <> void Options::assignBool(
518
    options::bitvectorPropagate__option_t,
519
    std::string option,
520
    bool value);
521
template <> const options::bitvectorQuickXplain__option_t::type& Options::operator[](
522
    options::bitvectorQuickXplain__option_t) const;
523
template <> bool Options::wasSetByUser(options::bitvectorQuickXplain__option_t) const;
524
template <> void Options::assignBool(
525
    options::bitvectorQuickXplain__option_t,
526
    std::string option,
527
    bool value);
528
template <> void Options::set(
529
    options::bvSatSolver__option_t,
530
    const options::bvSatSolver__option_t::type& x);
531
template <> const options::bvSatSolver__option_t::type& Options::operator[](
532
    options::bvSatSolver__option_t) const;
533
template <> bool Options::wasSetByUser(options::bvSatSolver__option_t) const;
534
template <> void Options::assign(
535
    options::bvSatSolver__option_t,
536
    std::string option,
537
    std::string value);
538
template <> void Options::set(
539
    options::skolemizeArguments__option_t,
540
    const options::skolemizeArguments__option_t::type& x);
541
template <> const options::skolemizeArguments__option_t::type& Options::operator[](
542
    options::skolemizeArguments__option_t) const;
543
template <> bool Options::wasSetByUser(options::skolemizeArguments__option_t) const;
544
template <> void Options::assignBool(
545
    options::skolemizeArguments__option_t,
546
    std::string option,
547
    bool value);
548
template <> void Options::set(
549
    options::bvSolver__option_t,
550
    const options::bvSolver__option_t::type& x);
551
template <> const options::bvSolver__option_t::type& Options::operator[](
552
    options::bvSolver__option_t) const;
553
template <> bool Options::wasSetByUser(options::bvSolver__option_t) const;
554
template <> void Options::assign(
555
    options::bvSolver__option_t,
556
    std::string option,
557
    std::string value);
558
template <> void Options::set(
559
    options::bitvectorToBool__option_t,
560
    const options::bitvectorToBool__option_t::type& x);
561
template <> const options::bitvectorToBool__option_t::type& Options::operator[](
562
    options::bitvectorToBool__option_t) const;
563
template <> bool Options::wasSetByUser(options::bitvectorToBool__option_t) const;
564
template <> void Options::assignBool(
565
    options::bitvectorToBool__option_t,
566
    std::string option,
567
    bool value);
568
569
570
namespace options {
571
572
1850
inline bitvectorAig__option_t::type bitvectorAig__option_t::operator()() const
573
{
574
1850
  return (*Options::current())[*this];
575
}
576
inline bool bitvectorAig__option_t::wasSetByUser() const
577
{
578
  return Options::current()->wasSetByUser(*this);
579
}
580
inline void bitvectorAig__option_t::set(const bitvectorAig__option_t::type& v)
581
{
582
  Options::current()->set(*this, v);
583
}
584
inline const char* bitvectorAig__option_t::getName() const
585
{
586
  return "bitblast-aig";
587
}
588
1611512
inline bitblastMode__option_t::type bitblastMode__option_t::operator()() const
589
{
590
1611512
  return (*Options::current())[*this];
591
}
592
6
inline bool bitblastMode__option_t::wasSetByUser() const
593
{
594
6
  return Options::current()->wasSetByUser(*this);
595
}
596
inline void bitblastMode__option_t::set(const bitblastMode__option_t::type& v)
597
{
598
  Options::current()->set(*this, v);
599
}
600
inline const char* bitblastMode__option_t::getName() const
601
{
602
  return "bitblast";
603
}
604
302293
inline bitwiseEq__option_t::type bitwiseEq__option_t::operator()() const
605
{
606
302293
  return (*Options::current())[*this];
607
}
608
inline bool bitwiseEq__option_t::wasSetByUser() const
609
{
610
  return Options::current()->wasSetByUser(*this);
611
}
612
inline void bitwiseEq__option_t::set(const bitwiseEq__option_t::type& v)
613
{
614
  Options::current()->set(*this, v);
615
}
616
inline const char* bitwiseEq__option_t::getName() const
617
{
618
  return "bitwise-eq";
619
}
620
53583
inline boolToBitvector__option_t::type boolToBitvector__option_t::operator()() const
621
{
622
53583
  return (*Options::current())[*this];
623
}
624
inline bool boolToBitvector__option_t::wasSetByUser() const
625
{
626
  return Options::current()->wasSetByUser(*this);
627
}
628
inline void boolToBitvector__option_t::set(const boolToBitvector__option_t::type& v)
629
{
630
  Options::current()->set(*this, v);
631
}
632
inline const char* boolToBitvector__option_t::getName() const
633
{
634
  return "bool-to-bv";
635
}
636
1692920
inline bvAbstraction__option_t::type bvAbstraction__option_t::operator()() const
637
{
638
1692920
  return (*Options::current())[*this];
639
}
640
inline bool bvAbstraction__option_t::wasSetByUser() const
641
{
642
  return Options::current()->wasSetByUser(*this);
643
}
644
1529
inline void bvAbstraction__option_t::set(const bvAbstraction__option_t::type& v)
645
{
646
1529
  Options::current()->set(*this, v);
647
1529
}
648
inline const char* bvAbstraction__option_t::getName() const
649
{
650
  return "bv-abstraction";
651
}
652
inline bitvectorAigSimplifications__option_t::type bitvectorAigSimplifications__option_t::operator()() const
653
{
654
  return (*Options::current())[*this];
655
}
656
8995
inline bool bitvectorAigSimplifications__option_t::wasSetByUser() const
657
{
658
8995
  return Options::current()->wasSetByUser(*this);
659
}
660
inline void bitvectorAigSimplifications__option_t::set(const bitvectorAigSimplifications__option_t::type& v)
661
{
662
  Options::current()->set(*this, v);
663
}
664
inline const char* bitvectorAigSimplifications__option_t::getName() const
665
{
666
  return "bv-aig-simp";
667
}
668
94
inline bvAlgExtf__option_t::type bvAlgExtf__option_t::operator()() const
669
{
670
94
  return (*Options::current())[*this];
671
}
672
inline bool bvAlgExtf__option_t::wasSetByUser() const
673
{
674
  return Options::current()->wasSetByUser(*this);
675
}
676
inline void bvAlgExtf__option_t::set(const bvAlgExtf__option_t::type& v)
677
{
678
  Options::current()->set(*this, v);
679
}
680
inline const char* bvAlgExtf__option_t::getName() const
681
{
682
  return "bv-alg-extf";
683
}
684
inline bitvectorAlgebraicBudget__option_t::type bitvectorAlgebraicBudget__option_t::operator()() const
685
{
686
  return (*Options::current())[*this];
687
}
688
8995
inline bool bitvectorAlgebraicBudget__option_t::wasSetByUser() const
689
{
690
8995
  return Options::current()->wasSetByUser(*this);
691
}
692
inline void bitvectorAlgebraicBudget__option_t::set(const bitvectorAlgebraicBudget__option_t::type& v)
693
{
694
  Options::current()->set(*this, v);
695
}
696
inline const char* bitvectorAlgebraicBudget__option_t::getName() const
697
{
698
  return "bv-algebraic-budget";
699
}
700
8954
inline bitvectorAlgebraicSolver__option_t::type bitvectorAlgebraicSolver__option_t::operator()() const
701
{
702
8954
  return (*Options::current())[*this];
703
}
704
inline bool bitvectorAlgebraicSolver__option_t::wasSetByUser() const
705
{
706
  return Options::current()->wasSetByUser(*this);
707
}
708
inline void bitvectorAlgebraicSolver__option_t::set(const bitvectorAlgebraicSolver__option_t::type& v)
709
{
710
  Options::current()->set(*this, v);
711
}
712
inline const char* bitvectorAlgebraicSolver__option_t::getName() const
713
{
714
  return "bv-algebraic-solver";
715
}
716
2054144
inline bvEagerExplanations__option_t::type bvEagerExplanations__option_t::operator()() const
717
{
718
2054144
  return (*Options::current())[*this];
719
}
720
8995
inline bool bvEagerExplanations__option_t::wasSetByUser() const
721
{
722
8995
  return Options::current()->wasSetByUser(*this);
723
}
724
3632
inline void bvEagerExplanations__option_t::set(const bvEagerExplanations__option_t::type& v)
725
{
726
3632
  Options::current()->set(*this, v);
727
3632
}
728
inline const char* bvEagerExplanations__option_t::getName() const
729
{
730
  return "bv-eager-explanations";
731
}
732
17949
inline bitvectorEqualitySolver__option_t::type bitvectorEqualitySolver__option_t::operator()() const
733
{
734
17949
  return (*Options::current())[*this];
735
}
736
inline bool bitvectorEqualitySolver__option_t::wasSetByUser() const
737
{
738
  return Options::current()->wasSetByUser(*this);
739
}
740
inline void bitvectorEqualitySolver__option_t::set(const bitvectorEqualitySolver__option_t::type& v)
741
{
742
  Options::current()->set(*this, v);
743
}
744
inline const char* bitvectorEqualitySolver__option_t::getName() const
745
{
746
  return "bv-eq-solver";
747
}
748
170854
inline bvExtractArithRewrite__option_t::type bvExtractArithRewrite__option_t::operator()() const
749
{
750
170854
  return (*Options::current())[*this];
751
}
752
inline bool bvExtractArithRewrite__option_t::wasSetByUser() const
753
{
754
  return Options::current()->wasSetByUser(*this);
755
}
756
inline void bvExtractArithRewrite__option_t::set(const bvExtractArithRewrite__option_t::type& v)
757
{
758
  Options::current()->set(*this, v);
759
}
760
inline const char* bvExtractArithRewrite__option_t::getName() const
761
{
762
  return "bv-extract-arith";
763
}
764
11323
inline bvGaussElim__option_t::type bvGaussElim__option_t::operator()() const
765
{
766
11323
  return (*Options::current())[*this];
767
}
768
inline bool bvGaussElim__option_t::wasSetByUser() const
769
{
770
  return Options::current()->wasSetByUser(*this);
771
}
772
inline const char* bvGaussElim__option_t::getName() const
773
{
774
  return "bv-gauss-elim";
775
}
776
8954
inline bitvectorInequalitySolver__option_t::type bitvectorInequalitySolver__option_t::operator()() const
777
{
778
8954
  return (*Options::current())[*this];
779
}
780
inline bool bitvectorInequalitySolver__option_t::wasSetByUser() const
781
{
782
  return Options::current()->wasSetByUser(*this);
783
}
784
inline void bitvectorInequalitySolver__option_t::set(const bitvectorInequalitySolver__option_t::type& v)
785
{
786
  Options::current()->set(*this, v);
787
}
788
inline const char* bitvectorInequalitySolver__option_t::getName() const
789
{
790
  return "bv-inequality-solver";
791
}
792
13142
inline bvIntroducePow2__option_t::type bvIntroducePow2__option_t::operator()() const
793
{
794
13142
  return (*Options::current())[*this];
795
}
796
inline bool bvIntroducePow2__option_t::wasSetByUser() const
797
{
798
  return Options::current()->wasSetByUser(*this);
799
}
800
inline void bvIntroducePow2__option_t::set(const bvIntroducePow2__option_t::type& v)
801
{
802
  Options::current()->set(*this, v);
803
}
804
inline const char* bvIntroducePow2__option_t::getName() const
805
{
806
  return "bv-intro-pow2";
807
}
808
43
inline bvLazyReduceExtf__option_t::type bvLazyReduceExtf__option_t::operator()() const
809
{
810
43
  return (*Options::current())[*this];
811
}
812
inline bool bvLazyReduceExtf__option_t::wasSetByUser() const
813
{
814
  return Options::current()->wasSetByUser(*this);
815
}
816
10
inline void bvLazyReduceExtf__option_t::set(const bvLazyReduceExtf__option_t::type& v)
817
{
818
10
  Options::current()->set(*this, v);
819
10
}
820
inline const char* bvLazyReduceExtf__option_t::getName() const
821
{
822
  return "bv-lazy-reduce-extf";
823
}
824
961
inline bvLazyRewriteExtf__option_t::type bvLazyRewriteExtf__option_t::operator()() const
825
{
826
961
  return (*Options::current())[*this];
827
}
828
2
inline bool bvLazyRewriteExtf__option_t::wasSetByUser() const
829
{
830
2
  return Options::current()->wasSetByUser(*this);
831
}
832
12
inline void bvLazyRewriteExtf__option_t::set(const bvLazyRewriteExtf__option_t::type& v)
833
{
834
12
  Options::current()->set(*this, v);
835
12
}
836
inline const char* bvLazyRewriteExtf__option_t::getName() const
837
{
838
  return "bv-lazy-rewrite-extf";
839
}
840
inline bvNumFunc__option_t::type bvNumFunc__option_t::operator()() const
841
{
842
  return (*Options::current())[*this];
843
}
844
inline bool bvNumFunc__option_t::wasSetByUser() const
845
{
846
  return Options::current()->wasSetByUser(*this);
847
}
848
inline const char* bvNumFunc__option_t::getName() const
849
{
850
  return "bv-num-func";
851
}
852
243
inline bvPrintConstsAsIndexedSymbols__option_t::type bvPrintConstsAsIndexedSymbols__option_t::operator()() const
853
{
854
243
  return (*Options::current())[*this];
855
}
856
inline bool bvPrintConstsAsIndexedSymbols__option_t::wasSetByUser() const
857
{
858
  return Options::current()->wasSetByUser(*this);
859
}
860
inline void bvPrintConstsAsIndexedSymbols__option_t::set(const bvPrintConstsAsIndexedSymbols__option_t::type& v)
861
{
862
  Options::current()->set(*this, v);
863
}
864
inline const char* bvPrintConstsAsIndexedSymbols__option_t::getName() const
865
{
866
  return "bv-print-consts-as-indexed-symbols";
867
}
868
8954
inline bitvectorPropagate__option_t::type bitvectorPropagate__option_t::operator()() const
869
{
870
8954
  return (*Options::current())[*this];
871
}
872
inline bool bitvectorPropagate__option_t::wasSetByUser() const
873
{
874
  return Options::current()->wasSetByUser(*this);
875
}
876
inline void bitvectorPropagate__option_t::set(const bitvectorPropagate__option_t::type& v)
877
{
878
  Options::current()->set(*this, v);
879
}
880
inline const char* bitvectorPropagate__option_t::getName() const
881
{
882
  return "bv-propagate";
883
}
884
21066
inline bitvectorQuickXplain__option_t::type bitvectorQuickXplain__option_t::operator()() const
885
{
886
21066
  return (*Options::current())[*this];
887
}
888
inline bool bitvectorQuickXplain__option_t::wasSetByUser() const
889
{
890
  return Options::current()->wasSetByUser(*this);
891
}
892
inline const char* bitvectorQuickXplain__option_t::getName() const
893
{
894
  return "bv-quick-xplain";
895
}
896
31
inline bvSatSolver__option_t::type bvSatSolver__option_t::operator()() const
897
{
898
31
  return (*Options::current())[*this];
899
}
900
inline bool bvSatSolver__option_t::wasSetByUser() const
901
{
902
  return Options::current()->wasSetByUser(*this);
903
}
904
inline void bvSatSolver__option_t::set(const bvSatSolver__option_t::type& v)
905
{
906
  Options::current()->set(*this, v);
907
}
908
inline const char* bvSatSolver__option_t::getName() const
909
{
910
  return "bv-sat-solver";
911
}
912
3
inline skolemizeArguments__option_t::type skolemizeArguments__option_t::operator()() const
913
{
914
3
  return (*Options::current())[*this];
915
}
916
inline bool skolemizeArguments__option_t::wasSetByUser() const
917
{
918
  return Options::current()->wasSetByUser(*this);
919
}
920
inline void skolemizeArguments__option_t::set(const skolemizeArguments__option_t::type& v)
921
{
922
  Options::current()->set(*this, v);
923
}
924
inline const char* skolemizeArguments__option_t::getName() const
925
{
926
  return "bv-skolemize";
927
}
928
35992
inline bvSolver__option_t::type bvSolver__option_t::operator()() const
929
{
930
35992
  return (*Options::current())[*this];
931
}
932
inline bool bvSolver__option_t::wasSetByUser() const
933
{
934
  return Options::current()->wasSetByUser(*this);
935
}
936
31
inline void bvSolver__option_t::set(const bvSolver__option_t::type& v)
937
{
938
31
  Options::current()->set(*this, v);
939
31
}
940
inline const char* bvSolver__option_t::getName() const
941
{
942
  return "bv-solver";
943
}
944
13142
inline bitvectorToBool__option_t::type bitvectorToBool__option_t::operator()() const
945
{
946
13142
  return (*Options::current())[*this];
947
}
948
34
inline bool bitvectorToBool__option_t::wasSetByUser() const
949
{
950
34
  return Options::current()->wasSetByUser(*this);
951
}
952
159
inline void bitvectorToBool__option_t::set(const bitvectorToBool__option_t::type& v)
953
{
954
159
  Options::current()->set(*this, v);
955
159
}
956
inline const char* bitvectorToBool__option_t::getName() const
957
{
958
  return "bv-to-bool";
959
}
960
961
}  // namespace options
962
}  // namespace CVC4
963
964
#endif /* CVC4__OPTIONS__BV_H */