GCC Code Coverage Report
Directory: . Exec Total Coverage
File: build-coverage/src/options/bv_options.cpp Lines: 100 275 36.4 %
Date: 2021-03-22 Branches: 22 100 22.0 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file module_template.cpp
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 Option template for option modules.
13
 **
14
 ** For each <module>_options.toml configuration file, mkoptions.py
15
 ** expands this template and generates a <module>_options.cpp file.
16
 **/
17
18
#include "options/options_holder.h"
19
#include "base/check.h"
20
21
namespace CVC4 {
22
23
template <> void Options::set(
24
    options::bitvectorAig__option_t,
25
    const options::bitvectorAig__option_t::type& x)
26
{
27
  d_holder->bitvectorAig = x;
28
}
29
1850
template <> const options::bitvectorAig__option_t::type& Options::operator[](
30
    options::bitvectorAig__option_t) const
31
{
32
1850
  return d_holder->bitvectorAig;
33
}
34
template <> bool Options::wasSetByUser(options::bitvectorAig__option_t) const
35
{
36
  return d_holder->bitvectorAig__setByUser__;
37
}
38
template <> void Options::set(
39
    options::bitblastMode__option_t,
40
    const options::bitblastMode__option_t::type& x)
41
{
42
  d_holder->bitblastMode = x;
43
}
44
1611512
template <> const options::bitblastMode__option_t::type& Options::operator[](
45
    options::bitblastMode__option_t) const
46
{
47
1611512
  return d_holder->bitblastMode;
48
}
49
6
template <> bool Options::wasSetByUser(options::bitblastMode__option_t) const
50
{
51
6
  return d_holder->bitblastMode__setByUser__;
52
}
53
template <> void Options::set(
54
    options::bitwiseEq__option_t,
55
    const options::bitwiseEq__option_t::type& x)
56
{
57
  d_holder->bitwiseEq = x;
58
}
59
302293
template <> const options::bitwiseEq__option_t::type& Options::operator[](
60
    options::bitwiseEq__option_t) const
61
{
62
302293
  return d_holder->bitwiseEq;
63
}
64
template <> bool Options::wasSetByUser(options::bitwiseEq__option_t) const
65
{
66
  return d_holder->bitwiseEq__setByUser__;
67
}
68
template <> void Options::set(
69
    options::boolToBitvector__option_t,
70
    const options::boolToBitvector__option_t::type& x)
71
{
72
  d_holder->boolToBitvector = x;
73
}
74
53583
template <> const options::boolToBitvector__option_t::type& Options::operator[](
75
    options::boolToBitvector__option_t) const
76
{
77
53583
  return d_holder->boolToBitvector;
78
}
79
template <> bool Options::wasSetByUser(options::boolToBitvector__option_t) const
80
{
81
  return d_holder->boolToBitvector__setByUser__;
82
}
83
1529
template <> void Options::set(
84
    options::bvAbstraction__option_t,
85
    const options::bvAbstraction__option_t::type& x)
86
{
87
1529
  d_holder->bvAbstraction = x;
88
1529
}
89
1692920
template <> const options::bvAbstraction__option_t::type& Options::operator[](
90
    options::bvAbstraction__option_t) const
91
{
92
1692920
  return d_holder->bvAbstraction;
93
}
94
template <> bool Options::wasSetByUser(options::bvAbstraction__option_t) const
95
{
96
  return d_holder->bvAbstraction__setByUser__;
97
}
98
template <> void Options::set(
99
    options::bitvectorAigSimplifications__option_t,
100
    const options::bitvectorAigSimplifications__option_t::type& x)
101
{
102
  d_holder->bitvectorAigSimplifications = x;
103
}
104
template <> const options::bitvectorAigSimplifications__option_t::type& Options::operator[](
105
    options::bitvectorAigSimplifications__option_t) const
106
{
107
  return d_holder->bitvectorAigSimplifications;
108
}
109
8995
template <> bool Options::wasSetByUser(options::bitvectorAigSimplifications__option_t) const
110
{
111
8995
  return d_holder->bitvectorAigSimplifications__setByUser__;
112
}
113
template <> void Options::set(
114
    options::bvAlgExtf__option_t,
115
    const options::bvAlgExtf__option_t::type& x)
116
{
117
  d_holder->bvAlgExtf = x;
118
}
119
94
template <> const options::bvAlgExtf__option_t::type& Options::operator[](
120
    options::bvAlgExtf__option_t) const
121
{
122
94
  return d_holder->bvAlgExtf;
123
}
124
template <> bool Options::wasSetByUser(options::bvAlgExtf__option_t) const
125
{
126
  return d_holder->bvAlgExtf__setByUser__;
127
}
128
template <> void Options::set(
129
    options::bitvectorAlgebraicBudget__option_t,
130
    const options::bitvectorAlgebraicBudget__option_t::type& x)
131
{
132
  d_holder->bitvectorAlgebraicBudget = x;
133
}
134
template <> const options::bitvectorAlgebraicBudget__option_t::type& Options::operator[](
135
    options::bitvectorAlgebraicBudget__option_t) const
136
{
137
  return d_holder->bitvectorAlgebraicBudget;
138
}
139
8995
template <> bool Options::wasSetByUser(options::bitvectorAlgebraicBudget__option_t) const
140
{
141
8995
  return d_holder->bitvectorAlgebraicBudget__setByUser__;
142
}
143
template <> void Options::set(
144
    options::bitvectorAlgebraicSolver__option_t,
145
    const options::bitvectorAlgebraicSolver__option_t::type& x)
146
{
147
  d_holder->bitvectorAlgebraicSolver = x;
148
}
149
8954
template <> const options::bitvectorAlgebraicSolver__option_t::type& Options::operator[](
150
    options::bitvectorAlgebraicSolver__option_t) const
151
{
152
8954
  return d_holder->bitvectorAlgebraicSolver;
153
}
154
template <> bool Options::wasSetByUser(options::bitvectorAlgebraicSolver__option_t) const
155
{
156
  return d_holder->bitvectorAlgebraicSolver__setByUser__;
157
}
158
3632
template <> void Options::set(
159
    options::bvEagerExplanations__option_t,
160
    const options::bvEagerExplanations__option_t::type& x)
161
{
162
3632
  d_holder->bvEagerExplanations = x;
163
3632
}
164
2054144
template <> const options::bvEagerExplanations__option_t::type& Options::operator[](
165
    options::bvEagerExplanations__option_t) const
166
{
167
2054144
  return d_holder->bvEagerExplanations;
168
}
169
8995
template <> bool Options::wasSetByUser(options::bvEagerExplanations__option_t) const
170
{
171
8995
  return d_holder->bvEagerExplanations__setByUser__;
172
}
173
template <> void Options::set(
174
    options::bitvectorEqualitySolver__option_t,
175
    const options::bitvectorEqualitySolver__option_t::type& x)
176
{
177
  d_holder->bitvectorEqualitySolver = x;
178
}
179
17949
template <> const options::bitvectorEqualitySolver__option_t::type& Options::operator[](
180
    options::bitvectorEqualitySolver__option_t) const
181
{
182
17949
  return d_holder->bitvectorEqualitySolver;
183
}
184
template <> bool Options::wasSetByUser(options::bitvectorEqualitySolver__option_t) const
185
{
186
  return d_holder->bitvectorEqualitySolver__setByUser__;
187
}
188
template <> void Options::set(
189
    options::bvExtractArithRewrite__option_t,
190
    const options::bvExtractArithRewrite__option_t::type& x)
191
{
192
  d_holder->bvExtractArithRewrite = x;
193
}
194
170854
template <> const options::bvExtractArithRewrite__option_t::type& Options::operator[](
195
    options::bvExtractArithRewrite__option_t) const
196
{
197
170854
  return d_holder->bvExtractArithRewrite;
198
}
199
template <> bool Options::wasSetByUser(options::bvExtractArithRewrite__option_t) const
200
{
201
  return d_holder->bvExtractArithRewrite__setByUser__;
202
}
203
11323
template <> const options::bvGaussElim__option_t::type& Options::operator[](
204
    options::bvGaussElim__option_t) const
205
{
206
11323
  return d_holder->bvGaussElim;
207
}
208
template <> bool Options::wasSetByUser(options::bvGaussElim__option_t) const
209
{
210
  return d_holder->bvGaussElim__setByUser__;
211
}
212
template <> void Options::set(
213
    options::bitvectorInequalitySolver__option_t,
214
    const options::bitvectorInequalitySolver__option_t::type& x)
215
{
216
  d_holder->bitvectorInequalitySolver = x;
217
}
218
8954
template <> const options::bitvectorInequalitySolver__option_t::type& Options::operator[](
219
    options::bitvectorInequalitySolver__option_t) const
220
{
221
8954
  return d_holder->bitvectorInequalitySolver;
222
}
223
template <> bool Options::wasSetByUser(options::bitvectorInequalitySolver__option_t) const
224
{
225
  return d_holder->bitvectorInequalitySolver__setByUser__;
226
}
227
template <> void Options::set(
228
    options::bvIntroducePow2__option_t,
229
    const options::bvIntroducePow2__option_t::type& x)
230
{
231
  d_holder->bvIntroducePow2 = x;
232
}
233
13142
template <> const options::bvIntroducePow2__option_t::type& Options::operator[](
234
    options::bvIntroducePow2__option_t) const
235
{
236
13142
  return d_holder->bvIntroducePow2;
237
}
238
template <> bool Options::wasSetByUser(options::bvIntroducePow2__option_t) const
239
{
240
  return d_holder->bvIntroducePow2__setByUser__;
241
}
242
10
template <> void Options::set(
243
    options::bvLazyReduceExtf__option_t,
244
    const options::bvLazyReduceExtf__option_t::type& x)
245
{
246
10
  d_holder->bvLazyReduceExtf = x;
247
10
}
248
43
template <> const options::bvLazyReduceExtf__option_t::type& Options::operator[](
249
    options::bvLazyReduceExtf__option_t) const
250
{
251
43
  return d_holder->bvLazyReduceExtf;
252
}
253
template <> bool Options::wasSetByUser(options::bvLazyReduceExtf__option_t) const
254
{
255
  return d_holder->bvLazyReduceExtf__setByUser__;
256
}
257
12
template <> void Options::set(
258
    options::bvLazyRewriteExtf__option_t,
259
    const options::bvLazyRewriteExtf__option_t::type& x)
260
{
261
12
  d_holder->bvLazyRewriteExtf = x;
262
12
}
263
961
template <> const options::bvLazyRewriteExtf__option_t::type& Options::operator[](
264
    options::bvLazyRewriteExtf__option_t) const
265
{
266
961
  return d_holder->bvLazyRewriteExtf;
267
}
268
2
template <> bool Options::wasSetByUser(options::bvLazyRewriteExtf__option_t) const
269
{
270
2
  return d_holder->bvLazyRewriteExtf__setByUser__;
271
}
272
template <> const options::bvNumFunc__option_t::type& Options::operator[](
273
    options::bvNumFunc__option_t) const
274
{
275
  return d_holder->bvNumFunc;
276
}
277
template <> bool Options::wasSetByUser(options::bvNumFunc__option_t) const
278
{
279
  return d_holder->bvNumFunc__setByUser__;
280
}
281
template <> void Options::set(
282
    options::bvPrintConstsAsIndexedSymbols__option_t,
283
    const options::bvPrintConstsAsIndexedSymbols__option_t::type& x)
284
{
285
  d_holder->bvPrintConstsAsIndexedSymbols = x;
286
}
287
243
template <> const options::bvPrintConstsAsIndexedSymbols__option_t::type& Options::operator[](
288
    options::bvPrintConstsAsIndexedSymbols__option_t) const
289
{
290
243
  return d_holder->bvPrintConstsAsIndexedSymbols;
291
}
292
template <> bool Options::wasSetByUser(options::bvPrintConstsAsIndexedSymbols__option_t) const
293
{
294
  return d_holder->bvPrintConstsAsIndexedSymbols__setByUser__;
295
}
296
template <> void Options::set(
297
    options::bitvectorPropagate__option_t,
298
    const options::bitvectorPropagate__option_t::type& x)
299
{
300
  d_holder->bitvectorPropagate = x;
301
}
302
8954
template <> const options::bitvectorPropagate__option_t::type& Options::operator[](
303
    options::bitvectorPropagate__option_t) const
304
{
305
8954
  return d_holder->bitvectorPropagate;
306
}
307
template <> bool Options::wasSetByUser(options::bitvectorPropagate__option_t) const
308
{
309
  return d_holder->bitvectorPropagate__setByUser__;
310
}
311
21066
template <> const options::bitvectorQuickXplain__option_t::type& Options::operator[](
312
    options::bitvectorQuickXplain__option_t) const
313
{
314
21066
  return d_holder->bitvectorQuickXplain;
315
}
316
template <> bool Options::wasSetByUser(options::bitvectorQuickXplain__option_t) const
317
{
318
  return d_holder->bitvectorQuickXplain__setByUser__;
319
}
320
template <> void Options::set(
321
    options::bvSatSolver__option_t,
322
    const options::bvSatSolver__option_t::type& x)
323
{
324
  d_holder->bvSatSolver = x;
325
}
326
31
template <> const options::bvSatSolver__option_t::type& Options::operator[](
327
    options::bvSatSolver__option_t) const
328
{
329
31
  return d_holder->bvSatSolver;
330
}
331
template <> bool Options::wasSetByUser(options::bvSatSolver__option_t) const
332
{
333
  return d_holder->bvSatSolver__setByUser__;
334
}
335
template <> void Options::set(
336
    options::skolemizeArguments__option_t,
337
    const options::skolemizeArguments__option_t::type& x)
338
{
339
  d_holder->skolemizeArguments = x;
340
}
341
3
template <> const options::skolemizeArguments__option_t::type& Options::operator[](
342
    options::skolemizeArguments__option_t) const
343
{
344
3
  return d_holder->skolemizeArguments;
345
}
346
template <> bool Options::wasSetByUser(options::skolemizeArguments__option_t) const
347
{
348
  return d_holder->skolemizeArguments__setByUser__;
349
}
350
31
template <> void Options::set(
351
    options::bvSolver__option_t,
352
    const options::bvSolver__option_t::type& x)
353
{
354
31
  d_holder->bvSolver = x;
355
31
}
356
35992
template <> const options::bvSolver__option_t::type& Options::operator[](
357
    options::bvSolver__option_t) const
358
{
359
35992
  return d_holder->bvSolver;
360
}
361
template <> bool Options::wasSetByUser(options::bvSolver__option_t) const
362
{
363
  return d_holder->bvSolver__setByUser__;
364
}
365
159
template <> void Options::set(
366
    options::bitvectorToBool__option_t,
367
    const options::bitvectorToBool__option_t::type& x)
368
{
369
159
  d_holder->bitvectorToBool = x;
370
159
}
371
13142
template <> const options::bitvectorToBool__option_t::type& Options::operator[](
372
    options::bitvectorToBool__option_t) const
373
{
374
13142
  return d_holder->bitvectorToBool;
375
}
376
34
template <> bool Options::wasSetByUser(options::bitvectorToBool__option_t) const
377
{
378
34
  return d_holder->bitvectorToBool__setByUser__;
379
}
380
381
382
namespace options {
383
384
thread_local struct bitvectorAig__option_t bitvectorAig;
385
thread_local struct bitblastMode__option_t bitblastMode;
386
thread_local struct bitwiseEq__option_t bitwiseEq;
387
thread_local struct boolToBitvector__option_t boolToBitvector;
388
thread_local struct bvAbstraction__option_t bvAbstraction;
389
thread_local struct bitvectorAigSimplifications__option_t bitvectorAigSimplifications;
390
thread_local struct bvAlgExtf__option_t bvAlgExtf;
391
thread_local struct bitvectorAlgebraicBudget__option_t bitvectorAlgebraicBudget;
392
thread_local struct bitvectorAlgebraicSolver__option_t bitvectorAlgebraicSolver;
393
thread_local struct bvEagerExplanations__option_t bvEagerExplanations;
394
thread_local struct bitvectorEqualitySolver__option_t bitvectorEqualitySolver;
395
thread_local struct bvExtractArithRewrite__option_t bvExtractArithRewrite;
396
thread_local struct bvGaussElim__option_t bvGaussElim;
397
thread_local struct bitvectorInequalitySolver__option_t bitvectorInequalitySolver;
398
thread_local struct bvIntroducePow2__option_t bvIntroducePow2;
399
thread_local struct bvLazyReduceExtf__option_t bvLazyReduceExtf;
400
thread_local struct bvLazyRewriteExtf__option_t bvLazyRewriteExtf;
401
thread_local struct bvNumFunc__option_t bvNumFunc;
402
thread_local struct bvPrintConstsAsIndexedSymbols__option_t bvPrintConstsAsIndexedSymbols;
403
thread_local struct bitvectorPropagate__option_t bitvectorPropagate;
404
thread_local struct bitvectorQuickXplain__option_t bitvectorQuickXplain;
405
thread_local struct bvSatSolver__option_t bvSatSolver;
406
thread_local struct skolemizeArguments__option_t skolemizeArguments;
407
thread_local struct bvSolver__option_t bvSolver;
408
thread_local struct bitvectorToBool__option_t bitvectorToBool;
409
410
411
std::ostream&
412
operator<<(std::ostream& os, BitblastMode mode)
413
{
414
  os << "BitblastMode::";
415
  switch(mode) {
416
    case BitblastMode::EAGER:
417
      os << "EAGER";
418
      break;
419
    case BitblastMode::LAZY:
420
      os << "LAZY";
421
      break;
422
    default:
423
        Unreachable();
424
  }
425
  return os;
426
}
427
428
BitblastMode
429
32
stringToBitblastMode(const std::string& option, const std::string& optarg)
430
{
431
32
  if (optarg == "eager")
432
  {
433
30
    return BitblastMode::EAGER;
434
  }
435
2
  else if (optarg == "lazy")
436
  {
437
2
    return BitblastMode::LAZY;
438
  }
439
  else if (optarg == "help")
440
  {
441
    puts("Bit-blasting modes.\n"
442
         "Available modes for --bitblast are:\n"
443
         "+ eager\n"
444
         "  Bitblast eagerly to bit-vector SAT solver.\n"
445
         "+ lazy (default)\n"
446
         "  Separate boolean structure and term reasoning between the core SAT solver and\n"
447
         "  the bit-vector SAT solver.\n");
448
    exit(1);
449
  }
450
  else
451
  {
452
    throw OptionException(std::string("unknown option for --bitblast: `") +
453
                          optarg + "'.  Try --bitblast=help.");
454
  }
455
}
456
457
std::ostream&
458
operator<<(std::ostream& os, BoolToBVMode mode)
459
{
460
  os << "BoolToBVMode::";
461
  switch(mode) {
462
    case BoolToBVMode::ITE:
463
      os << "ITE";
464
      break;
465
    case BoolToBVMode::OFF:
466
      os << "OFF";
467
      break;
468
    case BoolToBVMode::ALL:
469
      os << "ALL";
470
      break;
471
    default:
472
        Unreachable();
473
  }
474
  return os;
475
}
476
477
BoolToBVMode
478
12
stringToBoolToBVMode(const std::string& option, const std::string& optarg)
479
{
480
12
  if (optarg == "ite")
481
  {
482
4
    return BoolToBVMode::ITE;
483
  }
484
8
  else if (optarg == "off")
485
  {
486
    return BoolToBVMode::OFF;
487
  }
488
8
  else if (optarg == "all")
489
  {
490
8
    return BoolToBVMode::ALL;
491
  }
492
  else if (optarg == "help")
493
  {
494
    puts("BoolToBV preprocessing pass modes.\n"
495
         "Available modes for --bool-to-bv are:\n"
496
         "+ ite\n"
497
         "  Try to turn ITEs into BITVECTOR_ITE when possible. It can fail per-formula if\n"
498
         "  not all sub-formulas can be turned to bit-vectors.\n"
499
         "+ off (default)\n"
500
         "  Don't push any booleans to width one bit-vectors.\n"
501
         "+ all\n"
502
         "  Force all booleans to be bit-vectors of width one except at the top level.\n"
503
         "  Most aggressive mode.\n");
504
    exit(1);
505
  }
506
  else
507
  {
508
    throw OptionException(std::string("unknown option for --bool-to-bv: `") +
509
                          optarg + "'.  Try --bool-to-bv=help.");
510
  }
511
}
512
513
std::ostream&
514
operator<<(std::ostream& os, SatSolverMode mode)
515
{
516
  os << "SatSolverMode::";
517
  switch(mode) {
518
    case SatSolverMode::CRYPTOMINISAT:
519
      os << "CRYPTOMINISAT";
520
      break;
521
    case SatSolverMode::MINISAT:
522
      os << "MINISAT";
523
      break;
524
    case SatSolverMode::KISSAT:
525
      os << "KISSAT";
526
      break;
527
    case SatSolverMode::CADICAL:
528
      os << "CADICAL";
529
      break;
530
    default:
531
        Unreachable();
532
  }
533
  return os;
534
}
535
536
SatSolverMode
537
14
stringToSatSolverMode(const std::string& option, const std::string& optarg)
538
{
539
14
  if (optarg == "cryptominisat")
540
  {
541
7
    return SatSolverMode::CRYPTOMINISAT;
542
  }
543
7
  else if (optarg == "minisat")
544
  {
545
2
    return SatSolverMode::MINISAT;
546
  }
547
5
  else if (optarg == "kissat")
548
  {
549
    return SatSolverMode::KISSAT;
550
  }
551
5
  else if (optarg == "cadical")
552
  {
553
3
    return SatSolverMode::CADICAL;
554
  }
555
2
  else if (optarg == "help")
556
  {
557
    puts("SAT solver for bit-blasting backend.\n"
558
         "Available modes for --bv-sat-solver are:\n"
559
         "+ cryptominisat\n"
560
         "+ minisat (default)\n"
561
         "+ kissat\n"
562
         "+ cadical\n");
563
    exit(1);
564
  }
565
  else
566
  {
567
4
    throw OptionException(std::string("unknown option for --bv-sat-solver: `") +
568
6
                          optarg + "'.  Try --bv-sat-solver=help.");
569
  }
570
}
571
572
std::ostream&
573
operator<<(std::ostream& os, BVSolver mode)
574
{
575
  os << "BVSolver::";
576
  switch(mode) {
577
    case BVSolver::SIMPLE:
578
      os << "SIMPLE";
579
      break;
580
    case BVSolver::BITBLAST:
581
      os << "BITBLAST";
582
      break;
583
    case BVSolver::LAZY:
584
      os << "LAZY";
585
      break;
586
    default:
587
        Unreachable();
588
  }
589
  return os;
590
}
591
592
BVSolver
593
13
stringToBVSolver(const std::string& option, const std::string& optarg)
594
{
595
13
  if (optarg == "simple")
596
  {
597
13
    return BVSolver::SIMPLE;
598
  }
599
  else if (optarg == "bitblast")
600
  {
601
    return BVSolver::BITBLAST;
602
  }
603
  else if (optarg == "lazy")
604
  {
605
    return BVSolver::LAZY;
606
  }
607
  else if (optarg == "help")
608
  {
609
    puts("Bit-vector solvers.\n"
610
         "Available modes for --bv-solver are:\n"
611
         "+ simple\n"
612
         "  Enables simple bitblasting solver with proof support.\n"
613
         "+ bitblast\n"
614
         "  Enables bitblasting solver.\n"
615
         "+ lazy (default)\n"
616
         "  Enables the lazy BV solver infrastructure.\n");
617
    exit(1);
618
  }
619
  else
620
  {
621
    throw OptionException(std::string("unknown option for --bv-solver: `") +
622
                          optarg + "'.  Try --bv-solver=help.");
623
  }
624
}
625
626
627
}  // namespace options
628
26676
}  // namespace CVC4