GCC Code Coverage Report
Directory: . Exec Total Coverage
File: build-coverage/src/options/smt_options.cpp Lines: 272 648 42.0 %
Date: 2021-03-23 Branches: 30 211 14.2 %

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
3742
template <> const options::abstractValues__option_t::type& Options::operator[](
24
    options::abstractValues__option_t) const
25
{
26
3742
  return d_holder->abstractValues;
27
}
28
template <> bool Options::wasSetByUser(options::abstractValues__option_t) const
29
{
30
  return d_holder->abstractValues__setByUser__;
31
}
32
25
template <> void Options::set(
33
    options::ackermann__option_t,
34
    const options::ackermann__option_t::type& x)
35
{
36
25
  d_holder->ackermann = x;
37
25
}
38
29325
template <> const options::ackermann__option_t::type& Options::operator[](
39
    options::ackermann__option_t) const
40
{
41
29325
  return d_holder->ackermann;
42
}
43
template <> bool Options::wasSetByUser(options::ackermann__option_t) const
44
{
45
  return d_holder->ackermann__setByUser__;
46
}
47
template <> const options::arithNlLemmaStep__option_t::type& Options::operator[](
48
    options::arithNlLemmaStep__option_t) const
49
{
50
  return d_holder->arithNlLemmaStep;
51
}
52
template <> bool Options::wasSetByUser(options::arithNlLemmaStep__option_t) const
53
{
54
  return d_holder->arithNlLemmaStep__setByUser__;
55
}
56
198211
template <> const options::arithPivotStep__option_t::type& Options::operator[](
57
    options::arithPivotStep__option_t) const
58
{
59
198211
  return d_holder->arithPivotStep;
60
}
61
template <> bool Options::wasSetByUser(options::arithPivotStep__option_t) const
62
{
63
  return d_holder->arithPivotStep__setByUser__;
64
}
65
91896
template <> const options::bitblastStep__option_t::type& Options::operator[](
66
    options::bitblastStep__option_t) const
67
{
68
91896
  return d_holder->bitblastStep;
69
}
70
template <> bool Options::wasSetByUser(options::bitblastStep__option_t) const
71
{
72
  return d_holder->bitblastStep__setByUser__;
73
}
74
template <> void Options::set(
75
    options::blockModelsMode__option_t,
76
    const options::blockModelsMode__option_t::type& x)
77
{
78
  d_holder->blockModelsMode = x;
79
}
80
6721
template <> const options::blockModelsMode__option_t::type& Options::operator[](
81
    options::blockModelsMode__option_t) const
82
{
83
6721
  return d_holder->blockModelsMode;
84
}
85
template <> bool Options::wasSetByUser(options::blockModelsMode__option_t) const
86
{
87
  return d_holder->blockModelsMode__setByUser__;
88
}
89
588
template <> const options::bvEagerAssertStep__option_t::type& Options::operator[](
90
    options::bvEagerAssertStep__option_t) const
91
{
92
588
  return d_holder->bvEagerAssertStep;
93
}
94
template <> bool Options::wasSetByUser(options::bvEagerAssertStep__option_t) const
95
{
96
  return d_holder->bvEagerAssertStep__setByUser__;
97
}
98
171639
template <> const options::bvPropagationStep__option_t::type& Options::operator[](
99
    options::bvPropagationStep__option_t) const
100
{
101
171639
  return d_holder->bvPropagationStep;
102
}
103
template <> bool Options::wasSetByUser(options::bvPropagationStep__option_t) const
104
{
105
  return d_holder->bvPropagationStep__setByUser__;
106
}
107
10409693
template <> const options::bvSatConflictStep__option_t::type& Options::operator[](
108
    options::bvSatConflictStep__option_t) const
109
{
110
10409693
  return d_holder->bvSatConflictStep;
111
}
112
template <> bool Options::wasSetByUser(options::bvSatConflictStep__option_t) const
113
{
114
  return d_holder->bvSatConflictStep__setByUser__;
115
}
116
10602716
template <> const options::bvSatPropagateStep__option_t::type& Options::operator[](
117
    options::bvSatPropagateStep__option_t) const
118
{
119
10602716
  return d_holder->bvSatPropagateStep;
120
}
121
template <> bool Options::wasSetByUser(options::bvSatPropagateStep__option_t) const
122
{
123
  return d_holder->bvSatPropagateStep__setByUser__;
124
}
125
1610
template <> const options::bvSatSimplifyStep__option_t::type& Options::operator[](
126
    options::bvSatSimplifyStep__option_t) const
127
{
128
1610
  return d_holder->bvSatSimplifyStep;
129
}
130
template <> bool Options::wasSetByUser(options::bvSatSimplifyStep__option_t) const
131
{
132
  return d_holder->bvSatSimplifyStep__setByUser__;
133
}
134
150
template <> const options::BVAndIntegerGranularity__option_t::type& Options::operator[](
135
    options::BVAndIntegerGranularity__option_t) const
136
{
137
150
  return d_holder->BVAndIntegerGranularity;
138
}
139
template <> bool Options::wasSetByUser(options::BVAndIntegerGranularity__option_t) const
140
{
141
  return d_holder->BVAndIntegerGranularity__setByUser__;
142
}
143
18
template <> const options::checkAbducts__option_t::type& Options::operator[](
144
    options::checkAbducts__option_t) const
145
{
146
18
  return d_holder->checkAbducts;
147
}
148
template <> bool Options::wasSetByUser(options::checkAbducts__option_t) const
149
{
150
  return d_holder->checkAbducts__setByUser__;
151
}
152
10
template <> const options::checkInterpols__option_t::type& Options::operator[](
153
    options::checkInterpols__option_t) const
154
{
155
10
  return d_holder->checkInterpols;
156
}
157
template <> bool Options::wasSetByUser(options::checkInterpols__option_t) const
158
{
159
  return d_holder->checkInterpols__setByUser__;
160
}
161
1090
template <> void Options::set(
162
    options::checkModels__option_t,
163
    const options::checkModels__option_t::type& x)
164
{
165
1090
  d_holder->checkModels = x;
166
1090
}
167
49290
template <> const options::checkModels__option_t::type& Options::operator[](
168
    options::checkModels__option_t) const
169
{
170
49290
  return d_holder->checkModels;
171
}
172
1
template <> bool Options::wasSetByUser(options::checkModels__option_t) const
173
{
174
1
  return d_holder->checkModels__setByUser__;
175
}
176
19
template <> void Options::set(
177
    options::checkProofs__option_t,
178
    const options::checkProofs__option_t::type& x)
179
{
180
19
  d_holder->checkProofs = x;
181
19
}
182
23294
template <> const options::checkProofs__option_t::type& Options::operator[](
183
    options::checkProofs__option_t) const
184
{
185
23294
  return d_holder->checkProofs;
186
}
187
template <> bool Options::wasSetByUser(options::checkProofs__option_t) const
188
{
189
  return d_holder->checkProofs__setByUser__;
190
}
191
166
template <> void Options::set(
192
    options::checkSynthSol__option_t,
193
    const options::checkSynthSol__option_t::type& x)
194
{
195
166
  d_holder->checkSynthSol = x;
196
166
}
197
8260
template <> const options::checkSynthSol__option_t::type& Options::operator[](
198
    options::checkSynthSol__option_t) const
199
{
200
8260
  return d_holder->checkSynthSol;
201
}
202
template <> bool Options::wasSetByUser(options::checkSynthSol__option_t) const
203
{
204
  return d_holder->checkSynthSol__setByUser__;
205
}
206
840
template <> void Options::set(
207
    options::checkUnsatCores__option_t,
208
    const options::checkUnsatCores__option_t::type& x)
209
{
210
840
  d_holder->checkUnsatCores = x;
211
840
}
212
21010
template <> const options::checkUnsatCores__option_t::type& Options::operator[](
213
    options::checkUnsatCores__option_t) const
214
{
215
21010
  return d_holder->checkUnsatCores;
216
}
217
template <> bool Options::wasSetByUser(options::checkUnsatCores__option_t) const
218
{
219
  return d_holder->checkUnsatCores__setByUser__;
220
}
221
840
template <> void Options::set(
222
    options::checkUnsatCoresNew__option_t,
223
    const options::checkUnsatCoresNew__option_t::type& x)
224
{
225
840
  d_holder->checkUnsatCoresNew = x;
226
840
}
227
29063
template <> const options::checkUnsatCoresNew__option_t::type& Options::operator[](
228
    options::checkUnsatCoresNew__option_t) const
229
{
230
29063
  return d_holder->checkUnsatCoresNew;
231
}
232
template <> bool Options::wasSetByUser(options::checkUnsatCoresNew__option_t) const
233
{
234
  return d_holder->checkUnsatCoresNew__setByUser__;
235
}
236
1096827
template <> const options::cnfStep__option_t::type& Options::operator[](
237
    options::cnfStep__option_t) const
238
{
239
1096827
  return d_holder->cnfStep;
240
}
241
template <> bool Options::wasSetByUser(options::cnfStep__option_t) const
242
{
243
  return d_holder->cnfStep__setByUser__;
244
}
245
template <> void Options::set(
246
    options::debugCheckModels__option_t,
247
    const options::debugCheckModels__option_t::type& x)
248
{
249
  d_holder->debugCheckModels = x;
250
}
251
11846
template <> const options::debugCheckModels__option_t::type& Options::operator[](
252
    options::debugCheckModels__option_t) const
253
{
254
11846
  return d_holder->debugCheckModels;
255
}
256
template <> bool Options::wasSetByUser(options::debugCheckModels__option_t) const
257
{
258
  return d_holder->debugCheckModels__setByUser__;
259
}
260
2510964
template <> const options::decisionStep__option_t::type& Options::operator[](
261
    options::decisionStep__option_t) const
262
{
263
2510964
  return d_holder->decisionStep;
264
}
265
template <> bool Options::wasSetByUser(options::decisionStep__option_t) const
266
{
267
  return d_holder->decisionStep__setByUser__;
268
}
269
template <> const options::diagnosticChannelName__option_t::type& Options::operator[](
270
    options::diagnosticChannelName__option_t) const
271
{
272
  return d_holder->diagnosticChannelName;
273
}
274
9623
template <> bool Options::wasSetByUser(options::diagnosticChannelName__option_t) const
275
{
276
9623
  return d_holder->diagnosticChannelName__setByUser__;
277
}
278
283135
template <> const options::dumpInstantiations__option_t::type& Options::operator[](
279
    options::dumpInstantiations__option_t) const
280
{
281
283135
  return d_holder->dumpInstantiations;
282
}
283
template <> bool Options::wasSetByUser(options::dumpInstantiations__option_t) const
284
{
285
  return d_holder->dumpInstantiations__setByUser__;
286
}
287
291035
template <> const options::dumpModels__option_t::type& Options::operator[](
288
    options::dumpModels__option_t) const
289
{
290
291035
  return d_holder->dumpModels;
291
}
292
template <> bool Options::wasSetByUser(options::dumpModels__option_t) const
293
{
294
  return d_holder->dumpModels__setByUser__;
295
}
296
291155
template <> const options::dumpProofs__option_t::type& Options::operator[](
297
    options::dumpProofs__option_t) const
298
{
299
291155
  return d_holder->dumpProofs;
300
}
301
template <> bool Options::wasSetByUser(options::dumpProofs__option_t) const
302
{
303
  return d_holder->dumpProofs__setByUser__;
304
}
305
template <> const options::dumpToFileName__option_t::type& Options::operator[](
306
    options::dumpToFileName__option_t) const
307
{
308
  return d_holder->dumpToFileName;
309
}
310
9623
template <> bool Options::wasSetByUser(options::dumpToFileName__option_t) const
311
{
312
9623
  return d_holder->dumpToFileName__setByUser__;
313
}
314
4
template <> void Options::set(
315
    options::dumpUnsatCores__option_t,
316
    const options::dumpUnsatCores__option_t::type& x)
317
{
318
4
  d_holder->dumpUnsatCores = x;
319
4
}
320
291304
template <> const options::dumpUnsatCores__option_t::type& Options::operator[](
321
    options::dumpUnsatCores__option_t) const
322
{
323
291304
  return d_holder->dumpUnsatCores;
324
}
325
template <> bool Options::wasSetByUser(options::dumpUnsatCores__option_t) const
326
{
327
  return d_holder->dumpUnsatCores__setByUser__;
328
}
329
292144
template <> const options::dumpUnsatCoresFull__option_t::type& Options::operator[](
330
    options::dumpUnsatCoresFull__option_t) const
331
{
332
292144
  return d_holder->dumpUnsatCoresFull;
333
}
334
template <> bool Options::wasSetByUser(options::dumpUnsatCoresFull__option_t) const
335
{
336
  return d_holder->dumpUnsatCoresFull__setByUser__;
337
}
338
3
template <> const options::dumpModeString__option_t::type& Options::operator[](
339
    options::dumpModeString__option_t) const
340
{
341
3
  return d_holder->dumpModeString;
342
}
343
9624
template <> bool Options::wasSetByUser(options::dumpModeString__option_t) const
344
{
345
9624
  return d_holder->dumpModeString__setByUser__;
346
}
347
1
template <> void Options::set(
348
    options::earlyIteRemoval__option_t,
349
    const options::earlyIteRemoval__option_t::type& x)
350
{
351
1
  d_holder->earlyIteRemoval = x;
352
1
}
353
11325
template <> const options::earlyIteRemoval__option_t::type& Options::operator[](
354
    options::earlyIteRemoval__option_t) const
355
{
356
11325
  return d_holder->earlyIteRemoval;
357
}
358
1
template <> bool Options::wasSetByUser(options::earlyIteRemoval__option_t) const
359
{
360
1
  return d_holder->earlyIteRemoval__setByUser__;
361
}
362
template <> const options::expandDefinitions__option_t::type& Options::operator[](
363
    options::expandDefinitions__option_t) const
364
{
365
  return d_holder->expandDefinitions;
366
}
367
template <> bool Options::wasSetByUser(options::expandDefinitions__option_t) const
368
{
369
  return d_holder->expandDefinitions__setByUser__;
370
}
371
template <> void Options::set(
372
    options::extRewPrep__option_t,
373
    const options::extRewPrep__option_t::type& x)
374
{
375
  d_holder->extRewPrep = x;
376
}
377
11327
template <> const options::extRewPrep__option_t::type& Options::operator[](
378
    options::extRewPrep__option_t) const
379
{
380
11327
  return d_holder->extRewPrep;
381
}
382
template <> bool Options::wasSetByUser(options::extRewPrep__option_t) const
383
{
384
  return d_holder->extRewPrep__setByUser__;
385
}
386
template <> void Options::set(
387
    options::extRewPrepAgg__option_t,
388
    const options::extRewPrepAgg__option_t::type& x)
389
{
390
  d_holder->extRewPrepAgg = x;
391
}
392
22
template <> const options::extRewPrepAgg__option_t::type& Options::operator[](
393
    options::extRewPrepAgg__option_t) const
394
{
395
22
  return d_holder->extRewPrepAgg;
396
}
397
template <> bool Options::wasSetByUser(options::extRewPrepAgg__option_t) const
398
{
399
  return d_holder->extRewPrepAgg__setByUser__;
400
}
401
23
template <> const options::forceNoLimitCpuWhileDump__option_t::type& Options::operator[](
402
    options::forceNoLimitCpuWhileDump__option_t) const
403
{
404
23
  return d_holder->forceNoLimitCpuWhileDump;
405
}
406
template <> bool Options::wasSetByUser(options::forceNoLimitCpuWhileDump__option_t) const
407
{
408
  return d_holder->forceNoLimitCpuWhileDump__setByUser__;
409
}
410
11327
template <> const options::foreignTheoryRewrite__option_t::type& Options::operator[](
411
    options::foreignTheoryRewrite__option_t) const
412
{
413
11327
  return d_holder->foreignTheoryRewrite;
414
}
415
template <> bool Options::wasSetByUser(options::foreignTheoryRewrite__option_t) const
416
{
417
  return d_holder->foreignTheoryRewrite__setByUser__;
418
}
419
43
template <> const options::iandMode__option_t::type& Options::operator[](
420
    options::iandMode__option_t) const
421
{
422
43
  return d_holder->iandMode;
423
}
424
template <> bool Options::wasSetByUser(options::iandMode__option_t) const
425
{
426
  return d_holder->iandMode__setByUser__;
427
}
428
template <> void Options::set(
429
    options::incrementalSolving__option_t,
430
    const options::incrementalSolving__option_t::type& x)
431
{
432
  d_holder->incrementalSolving = x;
433
}
434
3964318
template <> const options::incrementalSolving__option_t::type& Options::operator[](
435
    options::incrementalSolving__option_t) const
436
{
437
3964318
  return d_holder->incrementalSolving;
438
}
439
5459
template <> bool Options::wasSetByUser(options::incrementalSolving__option_t) const
440
{
441
5459
  return d_holder->incrementalSolving__setByUser__;
442
}
443
8
template <> void Options::set(
444
    options::interactiveMode__option_t,
445
    const options::interactiveMode__option_t::type& x)
446
{
447
8
  d_holder->interactiveMode = x;
448
8
}
449
template <> const options::interactiveMode__option_t::type& Options::operator[](
450
    options::interactiveMode__option_t) const
451
{
452
  return d_holder->interactiveMode;
453
}
454
template <> bool Options::wasSetByUser(options::interactiveMode__option_t) const
455
{
456
  return d_holder->interactiveMode__setByUser__;
457
}
458
template <> void Options::set(
459
    options::doITESimp__option_t,
460
    const options::doITESimp__option_t::type& x)
461
{
462
  d_holder->doITESimp = x;
463
}
464
21527
template <> const options::doITESimp__option_t::type& Options::operator[](
465
    options::doITESimp__option_t) const
466
{
467
21527
  return d_holder->doITESimp;
468
}
469
template <> bool Options::wasSetByUser(options::doITESimp__option_t) const
470
{
471
  return d_holder->doITESimp__setByUser__;
472
}
473
259701
template <> const options::lemmaStep__option_t::type& Options::operator[](
474
    options::lemmaStep__option_t) const
475
{
476
259701
  return d_holder->lemmaStep;
477
}
478
template <> bool Options::wasSetByUser(options::lemmaStep__option_t) const
479
{
480
  return d_holder->lemmaStep__setByUser__;
481
}
482
template <> void Options::set(
483
    options::modelCoresMode__option_t,
484
    const options::modelCoresMode__option_t::type& x)
485
{
486
  d_holder->modelCoresMode = x;
487
}
488
6723
template <> const options::modelCoresMode__option_t::type& Options::operator[](
489
    options::modelCoresMode__option_t) const
490
{
491
6723
  return d_holder->modelCoresMode;
492
}
493
template <> bool Options::wasSetByUser(options::modelCoresMode__option_t) const
494
{
495
  return d_holder->modelCoresMode__setByUser__;
496
}
497
45
template <> const options::modelUninterpPrint__option_t::type& Options::operator[](
498
    options::modelUninterpPrint__option_t) const
499
{
500
45
  return d_holder->modelUninterpPrint;
501
}
502
template <> bool Options::wasSetByUser(options::modelUninterpPrint__option_t) const
503
{
504
  return d_holder->modelUninterpPrint__setByUser__;
505
}
506
35
template <> const options::modelWitnessValue__option_t::type& Options::operator[](
507
    options::modelWitnessValue__option_t) const
508
{
509
35
  return d_holder->modelWitnessValue;
510
}
511
template <> bool Options::wasSetByUser(options::modelWitnessValue__option_t) const
512
{
513
  return d_holder->modelWitnessValue__setByUser__;
514
}
515
template <> const options::newSkolemStep__option_t::type& Options::operator[](
516
    options::newSkolemStep__option_t) const
517
{
518
  return d_holder->newSkolemStep;
519
}
520
template <> bool Options::wasSetByUser(options::newSkolemStep__option_t) const
521
{
522
  return d_holder->newSkolemStep__setByUser__;
523
}
524
template <> void Options::set(
525
    options::doITESimpOnRepeat__option_t,
526
    const options::doITESimpOnRepeat__option_t::type& x)
527
{
528
  d_holder->doITESimpOnRepeat = x;
529
}
530
template <> const options::doITESimpOnRepeat__option_t::type& Options::operator[](
531
    options::doITESimpOnRepeat__option_t) const
532
{
533
  return d_holder->doITESimpOnRepeat;
534
}
535
template <> bool Options::wasSetByUser(options::doITESimpOnRepeat__option_t) const
536
{
537
  return d_holder->doITESimpOnRepeat__setByUser__;
538
}
539
template <> const options::parseStep__option_t::type& Options::operator[](
540
    options::parseStep__option_t) const
541
{
542
  return d_holder->parseStep;
543
}
544
template <> bool Options::wasSetByUser(options::parseStep__option_t) const
545
{
546
  return d_holder->parseStep__setByUser__;
547
}
548
8599782
template <> const options::preprocessStep__option_t::type& Options::operator[](
549
    options::preprocessStep__option_t) const
550
{
551
8599782
  return d_holder->preprocessStep;
552
}
553
template <> bool Options::wasSetByUser(options::preprocessStep__option_t) const
554
{
555
  return d_holder->preprocessStep__setByUser__;
556
}
557
24139
template <> const options::produceAbducts__option_t::type& Options::operator[](
558
    options::produceAbducts__option_t) const
559
{
560
24139
  return d_holder->produceAbducts;
561
}
562
template <> bool Options::wasSetByUser(options::produceAbducts__option_t) const
563
{
564
  return d_holder->produceAbducts__setByUser__;
565
}
566
2240
template <> void Options::set(
567
    options::produceAssertions__option_t,
568
    const options::produceAssertions__option_t::type& x)
569
{
570
2240
  d_holder->produceAssertions = x;
571
2240
}
572
12349
template <> const options::produceAssertions__option_t::type& Options::operator[](
573
    options::produceAssertions__option_t) const
574
{
575
12349
  return d_holder->produceAssertions;
576
}
577
template <> bool Options::wasSetByUser(options::produceAssertions__option_t) const
578
{
579
  return d_holder->produceAssertions__setByUser__;
580
}
581
1100
template <> void Options::set(
582
    options::produceAssignments__option_t,
583
    const options::produceAssignments__option_t::type& x)
584
{
585
1100
  d_holder->produceAssignments = x;
586
1100
}
587
15812
template <> const options::produceAssignments__option_t::type& Options::operator[](
588
    options::produceAssignments__option_t) const
589
{
590
15812
  return d_holder->produceAssignments;
591
}
592
1
template <> bool Options::wasSetByUser(options::produceAssignments__option_t) const
593
{
594
1
  return d_holder->produceAssignments__setByUser__;
595
}
596
22232
template <> const options::produceInterpols__option_t::type& Options::operator[](
597
    options::produceInterpols__option_t) const
598
{
599
22232
  return d_holder->produceInterpols;
600
}
601
template <> bool Options::wasSetByUser(options::produceInterpols__option_t) const
602
{
603
  return d_holder->produceInterpols__setByUser__;
604
}
605
1557
template <> void Options::set(
606
    options::produceModels__option_t,
607
    const options::produceModels__option_t::type& x)
608
{
609
1557
  d_holder->produceModels = x;
610
1557
}
611
59536
template <> const options::produceModels__option_t::type& Options::operator[](
612
    options::produceModels__option_t) const
613
{
614
59536
  return d_holder->produceModels;
615
}
616
2
template <> bool Options::wasSetByUser(options::produceModels__option_t) const
617
{
618
2
  return d_holder->produceModels__setByUser__;
619
}
620
1838
template <> void Options::set(
621
    options::produceProofs__option_t,
622
    const options::produceProofs__option_t::type& x)
623
{
624
1838
  d_holder->produceProofs = x;
625
1838
}
626
32658236
template <> const options::produceProofs__option_t::type& Options::operator[](
627
    options::produceProofs__option_t) const
628
{
629
32658236
  return d_holder->produceProofs;
630
}
631
template <> bool Options::wasSetByUser(options::produceProofs__option_t) const
632
{
633
  return d_holder->produceProofs__setByUser__;
634
}
635
8182
template <> const options::unsatAssumptions__option_t::type& Options::operator[](
636
    options::unsatAssumptions__option_t) const
637
{
638
8182
  return d_holder->unsatAssumptions;
639
}
640
template <> bool Options::wasSetByUser(options::unsatAssumptions__option_t) const
641
{
642
  return d_holder->unsatAssumptions__setByUser__;
643
}
644
968
template <> void Options::set(
645
    options::unsatCores__option_t,
646
    const options::unsatCores__option_t::type& x)
647
{
648
968
  d_holder->unsatCores = x;
649
968
}
650
31137844
template <> const options::unsatCores__option_t::type& Options::operator[](
651
    options::unsatCores__option_t) const
652
{
653
31137844
  return d_holder->unsatCores;
654
}
655
template <> bool Options::wasSetByUser(options::unsatCores__option_t) const
656
{
657
  return d_holder->unsatCores__setByUser__;
658
}
659
219601
template <> const options::quantifierStep__option_t::type& Options::operator[](
660
    options::quantifierStep__option_t) const
661
{
662
219601
  return d_holder->quantifierStep;
663
}
664
template <> bool Options::wasSetByUser(options::quantifierStep__option_t) const
665
{
666
  return d_holder->quantifierStep__setByUser__;
667
}
668
template <> const options::regularChannelName__option_t::type& Options::operator[](
669
    options::regularChannelName__option_t) const
670
{
671
  return d_holder->regularChannelName;
672
}
673
9623
template <> bool Options::wasSetByUser(options::regularChannelName__option_t) const
674
{
675
9623
  return d_holder->regularChannelName__setByUser__;
676
}
677
8997
template <> void Options::set(
678
    options::repeatSimp__option_t,
679
    const options::repeatSimp__option_t::type& x)
680
{
681
8997
  d_holder->repeatSimp = x;
682
8997
}
683
23853
template <> const options::repeatSimp__option_t::type& Options::operator[](
684
    options::repeatSimp__option_t) const
685
{
686
23853
  return d_holder->repeatSimp;
687
}
688
8999
template <> bool Options::wasSetByUser(options::repeatSimp__option_t) const
689
{
690
8999
  return d_holder->repeatSimp__setByUser__;
691
}
692
2312
template <> const options::restartStep__option_t::type& Options::operator[](
693
    options::restartStep__option_t) const
694
{
695
2312
  return d_holder->restartStep;
696
}
697
template <> bool Options::wasSetByUser(options::restartStep__option_t) const
698
{
699
  return d_holder->restartStep__setByUser__;
700
}
701
72483949
template <> const options::rewriteStep__option_t::type& Options::operator[](
702
    options::rewriteStep__option_t) const
703
{
704
72483949
  return d_holder->rewriteStep;
705
}
706
template <> bool Options::wasSetByUser(options::rewriteStep__option_t) const
707
{
708
  return d_holder->rewriteStep__setByUser__;
709
}
710
8999
template <> const options::perCallResourceLimit__option_t::type& Options::operator[](
711
    options::perCallResourceLimit__option_t) const
712
{
713
8999
  return d_holder->perCallResourceLimit;
714
}
715
template <> bool Options::wasSetByUser(options::perCallResourceLimit__option_t) const
716
{
717
  return d_holder->perCallResourceLimit__setByUser__;
718
}
719
8999
template <> const options::cumulativeResourceLimit__option_t::type& Options::operator[](
720
    options::cumulativeResourceLimit__option_t) const
721
{
722
8999
  return d_holder->cumulativeResourceLimit;
723
}
724
template <> bool Options::wasSetByUser(options::cumulativeResourceLimit__option_t) const
725
{
726
  return d_holder->cumulativeResourceLimit__setByUser__;
727
}
728
2580164
template <> const options::satConflictStep__option_t::type& Options::operator[](
729
    options::satConflictStep__option_t) const
730
{
731
2580164
  return d_holder->satConflictStep;
732
}
733
template <> bool Options::wasSetByUser(options::satConflictStep__option_t) const
734
{
735
  return d_holder->satConflictStep__setByUser__;
736
}
737
template <> void Options::set(
738
    options::compressItes__option_t,
739
    const options::compressItes__option_t::type& x)
740
{
741
  d_holder->compressItes = x;
742
}
743
1
template <> const options::compressItes__option_t::type& Options::operator[](
744
    options::compressItes__option_t) const
745
{
746
1
  return d_holder->compressItes;
747
}
748
template <> bool Options::wasSetByUser(options::compressItes__option_t) const
749
{
750
  return d_holder->compressItes__setByUser__;
751
}
752
1
template <> const options::zombieHuntThreshold__option_t::type& Options::operator[](
753
    options::zombieHuntThreshold__option_t) const
754
{
755
1
  return d_holder->zombieHuntThreshold;
756
}
757
template <> bool Options::wasSetByUser(options::zombieHuntThreshold__option_t) const
758
{
759
  return d_holder->zombieHuntThreshold__setByUser__;
760
}
761
8999
template <> void Options::set(
762
    options::simplifyWithCareEnabled__option_t,
763
    const options::simplifyWithCareEnabled__option_t::type& x)
764
{
765
8999
  d_holder->simplifyWithCareEnabled = x;
766
8999
}
767
1
template <> const options::simplifyWithCareEnabled__option_t::type& Options::operator[](
768
    options::simplifyWithCareEnabled__option_t) const
769
{
770
1
  return d_holder->simplifyWithCareEnabled;
771
}
772
8999
template <> bool Options::wasSetByUser(options::simplifyWithCareEnabled__option_t) const
773
{
774
8999
  return d_holder->simplifyWithCareEnabled__setByUser__;
775
}
776
8001
template <> void Options::set(
777
    options::simplificationMode__option_t,
778
    const options::simplificationMode__option_t::type& x)
779
{
780
8001
  d_holder->simplificationMode = x;
781
8001
}
782
14182
template <> const options::simplificationMode__option_t::type& Options::operator[](
783
    options::simplificationMode__option_t) const
784
{
785
14182
  return d_holder->simplificationMode;
786
}
787
8027
template <> bool Options::wasSetByUser(options::simplificationMode__option_t) const
788
{
789
8027
  return d_holder->simplificationMode__setByUser__;
790
}
791
template <> void Options::set(
792
    options::solveBVAsInt__option_t,
793
    const options::solveBVAsInt__option_t::type& x)
794
{
795
  d_holder->solveBVAsInt = x;
796
}
797
29389
template <> const options::solveBVAsInt__option_t::type& Options::operator[](
798
    options::solveBVAsInt__option_t) const
799
{
800
29389
  return d_holder->solveBVAsInt;
801
}
802
template <> bool Options::wasSetByUser(options::solveBVAsInt__option_t) const
803
{
804
  return d_holder->solveBVAsInt__setByUser__;
805
}
806
33277
template <> const options::solveIntAsBV__option_t::type& Options::operator[](
807
    options::solveIntAsBV__option_t) const
808
{
809
33277
  return d_holder->solveIntAsBV;
810
}
811
template <> bool Options::wasSetByUser(options::solveIntAsBV__option_t) const
812
{
813
  return d_holder->solveIntAsBV__setByUser__;
814
}
815
23730
template <> const options::solveRealAsInt__option_t::type& Options::operator[](
816
    options::solveRealAsInt__option_t) const
817
{
818
23730
  return d_holder->solveRealAsInt;
819
}
820
template <> bool Options::wasSetByUser(options::solveRealAsInt__option_t) const
821
{
822
  return d_holder->solveRealAsInt__setByUser__;
823
}
824
1529
template <> void Options::set(
825
    options::sortInference__option_t,
826
    const options::sortInference__option_t::type& x)
827
{
828
1529
  d_holder->sortInference = x;
829
1529
}
830
31089
template <> const options::sortInference__option_t::type& Options::operator[](
831
    options::sortInference__option_t) const
832
{
833
31089
  return d_holder->sortInference;
834
}
835
template <> bool Options::wasSetByUser(options::sortInference__option_t) const
836
{
837
  return d_holder->sortInference__setByUser__;
838
}
839
11325
template <> const options::doStaticLearning__option_t::type& Options::operator[](
840
    options::doStaticLearning__option_t) const
841
{
842
11325
  return d_holder->doStaticLearning;
843
}
844
template <> bool Options::wasSetByUser(options::doStaticLearning__option_t) const
845
{
846
  return d_holder->doStaticLearning__setByUser__;
847
}
848
template <> void Options::set(
849
    options::sygusOut__option_t,
850
    const options::sygusOut__option_t::type& x)
851
{
852
  d_holder->sygusOut = x;
853
}
854
1347
template <> const options::sygusOut__option_t::type& Options::operator[](
855
    options::sygusOut__option_t) const
856
{
857
1347
  return d_holder->sygusOut;
858
}
859
template <> bool Options::wasSetByUser(options::sygusOut__option_t) const
860
{
861
  return d_holder->sygusOut__setByUser__;
862
}
863
template <> const options::sygusPrintCallbacks__option_t::type& Options::operator[](
864
    options::sygusPrintCallbacks__option_t) const
865
{
866
  return d_holder->sygusPrintCallbacks;
867
}
868
template <> bool Options::wasSetByUser(options::sygusPrintCallbacks__option_t) const
869
{
870
  return d_holder->sygusPrintCallbacks__setByUser__;
871
}
872
5308768
template <> const options::theoryCheckStep__option_t::type& Options::operator[](
873
    options::theoryCheckStep__option_t) const
874
{
875
5308768
  return d_holder->theoryCheckStep;
876
}
877
template <> bool Options::wasSetByUser(options::theoryCheckStep__option_t) const
878
{
879
  return d_holder->theoryCheckStep__setByUser__;
880
}
881
9006
template <> const options::perCallMillisecondLimit__option_t::type& Options::operator[](
882
    options::perCallMillisecondLimit__option_t) const
883
{
884
9006
  return d_holder->perCallMillisecondLimit;
885
}
886
template <> bool Options::wasSetByUser(options::perCallMillisecondLimit__option_t) const
887
{
888
  return d_holder->perCallMillisecondLimit__setByUser__;
889
}
890
5460
template <> const options::cumulativeMillisecondLimit__option_t::type& Options::operator[](
891
    options::cumulativeMillisecondLimit__option_t) const
892
{
893
5460
  return d_holder->cumulativeMillisecondLimit;
894
}
895
template <> bool Options::wasSetByUser(options::cumulativeMillisecondLimit__option_t) const
896
{
897
  return d_holder->cumulativeMillisecondLimit__setByUser__;
898
}
899
5676
template <> void Options::set(
900
    options::unconstrainedSimp__option_t,
901
    const options::unconstrainedSimp__option_t::type& x)
902
{
903
5676
  d_holder->unconstrainedSimp = x;
904
5676
}
905
25361
template <> const options::unconstrainedSimp__option_t::type& Options::operator[](
906
    options::unconstrainedSimp__option_t) const
907
{
908
25361
  return d_holder->unconstrainedSimp;
909
}
910
14746
template <> bool Options::wasSetByUser(options::unconstrainedSimp__option_t) const
911
{
912
14746
  return d_holder->unconstrainedSimp__setByUser__;
913
}
914
915
916
namespace options {
917
918
thread_local struct abstractValues__option_t abstractValues;
919
thread_local struct ackermann__option_t ackermann;
920
thread_local struct arithNlLemmaStep__option_t arithNlLemmaStep;
921
thread_local struct arithPivotStep__option_t arithPivotStep;
922
thread_local struct bitblastStep__option_t bitblastStep;
923
thread_local struct blockModelsMode__option_t blockModelsMode;
924
thread_local struct bvEagerAssertStep__option_t bvEagerAssertStep;
925
thread_local struct bvPropagationStep__option_t bvPropagationStep;
926
thread_local struct bvSatConflictStep__option_t bvSatConflictStep;
927
thread_local struct bvSatPropagateStep__option_t bvSatPropagateStep;
928
thread_local struct bvSatSimplifyStep__option_t bvSatSimplifyStep;
929
thread_local struct BVAndIntegerGranularity__option_t BVAndIntegerGranularity;
930
thread_local struct checkAbducts__option_t checkAbducts;
931
thread_local struct checkInterpols__option_t checkInterpols;
932
thread_local struct checkModels__option_t checkModels;
933
thread_local struct checkProofs__option_t checkProofs;
934
thread_local struct checkSynthSol__option_t checkSynthSol;
935
thread_local struct checkUnsatCores__option_t checkUnsatCores;
936
thread_local struct checkUnsatCoresNew__option_t checkUnsatCoresNew;
937
thread_local struct cnfStep__option_t cnfStep;
938
thread_local struct debugCheckModels__option_t debugCheckModels;
939
thread_local struct decisionStep__option_t decisionStep;
940
thread_local struct diagnosticChannelName__option_t diagnosticChannelName;
941
thread_local struct dumpInstantiations__option_t dumpInstantiations;
942
thread_local struct dumpModels__option_t dumpModels;
943
thread_local struct dumpProofs__option_t dumpProofs;
944
thread_local struct dumpToFileName__option_t dumpToFileName;
945
thread_local struct dumpUnsatCores__option_t dumpUnsatCores;
946
thread_local struct dumpUnsatCoresFull__option_t dumpUnsatCoresFull;
947
thread_local struct dumpModeString__option_t dumpModeString;
948
thread_local struct earlyIteRemoval__option_t earlyIteRemoval;
949
thread_local struct expandDefinitions__option_t expandDefinitions;
950
thread_local struct extRewPrep__option_t extRewPrep;
951
thread_local struct extRewPrepAgg__option_t extRewPrepAgg;
952
thread_local struct forceNoLimitCpuWhileDump__option_t forceNoLimitCpuWhileDump;
953
thread_local struct foreignTheoryRewrite__option_t foreignTheoryRewrite;
954
thread_local struct iandMode__option_t iandMode;
955
thread_local struct incrementalSolving__option_t incrementalSolving;
956
thread_local struct interactiveMode__option_t interactiveMode;
957
thread_local struct doITESimp__option_t doITESimp;
958
thread_local struct lemmaStep__option_t lemmaStep;
959
thread_local struct modelCoresMode__option_t modelCoresMode;
960
thread_local struct modelUninterpPrint__option_t modelUninterpPrint;
961
thread_local struct modelWitnessValue__option_t modelWitnessValue;
962
thread_local struct newSkolemStep__option_t newSkolemStep;
963
thread_local struct doITESimpOnRepeat__option_t doITESimpOnRepeat;
964
thread_local struct parseStep__option_t parseStep;
965
thread_local struct preprocessStep__option_t preprocessStep;
966
thread_local struct produceAbducts__option_t produceAbducts;
967
thread_local struct produceAssertions__option_t produceAssertions;
968
thread_local struct produceAssignments__option_t produceAssignments;
969
thread_local struct produceInterpols__option_t produceInterpols;
970
thread_local struct produceModels__option_t produceModels;
971
thread_local struct produceProofs__option_t produceProofs;
972
thread_local struct unsatAssumptions__option_t unsatAssumptions;
973
thread_local struct unsatCores__option_t unsatCores;
974
thread_local struct quantifierStep__option_t quantifierStep;
975
thread_local struct regularChannelName__option_t regularChannelName;
976
thread_local struct repeatSimp__option_t repeatSimp;
977
thread_local struct restartStep__option_t restartStep;
978
thread_local struct rewriteStep__option_t rewriteStep;
979
thread_local struct perCallResourceLimit__option_t perCallResourceLimit;
980
thread_local struct cumulativeResourceLimit__option_t cumulativeResourceLimit;
981
thread_local struct satConflictStep__option_t satConflictStep;
982
thread_local struct compressItes__option_t compressItes;
983
thread_local struct zombieHuntThreshold__option_t zombieHuntThreshold;
984
thread_local struct simplifyWithCareEnabled__option_t simplifyWithCareEnabled;
985
thread_local struct simplificationMode__option_t simplificationMode;
986
thread_local struct solveBVAsInt__option_t solveBVAsInt;
987
thread_local struct solveIntAsBV__option_t solveIntAsBV;
988
thread_local struct solveRealAsInt__option_t solveRealAsInt;
989
thread_local struct sortInference__option_t sortInference;
990
thread_local struct doStaticLearning__option_t doStaticLearning;
991
thread_local struct sygusOut__option_t sygusOut;
992
thread_local struct sygusPrintCallbacks__option_t sygusPrintCallbacks;
993
thread_local struct theoryCheckStep__option_t theoryCheckStep;
994
thread_local struct perCallMillisecondLimit__option_t perCallMillisecondLimit;
995
thread_local struct cumulativeMillisecondLimit__option_t cumulativeMillisecondLimit;
996
thread_local struct unconstrainedSimp__option_t unconstrainedSimp;
997
998
999
std::ostream&
1000
operator<<(std::ostream& os, BlockModelsMode mode)
1001
{
1002
  os << "BlockModelsMode::";
1003
  switch(mode) {
1004
    case BlockModelsMode::LITERALS:
1005
      os << "LITERALS";
1006
      break;
1007
    case BlockModelsMode::VALUES:
1008
      os << "VALUES";
1009
      break;
1010
    case BlockModelsMode::NONE:
1011
      os << "NONE";
1012
      break;
1013
    default:
1014
        Unreachable();
1015
  }
1016
  return os;
1017
}
1018
1019
BlockModelsMode
1020
19
stringToBlockModelsMode(const std::string& option, const std::string& optarg)
1021
{
1022
19
  if (optarg == "literals")
1023
  {
1024
17
    return BlockModelsMode::LITERALS;
1025
  }
1026
2
  else if (optarg == "values")
1027
  {
1028
2
    return BlockModelsMode::VALUES;
1029
  }
1030
  else if (optarg == "none")
1031
  {
1032
    return BlockModelsMode::NONE;
1033
  }
1034
  else if (optarg == "help")
1035
  {
1036
    puts("Blocking models modes.\n"
1037
         "Available modes for --block-models are:\n"
1038
         "+ literals\n"
1039
         "  Block models based on the SAT skeleton.\n"
1040
         "+ values\n"
1041
         "  Block models based on the concrete model values for the free variables.\n"
1042
         "+ none (default)\n"
1043
         "  Do not block models.\n");
1044
    exit(1);
1045
  }
1046
  else
1047
  {
1048
    throw OptionException(std::string("unknown option for --block-models: `") +
1049
                          optarg + "'.  Try --block-models=help.");
1050
  }
1051
}
1052
1053
std::ostream&
1054
operator<<(std::ostream& os, IandMode mode)
1055
{
1056
  os << "IandMode::";
1057
  switch(mode) {
1058
    case IandMode::VALUE:
1059
      os << "VALUE";
1060
      break;
1061
    case IandMode::BITWISE:
1062
      os << "BITWISE";
1063
      break;
1064
    case IandMode::SUM:
1065
      os << "SUM";
1066
      break;
1067
    default:
1068
        Unreachable();
1069
  }
1070
  return os;
1071
}
1072
1073
IandMode
1074
62
stringToIandMode(const std::string& option, const std::string& optarg)
1075
{
1076
62
  if (optarg == "value")
1077
  {
1078
16
    return IandMode::VALUE;
1079
  }
1080
46
  else if (optarg == "bitwise")
1081
  {
1082
30
    return IandMode::BITWISE;
1083
  }
1084
16
  else if (optarg == "sum")
1085
  {
1086
16
    return IandMode::SUM;
1087
  }
1088
  else if (optarg == "help")
1089
  {
1090
    puts("Refinement modes for integer AND\n"
1091
         "Available modes for --iand-mode are:\n"
1092
         "+ value (default)\n"
1093
         "  value-based refinement\n"
1094
         "+ bitwise\n"
1095
         "  use bitwise comparisons on binary representation of integer for refinement\n"
1096
         "  (experimental)\n"
1097
         "+ sum\n"
1098
         "  use sum to represent integer AND in refinement\n");
1099
    exit(1);
1100
  }
1101
  else
1102
  {
1103
    throw OptionException(std::string("unknown option for --iand-mode: `") +
1104
                          optarg + "'.  Try --iand-mode=help.");
1105
  }
1106
}
1107
1108
std::ostream&
1109
operator<<(std::ostream& os, ModelCoresMode mode)
1110
{
1111
  os << "ModelCoresMode::";
1112
  switch(mode) {
1113
    case ModelCoresMode::NON_IMPLIED:
1114
      os << "NON_IMPLIED";
1115
      break;
1116
    case ModelCoresMode::SIMPLE:
1117
      os << "SIMPLE";
1118
      break;
1119
    case ModelCoresMode::NONE:
1120
      os << "NONE";
1121
      break;
1122
    default:
1123
        Unreachable();
1124
  }
1125
  return os;
1126
}
1127
1128
ModelCoresMode
1129
6
stringToModelCoresMode(const std::string& option, const std::string& optarg)
1130
{
1131
6
  if (optarg == "non-implied")
1132
  {
1133
4
    return ModelCoresMode::NON_IMPLIED;
1134
  }
1135
2
  else if (optarg == "simple")
1136
  {
1137
2
    return ModelCoresMode::SIMPLE;
1138
  }
1139
  else if (optarg == "none")
1140
  {
1141
    return ModelCoresMode::NONE;
1142
  }
1143
  else if (optarg == "help")
1144
  {
1145
    puts("Model cores modes.\n"
1146
         "Available modes for --model-cores are:\n"
1147
         "+ non-implied\n"
1148
         "  Only include a subset of variables whose values, in addition to the values of\n"
1149
         "  variables whose values are implied, are sufficient to show the input formula\n"
1150
         "  is satisfied by the given model.\n"
1151
         "+ simple\n"
1152
         "  Only include a subset of variables whose values are sufficient to show the\n"
1153
         "  input formula is satisfied by the given model.\n"
1154
         "+ none (default)\n"
1155
         "  Do not compute model cores.\n");
1156
    exit(1);
1157
  }
1158
  else
1159
  {
1160
    throw OptionException(std::string("unknown option for --model-cores: `") +
1161
                          optarg + "'.  Try --model-cores=help.");
1162
  }
1163
}
1164
1165
std::ostream&
1166
operator<<(std::ostream& os, ModelUninterpPrintMode mode)
1167
{
1168
  os << "ModelUninterpPrintMode::";
1169
  switch(mode) {
1170
    case ModelUninterpPrintMode::DtEnum:
1171
      os << "DtEnum";
1172
      break;
1173
    case ModelUninterpPrintMode::DeclFun:
1174
      os << "DeclFun";
1175
      break;
1176
    case ModelUninterpPrintMode::None:
1177
      os << "None";
1178
      break;
1179
    case ModelUninterpPrintMode::DeclSortAndFun:
1180
      os << "DeclSortAndFun";
1181
      break;
1182
    default:
1183
        Unreachable();
1184
  }
1185
  return os;
1186
}
1187
1188
ModelUninterpPrintMode
1189
1
stringToModelUninterpPrintMode(const std::string& option, const std::string& optarg)
1190
{
1191
1
  if (optarg == "dtenum")
1192
  {
1193
    return ModelUninterpPrintMode::DtEnum;
1194
  }
1195
1
  else if (optarg == "decl-fun")
1196
  {
1197
1
    return ModelUninterpPrintMode::DeclFun;
1198
  }
1199
  else if (optarg == "none")
1200
  {
1201
    return ModelUninterpPrintMode::None;
1202
  }
1203
  else if (optarg == "decl-sort-and-fun")
1204
  {
1205
    return ModelUninterpPrintMode::DeclSortAndFun;
1206
  }
1207
  else if (optarg == "help")
1208
  {
1209
    puts("uninterpreted elements in models printing  modes.\n"
1210
         "Available modes for --model-u-print are:\n"
1211
         "+ dtenum\n"
1212
         "  print uninterpreted elements as datatype enumerations, where the sort is the\n"
1213
         "  datatype\n"
1214
         "+ decl-fun\n"
1215
         "  print uninterpreted elements declare-fun, but don't include a declare-sort for\n"
1216
         "  the sort\n"
1217
         "+ none (default)\n"
1218
         "  (default) do not print declarations of uninterpreted elements in models.\n"
1219
         "+ decl-sort-and-fun\n"
1220
         "  print uninterpreted elements declare-fun, and also include a declare-sort for\n"
1221
         "  the sort\n");
1222
    exit(1);
1223
  }
1224
  else
1225
  {
1226
    throw OptionException(std::string("unknown option for --model-u-print: `") +
1227
                          optarg + "'.  Try --model-u-print=help.");
1228
  }
1229
}
1230
1231
std::ostream&
1232
operator<<(std::ostream& os, ProduceInterpols mode)
1233
{
1234
  os << "ProduceInterpols::";
1235
  switch(mode) {
1236
    case ProduceInterpols::ALL:
1237
      os << "ALL";
1238
      break;
1239
    case ProduceInterpols::DEFAULT:
1240
      os << "DEFAULT";
1241
      break;
1242
    case ProduceInterpols::CONJECTURE:
1243
      os << "CONJECTURE";
1244
      break;
1245
    case ProduceInterpols::NONE:
1246
      os << "NONE";
1247
      break;
1248
    case ProduceInterpols::ASSUMPTIONS:
1249
      os << "ASSUMPTIONS";
1250
      break;
1251
    case ProduceInterpols::SHARED:
1252
      os << "SHARED";
1253
      break;
1254
    default:
1255
        Unreachable();
1256
  }
1257
  return os;
1258
}
1259
1260
ProduceInterpols
1261
11
stringToProduceInterpols(const std::string& option, const std::string& optarg)
1262
{
1263
11
  if (optarg == "all")
1264
  {
1265
    return ProduceInterpols::ALL;
1266
  }
1267
11
  else if (optarg == "default")
1268
  {
1269
9
    return ProduceInterpols::DEFAULT;
1270
  }
1271
2
  else if (optarg == "conjecture")
1272
  {
1273
2
    return ProduceInterpols::CONJECTURE;
1274
  }
1275
  else if (optarg == "none")
1276
  {
1277
    return ProduceInterpols::NONE;
1278
  }
1279
  else if (optarg == "assumptions")
1280
  {
1281
    return ProduceInterpols::ASSUMPTIONS;
1282
  }
1283
  else if (optarg == "shared")
1284
  {
1285
    return ProduceInterpols::SHARED;
1286
  }
1287
  else if (optarg == "help")
1288
  {
1289
    puts("Interpolants grammar mode\n"
1290
         "Available modes for --produce-interpols are:\n"
1291
         "+ all\n"
1292
         "  use only operators that occur either in the assumptions or the conjecture\n"
1293
         "+ default\n"
1294
         "  use the default grammar for the theory or the user-defined grammar if given\n"
1295
         "+ conjecture\n"
1296
         "  use only operators that occur in the conjecture\n"
1297
         "+ none (default)\n"
1298
         "  don't compute interpolants\n"
1299
         "+ assumptions\n"
1300
         "  use only operators that occur in the assumptions\n"
1301
         "+ shared\n"
1302
         "  use only operators that occur both in the assumptions and the conjecture\n");
1303
    exit(1);
1304
  }
1305
  else
1306
  {
1307
    throw OptionException(std::string("unknown option for --produce-interpols: `") +
1308
                          optarg + "'.  Try --produce-interpols=help.");
1309
  }
1310
}
1311
1312
std::ostream&
1313
1
operator<<(std::ostream& os, SimplificationMode mode)
1314
{
1315
1
  os << "SimplificationMode::";
1316
1
  switch(mode) {
1317
    case SimplificationMode::BATCH:
1318
      os << "BATCH";
1319
      break;
1320
1
    case SimplificationMode::NONE:
1321
1
      os << "NONE";
1322
1
      break;
1323
    default:
1324
        Unreachable();
1325
  }
1326
1
  return os;
1327
}
1328
1329
SimplificationMode
1330
30
stringToSimplificationMode(const std::string& option, const std::string& optarg)
1331
{
1332
30
  if (optarg == "batch")
1333
  {
1334
    return SimplificationMode::BATCH;
1335
  }
1336
30
  else if (optarg == "none")
1337
  {
1338
30
    return SimplificationMode::NONE;
1339
  }
1340
  else if (optarg == "help")
1341
  {
1342
    puts("Simplification modes.\n"
1343
         "Available modes for --simplification are:\n"
1344
         "+ batch (default)\n"
1345
         "  Save up all ASSERTions; run nonclausal simplification and clausal (MiniSat)\n"
1346
         "  propagation for all of them only after reaching a querying command (CHECKSAT\n"
1347
         "  or QUERY or predicate SUBTYPE declaration).\n"
1348
         "+ none\n"
1349
         "  Do not perform nonclausal simplification.\n");
1350
    exit(1);
1351
  }
1352
  else
1353
  {
1354
    throw OptionException(std::string("unknown option for --simplification: `") +
1355
                          optarg + "'.  Try --simplification=help.");
1356
  }
1357
}
1358
1359
std::ostream&
1360
operator<<(std::ostream& os, SolveBVAsIntMode mode)
1361
{
1362
  os << "SolveBVAsIntMode::";
1363
  switch(mode) {
1364
    case SolveBVAsIntMode::IAND:
1365
      os << "IAND";
1366
      break;
1367
    case SolveBVAsIntMode::BV:
1368
      os << "BV";
1369
      break;
1370
    case SolveBVAsIntMode::SUM:
1371
      os << "SUM";
1372
      break;
1373
    case SolveBVAsIntMode::OFF:
1374
      os << "OFF";
1375
      break;
1376
    default:
1377
        Unreachable();
1378
  }
1379
  return os;
1380
}
1381
1382
SolveBVAsIntMode
1383
116
stringToSolveBVAsIntMode(const std::string& option, const std::string& optarg)
1384
{
1385
116
  if (optarg == "iand")
1386
  {
1387
28
    return SolveBVAsIntMode::IAND;
1388
  }
1389
88
  else if (optarg == "bv")
1390
  {
1391
18
    return SolveBVAsIntMode::BV;
1392
  }
1393
70
  else if (optarg == "sum")
1394
  {
1395
70
    return SolveBVAsIntMode::SUM;
1396
  }
1397
  else if (optarg == "off")
1398
  {
1399
    return SolveBVAsIntMode::OFF;
1400
  }
1401
  else if (optarg == "help")
1402
  {
1403
    puts("solve-bv-as-int modes.\n"
1404
         "Available modes for --solve-bv-as-int are:\n"
1405
         "+ iand\n"
1406
         "  Translate bvand to the iand operator (experimental)\n"
1407
         "+ bv\n"
1408
         "  Translate bvand back to bit-vectors\n"
1409
         "+ sum\n"
1410
         "  Generate a sum expression for each bvand instance, based on the value in\n"
1411
         "  --solbv-bv-as-int-granularity\n"
1412
         "+ off (default)\n"
1413
         "  Do not translate bit-vectors to integers\n");
1414
    exit(1);
1415
  }
1416
  else
1417
  {
1418
    throw OptionException(std::string("unknown option for --solve-bv-as-int: `") +
1419
                          optarg + "'.  Try --solve-bv-as-int=help.");
1420
  }
1421
}
1422
1423
std::ostream&
1424
operator<<(std::ostream& os, SygusSolutionOutMode mode)
1425
{
1426
  os << "SygusSolutionOutMode::";
1427
  switch(mode) {
1428
    case SygusSolutionOutMode::STANDARD:
1429
      os << "STANDARD";
1430
      break;
1431
    case SygusSolutionOutMode::STATUS_OR_DEF:
1432
      os << "STATUS_OR_DEF";
1433
      break;
1434
    case SygusSolutionOutMode::STATUS:
1435
      os << "STATUS";
1436
      break;
1437
    case SygusSolutionOutMode::STATUS_AND_DEF:
1438
      os << "STATUS_AND_DEF";
1439
      break;
1440
    default:
1441
        Unreachable();
1442
  }
1443
  return os;
1444
}
1445
1446
SygusSolutionOutMode
1447
346
stringToSygusSolutionOutMode(const std::string& option, const std::string& optarg)
1448
{
1449
346
  if (optarg == "sygus-standard")
1450
  {
1451
    return SygusSolutionOutMode::STANDARD;
1452
  }
1453
346
  else if (optarg == "status-or-def")
1454
  {
1455
    return SygusSolutionOutMode::STATUS_OR_DEF;
1456
  }
1457
346
  else if (optarg == "status")
1458
  {
1459
346
    return SygusSolutionOutMode::STATUS;
1460
  }
1461
  else if (optarg == "status-and-def")
1462
  {
1463
    return SygusSolutionOutMode::STATUS_AND_DEF;
1464
  }
1465
  else if (optarg == "help")
1466
  {
1467
    puts("Modes for sygus solution output.\n"
1468
         "Available modes for --sygus-out are:\n"
1469
         "+ sygus-standard\n"
1470
         "  Print based on SyGuS standard.\n"
1471
         "+ status-or-def\n"
1472
         "  Print status if infeasible, or definition corresponding to solution if\n"
1473
         "  feasible.\n"
1474
         "+ status\n"
1475
         "  Print only status for check-synth calls.\n"
1476
         "+ status-and-def (default)\n"
1477
         "  Print status followed by definition corresponding to solution.\n");
1478
    exit(1);
1479
  }
1480
  else
1481
  {
1482
    throw OptionException(std::string("unknown option for --sygus-out: `") +
1483
                          optarg + "'.  Try --sygus-out=help.");
1484
  }
1485
}
1486
1487
1488
}  // namespace options
1489
26691
}  // namespace CVC4