GCC Code Coverage Report
Directory: . Exec Total Coverage
File: build-coverage/src/options/quantifiers_options.cpp Lines: 608 1900 32.0 %
Date: 2021-03-23 Branches: 39 691 5.6 %

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
228439
template <> const options::aggressiveMiniscopeQuant__option_t::type& Options::operator[](
24
    options::aggressiveMiniscopeQuant__option_t) const
25
{
26
228439
  return d_holder->aggressiveMiniscopeQuant;
27
}
28
template <> bool Options::wasSetByUser(options::aggressiveMiniscopeQuant__option_t) const
29
{
30
  return d_holder->aggressiveMiniscopeQuant__setByUser__;
31
}
32
template <> void Options::set(
33
    options::cegisSample__option_t,
34
    const options::cegisSample__option_t::type& x)
35
{
36
  d_holder->cegisSample = x;
37
}
38
5387
template <> const options::cegisSample__option_t::type& Options::operator[](
39
    options::cegisSample__option_t) const
40
{
41
5387
  return d_holder->cegisSample;
42
}
43
template <> bool Options::wasSetByUser(options::cegisSample__option_t) const
44
{
45
  return d_holder->cegisSample__setByUser__;
46
}
47
6238
template <> void Options::set(
48
    options::cegqi__option_t,
49
    const options::cegqi__option_t::type& x)
50
{
51
6238
  d_holder->cegqi = x;
52
6238
}
53
5020895
template <> const options::cegqi__option_t::type& Options::operator[](
54
    options::cegqi__option_t) const
55
{
56
5020895
  return d_holder->cegqi;
57
}
58
6259
template <> bool Options::wasSetByUser(options::cegqi__option_t) const
59
{
60
6259
  return d_holder->cegqi__setByUser__;
61
}
62
template <> void Options::set(
63
    options::cegqiAll__option_t,
64
    const options::cegqiAll__option_t::type& x)
65
{
66
  d_holder->cegqiAll = x;
67
}
68
20331
template <> const options::cegqiAll__option_t::type& Options::operator[](
69
    options::cegqiAll__option_t) const
70
{
71
20331
  return d_holder->cegqiAll;
72
}
73
template <> bool Options::wasSetByUser(options::cegqiAll__option_t) const
74
{
75
  return d_holder->cegqiAll__setByUser__;
76
}
77
1314
template <> void Options::set(
78
    options::cegqiBv__option_t,
79
    const options::cegqiBv__option_t::type& x)
80
{
81
1314
  d_holder->cegqiBv = x;
82
1314
}
83
19156
template <> const options::cegqiBv__option_t::type& Options::operator[](
84
    options::cegqiBv__option_t) const
85
{
86
19156
  return d_holder->cegqiBv;
87
}
88
1319
template <> bool Options::wasSetByUser(options::cegqiBv__option_t) const
89
{
90
1319
  return d_holder->cegqiBv__setByUser__;
91
}
92
template <> void Options::set(
93
    options::cegqiBvConcInv__option_t,
94
    const options::cegqiBvConcInv__option_t::type& x)
95
{
96
  d_holder->cegqiBvConcInv = x;
97
}
98
275
template <> const options::cegqiBvConcInv__option_t::type& Options::operator[](
99
    options::cegqiBvConcInv__option_t) const
100
{
101
275
  return d_holder->cegqiBvConcInv;
102
}
103
template <> bool Options::wasSetByUser(options::cegqiBvConcInv__option_t) const
104
{
105
  return d_holder->cegqiBvConcInv__setByUser__;
106
}
107
template <> void Options::set(
108
    options::cegqiBvIneqMode__option_t,
109
    const options::cegqiBvIneqMode__option_t::type& x)
110
{
111
  d_holder->cegqiBvIneqMode = x;
112
}
113
9847
template <> const options::cegqiBvIneqMode__option_t::type& Options::operator[](
114
    options::cegqiBvIneqMode__option_t) const
115
{
116
9847
  return d_holder->cegqiBvIneqMode;
117
}
118
template <> bool Options::wasSetByUser(options::cegqiBvIneqMode__option_t) const
119
{
120
  return d_holder->cegqiBvIneqMode__setByUser__;
121
}
122
template <> void Options::set(
123
    options::cegqiBvInterleaveValue__option_t,
124
    const options::cegqiBvInterleaveValue__option_t::type& x)
125
{
126
  d_holder->cegqiBvInterleaveValue = x;
127
}
128
1581
template <> const options::cegqiBvInterleaveValue__option_t::type& Options::operator[](
129
    options::cegqiBvInterleaveValue__option_t) const
130
{
131
1581
  return d_holder->cegqiBvInterleaveValue;
132
}
133
template <> bool Options::wasSetByUser(options::cegqiBvInterleaveValue__option_t) const
134
{
135
  return d_holder->cegqiBvInterleaveValue__setByUser__;
136
}
137
template <> void Options::set(
138
    options::cegqiBvLinearize__option_t,
139
    const options::cegqiBvLinearize__option_t::type& x)
140
{
141
  d_holder->cegqiBvLinearize = x;
142
}
143
9730
template <> const options::cegqiBvLinearize__option_t::type& Options::operator[](
144
    options::cegqiBvLinearize__option_t) const
145
{
146
9730
  return d_holder->cegqiBvLinearize;
147
}
148
template <> bool Options::wasSetByUser(options::cegqiBvLinearize__option_t) const
149
{
150
  return d_holder->cegqiBvLinearize__setByUser__;
151
}
152
template <> void Options::set(
153
    options::cegqiBvRmExtract__option_t,
154
    const options::cegqiBvRmExtract__option_t::type& x)
155
{
156
  d_holder->cegqiBvRmExtract = x;
157
}
158
714
template <> const options::cegqiBvRmExtract__option_t::type& Options::operator[](
159
    options::cegqiBvRmExtract__option_t) const
160
{
161
714
  return d_holder->cegqiBvRmExtract;
162
}
163
template <> bool Options::wasSetByUser(options::cegqiBvRmExtract__option_t) const
164
{
165
  return d_holder->cegqiBvRmExtract__setByUser__;
166
}
167
template <> void Options::set(
168
    options::cegqiBvSolveNl__option_t,
169
    const options::cegqiBvSolveNl__option_t::type& x)
170
{
171
  d_holder->cegqiBvSolveNl = x;
172
}
173
3184
template <> const options::cegqiBvSolveNl__option_t::type& Options::operator[](
174
    options::cegqiBvSolveNl__option_t) const
175
{
176
3184
  return d_holder->cegqiBvSolveNl;
177
}
178
template <> bool Options::wasSetByUser(options::cegqiBvSolveNl__option_t) const
179
{
180
  return d_holder->cegqiBvSolveNl__setByUser__;
181
}
182
1378
template <> void Options::set(
183
    options::cegqiFullEffort__option_t,
184
    const options::cegqiFullEffort__option_t::type& x)
185
{
186
1378
  d_holder->cegqiFullEffort = x;
187
1378
}
188
729
template <> const options::cegqiFullEffort__option_t::type& Options::operator[](
189
    options::cegqiFullEffort__option_t) const
190
{
191
729
  return d_holder->cegqiFullEffort;
192
}
193
1470
template <> bool Options::wasSetByUser(options::cegqiFullEffort__option_t) const
194
{
195
1470
  return d_holder->cegqiFullEffort__setByUser__;
196
}
197
template <> void Options::set(
198
    options::cegqiInnermost__option_t,
199
    const options::cegqiInnermost__option_t::type& x)
200
{
201
  d_holder->cegqiInnermost = x;
202
}
203
27662
template <> const options::cegqiInnermost__option_t::type& Options::operator[](
204
    options::cegqiInnermost__option_t) const
205
{
206
27662
  return d_holder->cegqiInnermost;
207
}
208
template <> bool Options::wasSetByUser(options::cegqiInnermost__option_t) const
209
{
210
  return d_holder->cegqiInnermost__setByUser__;
211
}
212
1319
template <> void Options::set(
213
    options::cegqiMidpoint__option_t,
214
    const options::cegqiMidpoint__option_t::type& x)
215
{
216
1319
  d_holder->cegqiMidpoint = x;
217
1319
}
218
2836
template <> const options::cegqiMidpoint__option_t::type& Options::operator[](
219
    options::cegqiMidpoint__option_t) const
220
{
221
2836
  return d_holder->cegqiMidpoint;
222
}
223
1319
template <> bool Options::wasSetByUser(options::cegqiMidpoint__option_t) const
224
{
225
1319
  return d_holder->cegqiMidpoint__setByUser__;
226
}
227
5845
template <> const options::cegqiMinBounds__option_t::type& Options::operator[](
228
    options::cegqiMinBounds__option_t) const
229
{
230
5845
  return d_holder->cegqiMinBounds;
231
}
232
template <> bool Options::wasSetByUser(options::cegqiMinBounds__option_t) const
233
{
234
  return d_holder->cegqiMinBounds__setByUser__;
235
}
236
template <> void Options::set(
237
    options::cegqiModel__option_t,
238
    const options::cegqiModel__option_t::type& x)
239
{
240
  d_holder->cegqiModel = x;
241
}
242
34928
template <> const options::cegqiModel__option_t::type& Options::operator[](
243
    options::cegqiModel__option_t) const
244
{
245
34928
  return d_holder->cegqiModel;
246
}
247
template <> bool Options::wasSetByUser(options::cegqiModel__option_t) const
248
{
249
  return d_holder->cegqiModel__setByUser__;
250
}
251
template <> void Options::set(
252
    options::cegqiMultiInst__option_t,
253
    const options::cegqiMultiInst__option_t::type& x)
254
{
255
  d_holder->cegqiMultiInst = x;
256
}
257
35736
template <> const options::cegqiMultiInst__option_t::type& Options::operator[](
258
    options::cegqiMultiInst__option_t) const
259
{
260
35736
  return d_holder->cegqiMultiInst;
261
}
262
template <> bool Options::wasSetByUser(options::cegqiMultiInst__option_t) const
263
{
264
  return d_holder->cegqiMultiInst__setByUser__;
265
}
266
6890
template <> void Options::set(
267
    options::cegqiNestedQE__option_t,
268
    const options::cegqiNestedQE__option_t::type& x)
269
{
270
6890
  d_holder->cegqiNestedQE = x;
271
6890
}
272
14974
template <> const options::cegqiNestedQE__option_t::type& Options::operator[](
273
    options::cegqiNestedQE__option_t) const
274
{
275
14974
  return d_holder->cegqiNestedQE;
276
}
277
template <> bool Options::wasSetByUser(options::cegqiNestedQE__option_t) const
278
{
279
  return d_holder->cegqiNestedQE__setByUser__;
280
}
281
40
template <> const options::cegqiNopt__option_t::type& Options::operator[](
282
    options::cegqiNopt__option_t) const
283
{
284
40
  return d_holder->cegqiNopt;
285
}
286
template <> bool Options::wasSetByUser(options::cegqiNopt__option_t) const
287
{
288
  return d_holder->cegqiNopt__setByUser__;
289
}
290
template <> void Options::set(
291
    options::cegqiRepeatLit__option_t,
292
    const options::cegqiRepeatLit__option_t::type& x)
293
{
294
  d_holder->cegqiRepeatLit = x;
295
}
296
162888
template <> const options::cegqiRepeatLit__option_t::type& Options::operator[](
297
    options::cegqiRepeatLit__option_t) const
298
{
299
162888
  return d_holder->cegqiRepeatLit;
300
}
301
template <> bool Options::wasSetByUser(options::cegqiRepeatLit__option_t) const
302
{
303
  return d_holder->cegqiRepeatLit__setByUser__;
304
}
305
9
template <> const options::cegqiRoundUpLowerLia__option_t::type& Options::operator[](
306
    options::cegqiRoundUpLowerLia__option_t) const
307
{
308
9
  return d_holder->cegqiRoundUpLowerLia;
309
}
310
template <> bool Options::wasSetByUser(options::cegqiRoundUpLowerLia__option_t) const
311
{
312
  return d_holder->cegqiRoundUpLowerLia__setByUser__;
313
}
314
template <> void Options::set(
315
    options::cegqiSat__option_t,
316
    const options::cegqiSat__option_t::type& x)
317
{
318
  d_holder->cegqiSat = x;
319
}
320
3591
template <> const options::cegqiSat__option_t::type& Options::operator[](
321
    options::cegqiSat__option_t) const
322
{
323
3591
  return d_holder->cegqiSat;
324
}
325
template <> bool Options::wasSetByUser(options::cegqiSat__option_t) const
326
{
327
  return d_holder->cegqiSat__setByUser__;
328
}
329
template <> void Options::set(
330
    options::cegqiUseInfInt__option_t,
331
    const options::cegqiUseInfInt__option_t::type& x)
332
{
333
  d_holder->cegqiUseInfInt = x;
334
}
335
5385
template <> const options::cegqiUseInfInt__option_t::type& Options::operator[](
336
    options::cegqiUseInfInt__option_t) const
337
{
338
5385
  return d_holder->cegqiUseInfInt;
339
}
340
template <> bool Options::wasSetByUser(options::cegqiUseInfInt__option_t) const
341
{
342
  return d_holder->cegqiUseInfInt__setByUser__;
343
}
344
template <> void Options::set(
345
    options::cegqiUseInfReal__option_t,
346
    const options::cegqiUseInfReal__option_t::type& x)
347
{
348
  d_holder->cegqiUseInfReal = x;
349
}
350
460
template <> const options::cegqiUseInfReal__option_t::type& Options::operator[](
351
    options::cegqiUseInfReal__option_t) const
352
{
353
460
  return d_holder->cegqiUseInfReal;
354
}
355
template <> bool Options::wasSetByUser(options::cegqiUseInfReal__option_t) const
356
{
357
  return d_holder->cegqiUseInfReal__setByUser__;
358
}
359
20995
template <> const options::condVarSplitQuantAgg__option_t::type& Options::operator[](
360
    options::condVarSplitQuantAgg__option_t) const
361
{
362
20995
  return d_holder->condVarSplitQuantAgg;
363
}
364
template <> bool Options::wasSetByUser(options::condVarSplitQuantAgg__option_t) const
365
{
366
  return d_holder->condVarSplitQuantAgg__setByUser__;
367
}
368
207532
template <> const options::condVarSplitQuant__option_t::type& Options::operator[](
369
    options::condVarSplitQuant__option_t) const
370
{
371
207532
  return d_holder->condVarSplitQuant;
372
}
373
template <> bool Options::wasSetByUser(options::condVarSplitQuant__option_t) const
374
{
375
  return d_holder->condVarSplitQuant__setByUser__;
376
}
377
4
template <> void Options::set(
378
    options::conjectureFilterActiveTerms__option_t,
379
    const options::conjectureFilterActiveTerms__option_t::type& x)
380
{
381
4
  d_holder->conjectureFilterActiveTerms = x;
382
4
}
383
3245
template <> const options::conjectureFilterActiveTerms__option_t::type& Options::operator[](
384
    options::conjectureFilterActiveTerms__option_t) const
385
{
386
3245
  return d_holder->conjectureFilterActiveTerms;
387
}
388
4
template <> bool Options::wasSetByUser(options::conjectureFilterActiveTerms__option_t) const
389
{
390
4
  return d_holder->conjectureFilterActiveTerms__setByUser__;
391
}
392
4
template <> void Options::set(
393
    options::conjectureFilterCanonical__option_t,
394
    const options::conjectureFilterCanonical__option_t::type& x)
395
{
396
4
  d_holder->conjectureFilterCanonical = x;
397
4
}
398
6593
template <> const options::conjectureFilterCanonical__option_t::type& Options::operator[](
399
    options::conjectureFilterCanonical__option_t) const
400
{
401
6593
  return d_holder->conjectureFilterCanonical;
402
}
403
4
template <> bool Options::wasSetByUser(options::conjectureFilterCanonical__option_t) const
404
{
405
4
  return d_holder->conjectureFilterCanonical__setByUser__;
406
}
407
template <> void Options::set(
408
    options::conjectureFilterModel__option_t,
409
    const options::conjectureFilterModel__option_t::type& x)
410
{
411
  d_holder->conjectureFilterModel = x;
412
}
413
14667
template <> const options::conjectureFilterModel__option_t::type& Options::operator[](
414
    options::conjectureFilterModel__option_t) const
415
{
416
14667
  return d_holder->conjectureFilterModel;
417
}
418
4
template <> bool Options::wasSetByUser(options::conjectureFilterModel__option_t) const
419
{
420
4
  return d_holder->conjectureFilterModel__setByUser__;
421
}
422
template <> void Options::set(
423
    options::conjectureGen__option_t,
424
    const options::conjectureGen__option_t::type& x)
425
{
426
  d_holder->conjectureGen = x;
427
}
428
6054
template <> const options::conjectureGen__option_t::type& Options::operator[](
429
    options::conjectureGen__option_t) const
430
{
431
6054
  return d_holder->conjectureGen;
432
}
433
template <> bool Options::wasSetByUser(options::conjectureGen__option_t) const
434
{
435
  return d_holder->conjectureGen__setByUser__;
436
}
437
92
template <> const options::conjectureGenGtEnum__option_t::type& Options::operator[](
438
    options::conjectureGenGtEnum__option_t) const
439
{
440
92
  return d_holder->conjectureGenGtEnum;
441
}
442
template <> bool Options::wasSetByUser(options::conjectureGenGtEnum__option_t) const
443
{
444
  return d_holder->conjectureGenGtEnum__setByUser__;
445
}
446
48
template <> const options::conjectureGenMaxDepth__option_t::type& Options::operator[](
447
    options::conjectureGenMaxDepth__option_t) const
448
{
449
48
  return d_holder->conjectureGenMaxDepth;
450
}
451
template <> bool Options::wasSetByUser(options::conjectureGenMaxDepth__option_t) const
452
{
453
  return d_holder->conjectureGenMaxDepth__setByUser__;
454
}
455
770
template <> const options::conjectureGenPerRound__option_t::type& Options::operator[](
456
    options::conjectureGenPerRound__option_t) const
457
{
458
770
  return d_holder->conjectureGenPerRound;
459
}
460
8997
template <> bool Options::wasSetByUser(options::conjectureGenPerRound__option_t) const
461
{
462
8997
  return d_holder->conjectureGenPerRound__setByUser__;
463
}
464
97
template <> const options::conjectureUeeIntro__option_t::type& Options::operator[](
465
    options::conjectureUeeIntro__option_t) const
466
{
467
97
  return d_holder->conjectureUeeIntro;
468
}
469
template <> bool Options::wasSetByUser(options::conjectureUeeIntro__option_t) const
470
{
471
  return d_holder->conjectureUeeIntro__setByUser__;
472
}
473
8997
template <> const options::conjectureNoFilter__option_t::type& Options::operator[](
474
    options::conjectureNoFilter__option_t) const
475
{
476
8997
  return d_holder->conjectureNoFilter;
477
}
478
template <> bool Options::wasSetByUser(options::conjectureNoFilter__option_t) const
479
{
480
  return d_holder->conjectureNoFilter__setByUser__;
481
}
482
template <> void Options::set(
483
    options::debugInst__option_t,
484
    const options::debugInst__option_t::type& x)
485
{
486
  d_holder->debugInst = x;
487
}
488
12612
template <> const options::debugInst__option_t::type& Options::operator[](
489
    options::debugInst__option_t) const
490
{
491
12612
  return d_holder->debugInst;
492
}
493
template <> bool Options::wasSetByUser(options::debugInst__option_t) const
494
{
495
  return d_holder->debugInst__setByUser__;
496
}
497
template <> void Options::set(
498
    options::debugSygus__option_t,
499
    const options::debugSygus__option_t::type& x)
500
{
501
  d_holder->debugSygus = x;
502
}
503
56223
template <> const options::debugSygus__option_t::type& Options::operator[](
504
    options::debugSygus__option_t) const
505
{
506
56223
  return d_holder->debugSygus;
507
}
508
template <> bool Options::wasSetByUser(options::debugSygus__option_t) const
509
{
510
  return d_holder->debugSygus__setByUser__;
511
}
512
10
template <> void Options::set(
513
    options::dtStcInduction__option_t,
514
    const options::dtStcInduction__option_t::type& x)
515
{
516
10
  d_holder->dtStcInduction = x;
517
10
}
518
18437
template <> const options::dtStcInduction__option_t::type& Options::operator[](
519
    options::dtStcInduction__option_t) const
520
{
521
18437
  return d_holder->dtStcInduction;
522
}
523
10
template <> bool Options::wasSetByUser(options::dtStcInduction__option_t) const
524
{
525
10
  return d_holder->dtStcInduction__setByUser__;
526
}
527
34
template <> const options::dtVarExpandQuant__option_t::type& Options::operator[](
528
    options::dtVarExpandQuant__option_t) const
529
{
530
34
  return d_holder->dtVarExpandQuant;
531
}
532
template <> bool Options::wasSetByUser(options::dtVarExpandQuant__option_t) const
533
{
534
  return d_holder->dtVarExpandQuant__setByUser__;
535
}
536
250
template <> void Options::set(
537
    options::eMatching__option_t,
538
    const options::eMatching__option_t::type& x)
539
{
540
250
  d_holder->eMatching = x;
541
250
}
542
6078
template <> const options::eMatching__option_t::type& Options::operator[](
543
    options::eMatching__option_t) const
544
{
545
6078
  return d_holder->eMatching;
546
}
547
250
template <> bool Options::wasSetByUser(options::eMatching__option_t) const
548
{
549
250
  return d_holder->eMatching__setByUser__;
550
}
551
571640
template <> const options::elimTautQuant__option_t::type& Options::operator[](
552
    options::elimTautQuant__option_t) const
553
{
554
571640
  return d_holder->elimTautQuant;
555
}
556
template <> bool Options::wasSetByUser(options::elimTautQuant__option_t) const
557
{
558
  return d_holder->elimTautQuant__setByUser__;
559
}
560
113623
template <> const options::extRewriteQuant__option_t::type& Options::operator[](
561
    options::extRewriteQuant__option_t) const
562
{
563
113623
  return d_holder->extRewriteQuant;
564
}
565
template <> bool Options::wasSetByUser(options::extRewriteQuant__option_t) const
566
{
567
  return d_holder->extRewriteQuant__setByUser__;
568
}
569
83
template <> void Options::set(
570
    options::finiteModelFind__option_t,
571
    const options::finiteModelFind__option_t::type& x)
572
{
573
83
  d_holder->finiteModelFind = x;
574
83
}
575
8887497
template <> const options::finiteModelFind__option_t::type& Options::operator[](
576
    options::finiteModelFind__option_t) const
577
{
578
8887497
  return d_holder->finiteModelFind;
579
}
580
58
template <> bool Options::wasSetByUser(options::finiteModelFind__option_t) const
581
{
582
58
  return d_holder->finiteModelFind__setByUser__;
583
}
584
571
template <> void Options::set(
585
    options::fmfBound__option_t,
586
    const options::fmfBound__option_t::type& x)
587
{
588
571
  d_holder->fmfBound = x;
589
571
}
590
37328
template <> const options::fmfBound__option_t::type& Options::operator[](
591
    options::fmfBound__option_t) const
592
{
593
37328
  return d_holder->fmfBound;
594
}
595
557
template <> bool Options::wasSetByUser(options::fmfBound__option_t) const
596
{
597
557
  return d_holder->fmfBound__setByUser__;
598
}
599
template <> void Options::set(
600
    options::fmfBoundInt__option_t,
601
    const options::fmfBoundInt__option_t::type& x)
602
{
603
  d_holder->fmfBoundInt = x;
604
}
605
12
template <> const options::fmfBoundInt__option_t::type& Options::operator[](
606
    options::fmfBoundInt__option_t) const
607
{
608
12
  return d_holder->fmfBoundInt;
609
}
610
8993
template <> bool Options::wasSetByUser(options::fmfBoundInt__option_t) const
611
{
612
8993
  return d_holder->fmfBoundInt__setByUser__;
613
}
614
template <> void Options::set(
615
    options::fmfBoundLazy__option_t,
616
    const options::fmfBoundLazy__option_t::type& x)
617
{
618
  d_holder->fmfBoundLazy = x;
619
}
620
319
template <> const options::fmfBoundLazy__option_t::type& Options::operator[](
621
    options::fmfBoundLazy__option_t) const
622
{
623
319
  return d_holder->fmfBoundLazy;
624
}
625
8997
template <> bool Options::wasSetByUser(options::fmfBoundLazy__option_t) const
626
{
627
8997
  return d_holder->fmfBoundLazy__setByUser__;
628
}
629
46748
template <> const options::fmfFmcSimple__option_t::type& Options::operator[](
630
    options::fmfFmcSimple__option_t) const
631
{
632
46748
  return d_holder->fmfFmcSimple;
633
}
634
template <> bool Options::wasSetByUser(options::fmfFmcSimple__option_t) const
635
{
636
  return d_holder->fmfFmcSimple__setByUser__;
637
}
638
493
template <> const options::fmfFreshDistConst__option_t::type& Options::operator[](
639
    options::fmfFreshDistConst__option_t) const
640
{
641
493
  return d_holder->fmfFreshDistConst;
642
}
643
template <> bool Options::wasSetByUser(options::fmfFreshDistConst__option_t) const
644
{
645
  return d_holder->fmfFreshDistConst__setByUser__;
646
}
647
14
template <> void Options::set(
648
    options::fmfFunWellDefined__option_t,
649
    const options::fmfFunWellDefined__option_t::type& x)
650
{
651
14
  d_holder->fmfFunWellDefined = x;
652
14
}
653
15429
template <> const options::fmfFunWellDefined__option_t::type& Options::operator[](
654
    options::fmfFunWellDefined__option_t) const
655
{
656
15429
  return d_holder->fmfFunWellDefined;
657
}
658
14
template <> bool Options::wasSetByUser(options::fmfFunWellDefined__option_t) const
659
{
660
14
  return d_holder->fmfFunWellDefined__setByUser__;
661
}
662
10617
template <> const options::fmfFunWellDefinedRelevant__option_t::type& Options::operator[](
663
    options::fmfFunWellDefinedRelevant__option_t) const
664
{
665
10617
  return d_holder->fmfFunWellDefinedRelevant;
666
}
667
template <> bool Options::wasSetByUser(options::fmfFunWellDefinedRelevant__option_t) const
668
{
669
  return d_holder->fmfFunWellDefinedRelevant__setByUser__;
670
}
671
template <> void Options::set(
672
    options::fmfInstEngine__option_t,
673
    const options::fmfInstEngine__option_t::type& x)
674
{
675
  d_holder->fmfInstEngine = x;
676
}
677
484
template <> const options::fmfInstEngine__option_t::type& Options::operator[](
678
    options::fmfInstEngine__option_t) const
679
{
680
484
  return d_holder->fmfInstEngine;
681
}
682
template <> bool Options::wasSetByUser(options::fmfInstEngine__option_t) const
683
{
684
  return d_holder->fmfInstEngine__setByUser__;
685
}
686
8997
template <> const options::fmfTypeCompletionThresh__option_t::type& Options::operator[](
687
    options::fmfTypeCompletionThresh__option_t) const
688
{
689
8997
  return d_holder->fmfTypeCompletionThresh;
690
}
691
template <> bool Options::wasSetByUser(options::fmfTypeCompletionThresh__option_t) const
692
{
693
  return d_holder->fmfTypeCompletionThresh__setByUser__;
694
}
695
11992
template <> const options::fullSaturateInterleave__option_t::type& Options::operator[](
696
    options::fullSaturateInterleave__option_t) const
697
{
698
11992
  return d_holder->fullSaturateInterleave;
699
}
700
template <> bool Options::wasSetByUser(options::fullSaturateInterleave__option_t) const
701
{
702
  return d_holder->fullSaturateInterleave__setByUser__;
703
}
704
1390
template <> const options::fullSaturateStratify__option_t::type& Options::operator[](
705
    options::fullSaturateStratify__option_t) const
706
{
707
1390
  return d_holder->fullSaturateStratify;
708
}
709
template <> bool Options::wasSetByUser(options::fullSaturateStratify__option_t) const
710
{
711
  return d_holder->fullSaturateStratify__setByUser__;
712
}
713
1965
template <> const options::fullSaturateSum__option_t::type& Options::operator[](
714
    options::fullSaturateSum__option_t) const
715
{
716
1965
  return d_holder->fullSaturateSum;
717
}
718
template <> bool Options::wasSetByUser(options::fullSaturateSum__option_t) const
719
{
720
  return d_holder->fullSaturateSum__setByUser__;
721
}
722
template <> void Options::set(
723
    options::fullSaturateQuant__option_t,
724
    const options::fullSaturateQuant__option_t::type& x)
725
{
726
  d_holder->fullSaturateQuant = x;
727
}
728
12071
template <> const options::fullSaturateQuant__option_t::type& Options::operator[](
729
    options::fullSaturateQuant__option_t) const
730
{
731
12071
  return d_holder->fullSaturateQuant;
732
}
733
template <> bool Options::wasSetByUser(options::fullSaturateQuant__option_t) const
734
{
735
  return d_holder->fullSaturateQuant__setByUser__;
736
}
737
79
template <> const options::fullSaturateLimit__option_t::type& Options::operator[](
738
    options::fullSaturateLimit__option_t) const
739
{
740
79
  return d_holder->fullSaturateLimit;
741
}
742
template <> bool Options::wasSetByUser(options::fullSaturateLimit__option_t) const
743
{
744
  return d_holder->fullSaturateLimit__setByUser__;
745
}
746
127
template <> const options::fullSaturateQuantRd__option_t::type& Options::operator[](
747
    options::fullSaturateQuantRd__option_t) const
748
{
749
127
  return d_holder->fullSaturateQuantRd;
750
}
751
template <> bool Options::wasSetByUser(options::fullSaturateQuantRd__option_t) const
752
{
753
  return d_holder->fullSaturateQuantRd__setByUser__;
754
}
755
1529
template <> void Options::set(
756
    options::globalNegate__option_t,
757
    const options::globalNegate__option_t::type& x)
758
{
759
1529
  d_holder->globalNegate = x;
760
1529
}
761
35340
template <> const options::globalNegate__option_t::type& Options::operator[](
762
    options::globalNegate__option_t) const
763
{
764
35340
  return d_holder->globalNegate;
765
}
766
template <> bool Options::wasSetByUser(options::globalNegate__option_t) const
767
{
768
  return d_holder->globalNegate__setByUser__;
769
}
770
28057
template <> const options::hoElim__option_t::type& Options::operator[](
771
    options::hoElim__option_t) const
772
{
773
28057
  return d_holder->hoElim;
774
}
775
template <> bool Options::wasSetByUser(options::hoElim__option_t) const
776
{
777
  return d_holder->hoElim__setByUser__;
778
}
779
215
template <> void Options::set(
780
    options::hoElimStoreAx__option_t,
781
    const options::hoElimStoreAx__option_t::type& x)
782
{
783
215
  d_holder->hoElimStoreAx = x;
784
215
}
785
702
template <> const options::hoElimStoreAx__option_t::type& Options::operator[](
786
    options::hoElimStoreAx__option_t) const
787
{
788
702
  return d_holder->hoElimStoreAx;
789
}
790
216
template <> bool Options::wasSetByUser(options::hoElimStoreAx__option_t) const
791
{
792
216
  return d_holder->hoElimStoreAx__setByUser__;
793
}
794
160
template <> const options::hoMatching__option_t::type& Options::operator[](
795
    options::hoMatching__option_t) const
796
{
797
160
  return d_holder->hoMatching;
798
}
799
template <> bool Options::wasSetByUser(options::hoMatching__option_t) const
800
{
801
  return d_holder->hoMatching__setByUser__;
802
}
803
236
template <> const options::hoMatchingVarArgPriority__option_t::type& Options::operator[](
804
    options::hoMatchingVarArgPriority__option_t) const
805
{
806
236
  return d_holder->hoMatchingVarArgPriority;
807
}
808
template <> bool Options::wasSetByUser(options::hoMatchingVarArgPriority__option_t) const
809
{
810
  return d_holder->hoMatchingVarArgPriority__setByUser__;
811
}
812
1041
template <> const options::hoMergeTermDb__option_t::type& Options::operator[](
813
    options::hoMergeTermDb__option_t) const
814
{
815
1041
  return d_holder->hoMergeTermDb;
816
}
817
template <> bool Options::wasSetByUser(options::hoMergeTermDb__option_t) const
818
{
819
  return d_holder->hoMergeTermDb__setByUser__;
820
}
821
5825
template <> const options::incrementTriggers__option_t::type& Options::operator[](
822
    options::incrementTriggers__option_t) const
823
{
824
5825
  return d_holder->incrementTriggers;
825
}
826
template <> bool Options::wasSetByUser(options::incrementTriggers__option_t) const
827
{
828
  return d_holder->incrementTriggers__setByUser__;
829
}
830
5909
template <> const options::instLevelInputOnly__option_t::type& Options::operator[](
831
    options::instLevelInputOnly__option_t) const
832
{
833
5909
  return d_holder->instLevelInputOnly;
834
}
835
template <> bool Options::wasSetByUser(options::instLevelInputOnly__option_t) const
836
{
837
  return d_holder->instLevelInputOnly__setByUser__;
838
}
839
template <> void Options::set(
840
    options::instMaxLevel__option_t,
841
    const options::instMaxLevel__option_t::type& x)
842
{
843
  d_holder->instMaxLevel = x;
844
}
845
180553
template <> const options::instMaxLevel__option_t::type& Options::operator[](
846
    options::instMaxLevel__option_t) const
847
{
848
180553
  return d_holder->instMaxLevel;
849
}
850
template <> bool Options::wasSetByUser(options::instMaxLevel__option_t) const
851
{
852
  return d_holder->instMaxLevel__setByUser__;
853
}
854
1578
template <> void Options::set(
855
    options::instNoEntail__option_t,
856
    const options::instNoEntail__option_t::type& x)
857
{
858
1578
  d_holder->instNoEntail = x;
859
1578
}
860
236623
template <> const options::instNoEntail__option_t::type& Options::operator[](
861
    options::instNoEntail__option_t) const
862
{
863
236623
  return d_holder->instNoEntail;
864
}
865
1578
template <> bool Options::wasSetByUser(options::instNoEntail__option_t) const
866
{
867
1578
  return d_holder->instNoEntail__setByUser__;
868
}
869
template <> void Options::set(
870
    options::instWhenPhase__option_t,
871
    const options::instWhenPhase__option_t::type& x)
872
{
873
  d_holder->instWhenPhase = x;
874
}
875
17994
template <> const options::instWhenPhase__option_t::type& Options::operator[](
876
    options::instWhenPhase__option_t) const
877
{
878
17994
  return d_holder->instWhenPhase;
879
}
880
template <> bool Options::wasSetByUser(options::instWhenPhase__option_t) const
881
{
882
  return d_holder->instWhenPhase__setByUser__;
883
}
884
template <> void Options::set(
885
    options::instWhenStrictInterleave__option_t,
886
    const options::instWhenStrictInterleave__option_t::type& x)
887
{
888
  d_holder->instWhenStrictInterleave = x;
889
}
890
9621
template <> const options::instWhenStrictInterleave__option_t::type& Options::operator[](
891
    options::instWhenStrictInterleave__option_t) const
892
{
893
9621
  return d_holder->instWhenStrictInterleave;
894
}
895
template <> bool Options::wasSetByUser(options::instWhenStrictInterleave__option_t) const
896
{
897
  return d_holder->instWhenStrictInterleave__setByUser__;
898
}
899
template <> void Options::set(
900
    options::instWhenTcFirst__option_t,
901
    const options::instWhenTcFirst__option_t::type& x)
902
{
903
  d_holder->instWhenTcFirst = x;
904
}
905
8997
template <> const options::instWhenTcFirst__option_t::type& Options::operator[](
906
    options::instWhenTcFirst__option_t) const
907
{
908
8997
  return d_holder->instWhenTcFirst;
909
}
910
template <> bool Options::wasSetByUser(options::instWhenTcFirst__option_t) const
911
{
912
  return d_holder->instWhenTcFirst__setByUser__;
913
}
914
267
template <> void Options::set(
915
    options::instWhenMode__option_t,
916
    const options::instWhenMode__option_t::type& x)
917
{
918
267
  d_holder->instWhenMode = x;
919
267
}
920
153627
template <> const options::instWhenMode__option_t::type& Options::operator[](
921
    options::instWhenMode__option_t) const
922
{
923
153627
  return d_holder->instWhenMode;
924
}
925
509
template <> bool Options::wasSetByUser(options::instWhenMode__option_t) const
926
{
927
509
  return d_holder->instWhenMode__setByUser__;
928
}
929
10
template <> void Options::set(
930
    options::intWfInduction__option_t,
931
    const options::intWfInduction__option_t::type& x)
932
{
933
10
  d_holder->intWfInduction = x;
934
10
}
935
14531
template <> const options::intWfInduction__option_t::type& Options::operator[](
936
    options::intWfInduction__option_t) const
937
{
938
14531
  return d_holder->intWfInduction;
939
}
940
10
template <> bool Options::wasSetByUser(options::intWfInduction__option_t) const
941
{
942
10
  return d_holder->intWfInduction__setByUser__;
943
}
944
10
template <> void Options::set(
945
    options::iteDtTesterSplitQuant__option_t,
946
    const options::iteDtTesterSplitQuant__option_t::type& x)
947
{
948
10
  d_holder->iteDtTesterSplitQuant = x;
949
10
}
950
207842
template <> const options::iteDtTesterSplitQuant__option_t::type& Options::operator[](
951
    options::iteDtTesterSplitQuant__option_t) const
952
{
953
207842
  return d_holder->iteDtTesterSplitQuant;
954
}
955
10
template <> bool Options::wasSetByUser(options::iteDtTesterSplitQuant__option_t) const
956
{
957
10
  return d_holder->iteDtTesterSplitQuant__setByUser__;
958
}
959
10
template <> void Options::set(
960
    options::iteLiftQuant__option_t,
961
    const options::iteLiftQuant__option_t::type& x)
962
{
963
10
  d_holder->iteLiftQuant = x;
964
10
}
965
299325
template <> const options::iteLiftQuant__option_t::type& Options::operator[](
966
    options::iteLiftQuant__option_t) const
967
{
968
299325
  return d_holder->iteLiftQuant;
969
}
970
10
template <> bool Options::wasSetByUser(options::iteLiftQuant__option_t) const
971
{
972
10
  return d_holder->iteLiftQuant__setByUser__;
973
}
974
8699
template <> const options::literalMatchMode__option_t::type& Options::operator[](
975
    options::literalMatchMode__option_t) const
976
{
977
8699
  return d_holder->literalMatchMode;
978
}
979
template <> bool Options::wasSetByUser(options::literalMatchMode__option_t) const
980
{
981
  return d_holder->literalMatchMode__setByUser__;
982
}
983
1319
template <> void Options::set(
984
    options::macrosQuant__option_t,
985
    const options::macrosQuant__option_t::type& x)
986
{
987
1319
  d_holder->macrosQuant = x;
988
1319
}
989
6648
template <> const options::macrosQuant__option_t::type& Options::operator[](
990
    options::macrosQuant__option_t) const
991
{
992
6648
  return d_holder->macrosQuant;
993
}
994
1319
template <> bool Options::wasSetByUser(options::macrosQuant__option_t) const
995
{
996
1319
  return d_holder->macrosQuant__setByUser__;
997
}
998
56
template <> const options::macrosQuantMode__option_t::type& Options::operator[](
999
    options::macrosQuantMode__option_t) const
1000
{
1001
56
  return d_holder->macrosQuantMode;
1002
}
1003
template <> bool Options::wasSetByUser(options::macrosQuantMode__option_t) const
1004
{
1005
  return d_holder->macrosQuantMode__setByUser__;
1006
}
1007
6016
template <> const options::mbqiInterleave__option_t::type& Options::operator[](
1008
    options::mbqiInterleave__option_t) const
1009
{
1010
6016
  return d_holder->mbqiInterleave;
1011
}
1012
template <> bool Options::wasSetByUser(options::mbqiInterleave__option_t) const
1013
{
1014
  return d_holder->mbqiInterleave__setByUser__;
1015
}
1016
template <> void Options::set(
1017
    options::fmfOneInstPerRound__option_t,
1018
    const options::fmfOneInstPerRound__option_t::type& x)
1019
{
1020
  d_holder->fmfOneInstPerRound = x;
1021
}
1022
5812
template <> const options::fmfOneInstPerRound__option_t::type& Options::operator[](
1023
    options::fmfOneInstPerRound__option_t) const
1024
{
1025
5812
  return d_holder->fmfOneInstPerRound;
1026
}
1027
template <> bool Options::wasSetByUser(options::fmfOneInstPerRound__option_t) const
1028
{
1029
  return d_holder->fmfOneInstPerRound__setByUser__;
1030
}
1031
753
template <> void Options::set(
1032
    options::mbqiMode__option_t,
1033
    const options::mbqiMode__option_t::type& x)
1034
{
1035
753
  d_holder->mbqiMode = x;
1036
753
}
1037
35069
template <> const options::mbqiMode__option_t::type& Options::operator[](
1038
    options::mbqiMode__option_t) const
1039
{
1040
35069
  return d_holder->mbqiMode;
1041
}
1042
611
template <> bool Options::wasSetByUser(options::mbqiMode__option_t) const
1043
{
1044
611
  return d_holder->mbqiMode__setByUser__;
1045
}
1046
1079
template <> void Options::set(
1047
    options::miniscopeQuant__option_t,
1048
    const options::miniscopeQuant__option_t::type& x)
1049
{
1050
1079
  d_holder->miniscopeQuant = x;
1051
1079
}
1052
1577
template <> const options::miniscopeQuant__option_t::type& Options::operator[](
1053
    options::miniscopeQuant__option_t) const
1054
{
1055
1577
  return d_holder->miniscopeQuant;
1056
}
1057
1319
template <> bool Options::wasSetByUser(options::miniscopeQuant__option_t) const
1058
{
1059
1319
  return d_holder->miniscopeQuant__setByUser__;
1060
}
1061
1082
template <> void Options::set(
1062
    options::miniscopeQuantFreeVar__option_t,
1063
    const options::miniscopeQuantFreeVar__option_t::type& x)
1064
{
1065
1082
  d_holder->miniscopeQuantFreeVar = x;
1066
1082
}
1067
1824
template <> const options::miniscopeQuantFreeVar__option_t::type& Options::operator[](
1068
    options::miniscopeQuantFreeVar__option_t) const
1069
{
1070
1824
  return d_holder->miniscopeQuantFreeVar;
1071
}
1072
1319
template <> bool Options::wasSetByUser(options::miniscopeQuantFreeVar__option_t) const
1073
{
1074
1319
  return d_holder->miniscopeQuantFreeVar__setByUser__;
1075
}
1076
1240
template <> const options::multiTriggerCache__option_t::type& Options::operator[](
1077
    options::multiTriggerCache__option_t) const
1078
{
1079
1240
  return d_holder->multiTriggerCache;
1080
}
1081
template <> bool Options::wasSetByUser(options::multiTriggerCache__option_t) const
1082
{
1083
  return d_holder->multiTriggerCache__setByUser__;
1084
}
1085
18625
template <> const options::multiTriggerLinear__option_t::type& Options::operator[](
1086
    options::multiTriggerLinear__option_t) const
1087
{
1088
18625
  return d_holder->multiTriggerLinear;
1089
}
1090
template <> bool Options::wasSetByUser(options::multiTriggerLinear__option_t) const
1091
{
1092
  return d_holder->multiTriggerLinear__setByUser__;
1093
}
1094
8633
template <> const options::multiTriggerPriority__option_t::type& Options::operator[](
1095
    options::multiTriggerPriority__option_t) const
1096
{
1097
8633
  return d_holder->multiTriggerPriority;
1098
}
1099
template <> bool Options::wasSetByUser(options::multiTriggerPriority__option_t) const
1100
{
1101
  return d_holder->multiTriggerPriority__setByUser__;
1102
}
1103
13531
template <> const options::multiTriggerWhenSingle__option_t::type& Options::operator[](
1104
    options::multiTriggerWhenSingle__option_t) const
1105
{
1106
13531
  return d_holder->multiTriggerWhenSingle;
1107
}
1108
template <> bool Options::wasSetByUser(options::multiTriggerWhenSingle__option_t) const
1109
{
1110
  return d_holder->multiTriggerWhenSingle__setByUser__;
1111
}
1112
template <> void Options::set(
1113
    options::partialTriggers__option_t,
1114
    const options::partialTriggers__option_t::type& x)
1115
{
1116
  d_holder->partialTriggers = x;
1117
}
1118
36207
template <> const options::partialTriggers__option_t::type& Options::operator[](
1119
    options::partialTriggers__option_t) const
1120
{
1121
36207
  return d_holder->partialTriggers;
1122
}
1123
template <> bool Options::wasSetByUser(options::partialTriggers__option_t) const
1124
{
1125
  return d_holder->partialTriggers__setByUser__;
1126
}
1127
111
template <> void Options::set(
1128
    options::preSkolemQuant__option_t,
1129
    const options::preSkolemQuant__option_t::type& x)
1130
{
1131
111
  d_holder->preSkolemQuant = x;
1132
111
}
1133
84494
template <> const options::preSkolemQuant__option_t::type& Options::operator[](
1134
    options::preSkolemQuant__option_t) const
1135
{
1136
84494
  return d_holder->preSkolemQuant;
1137
}
1138
111
template <> bool Options::wasSetByUser(options::preSkolemQuant__option_t) const
1139
{
1140
111
  return d_holder->preSkolemQuant__setByUser__;
1141
}
1142
template <> void Options::set(
1143
    options::preSkolemQuantAgg__option_t,
1144
    const options::preSkolemQuantAgg__option_t::type& x)
1145
{
1146
  d_holder->preSkolemQuantAgg = x;
1147
}
1148
14
template <> const options::preSkolemQuantAgg__option_t::type& Options::operator[](
1149
    options::preSkolemQuantAgg__option_t) const
1150
{
1151
14
  return d_holder->preSkolemQuantAgg;
1152
}
1153
template <> bool Options::wasSetByUser(options::preSkolemQuantAgg__option_t) const
1154
{
1155
  return d_holder->preSkolemQuantAgg__setByUser__;
1156
}
1157
92
template <> void Options::set(
1158
    options::preSkolemQuantNested__option_t,
1159
    const options::preSkolemQuantNested__option_t::type& x)
1160
{
1161
92
  d_holder->preSkolemQuantNested = x;
1162
92
}
1163
165
template <> const options::preSkolemQuantNested__option_t::type& Options::operator[](
1164
    options::preSkolemQuantNested__option_t) const
1165
{
1166
165
  return d_holder->preSkolemQuantNested;
1167
}
1168
92
template <> bool Options::wasSetByUser(options::preSkolemQuantNested__option_t) const
1169
{
1170
92
  return d_holder->preSkolemQuantNested__setByUser__;
1171
}
1172
30
template <> void Options::set(
1173
    options::prenexQuantUser__option_t,
1174
    const options::prenexQuantUser__option_t::type& x)
1175
{
1176
30
  d_holder->prenexQuantUser = x;
1177
30
}
1178
1091
template <> const options::prenexQuantUser__option_t::type& Options::operator[](
1179
    options::prenexQuantUser__option_t) const
1180
{
1181
1091
  return d_holder->prenexQuantUser;
1182
}
1183
template <> bool Options::wasSetByUser(options::prenexQuantUser__option_t) const
1184
{
1185
  return d_holder->prenexQuantUser__setByUser__;
1186
}
1187
615
template <> void Options::set(
1188
    options::prenexQuant__option_t,
1189
    const options::prenexQuant__option_t::type& x)
1190
{
1191
615
  d_holder->prenexQuant = x;
1192
615
}
1193
389651
template <> const options::prenexQuant__option_t::type& Options::operator[](
1194
    options::prenexQuant__option_t) const
1195
{
1196
389651
  return d_holder->prenexQuant;
1197
}
1198
615
template <> bool Options::wasSetByUser(options::prenexQuant__option_t) const
1199
{
1200
615
  return d_holder->prenexQuant__setByUser__;
1201
}
1202
18
template <> void Options::set(
1203
    options::purifyTriggers__option_t,
1204
    const options::purifyTriggers__option_t::type& x)
1205
{
1206
18
  d_holder->purifyTriggers = x;
1207
18
}
1208
55794
template <> const options::purifyTriggers__option_t::type& Options::operator[](
1209
    options::purifyTriggers__option_t) const
1210
{
1211
55794
  return d_holder->purifyTriggers;
1212
}
1213
18
template <> bool Options::wasSetByUser(options::purifyTriggers__option_t) const
1214
{
1215
18
  return d_holder->purifyTriggers__setByUser__;
1216
}
1217
template <> void Options::set(
1218
    options::qcfAllConflict__option_t,
1219
    const options::qcfAllConflict__option_t::type& x)
1220
{
1221
  d_holder->qcfAllConflict = x;
1222
}
1223
790
template <> const options::qcfAllConflict__option_t::type& Options::operator[](
1224
    options::qcfAllConflict__option_t) const
1225
{
1226
790
  return d_holder->qcfAllConflict;
1227
}
1228
template <> bool Options::wasSetByUser(options::qcfAllConflict__option_t) const
1229
{
1230
  return d_holder->qcfAllConflict__setByUser__;
1231
}
1232
16739
template <> const options::qcfEagerCheckRd__option_t::type& Options::operator[](
1233
    options::qcfEagerCheckRd__option_t) const
1234
{
1235
16739
  return d_holder->qcfEagerCheckRd;
1236
}
1237
template <> bool Options::wasSetByUser(options::qcfEagerCheckRd__option_t) const
1238
{
1239
  return d_holder->qcfEagerCheckRd__setByUser__;
1240
}
1241
1407357
template <> const options::qcfEagerTest__option_t::type& Options::operator[](
1242
    options::qcfEagerTest__option_t) const
1243
{
1244
1407357
  return d_holder->qcfEagerTest;
1245
}
1246
template <> bool Options::wasSetByUser(options::qcfEagerTest__option_t) const
1247
{
1248
  return d_holder->qcfEagerTest__setByUser__;
1249
}
1250
1429
template <> const options::qcfNestedConflict__option_t::type& Options::operator[](
1251
    options::qcfNestedConflict__option_t) const
1252
{
1253
1429
  return d_holder->qcfNestedConflict;
1254
}
1255
template <> bool Options::wasSetByUser(options::qcfNestedConflict__option_t) const
1256
{
1257
  return d_holder->qcfNestedConflict__setByUser__;
1258
}
1259
16739
template <> const options::qcfSkipRd__option_t::type& Options::operator[](
1260
    options::qcfSkipRd__option_t) const
1261
{
1262
16739
  return d_holder->qcfSkipRd;
1263
}
1264
template <> bool Options::wasSetByUser(options::qcfSkipRd__option_t) const
1265
{
1266
  return d_holder->qcfSkipRd__setByUser__;
1267
}
1268
template <> void Options::set(
1269
    options::qcfTConstraint__option_t,
1270
    const options::qcfTConstraint__option_t::type& x)
1271
{
1272
  d_holder->qcfTConstraint = x;
1273
}
1274
206034
template <> const options::qcfTConstraint__option_t::type& Options::operator[](
1275
    options::qcfTConstraint__option_t) const
1276
{
1277
206034
  return d_holder->qcfTConstraint;
1278
}
1279
template <> bool Options::wasSetByUser(options::qcfTConstraint__option_t) const
1280
{
1281
  return d_holder->qcfTConstraint__setByUser__;
1282
}
1283
373624
template <> const options::qcfVoExp__option_t::type& Options::operator[](
1284
    options::qcfVoExp__option_t) const
1285
{
1286
373624
  return d_holder->qcfVoExp;
1287
}
1288
template <> bool Options::wasSetByUser(options::qcfVoExp__option_t) const
1289
{
1290
  return d_holder->qcfVoExp__setByUser__;
1291
}
1292
6054
template <> const options::quantAlphaEquiv__option_t::type& Options::operator[](
1293
    options::quantAlphaEquiv__option_t) const
1294
{
1295
6054
  return d_holder->quantAlphaEquiv;
1296
}
1297
template <> bool Options::wasSetByUser(options::quantAlphaEquiv__option_t) const
1298
{
1299
  return d_holder->quantAlphaEquiv__setByUser__;
1300
}
1301
1586
template <> void Options::set(
1302
    options::quantConflictFind__option_t,
1303
    const options::quantConflictFind__option_t::type& x)
1304
{
1305
1586
  d_holder->quantConflictFind = x;
1306
1586
}
1307
52916
template <> const options::quantConflictFind__option_t::type& Options::operator[](
1308
    options::quantConflictFind__option_t) const
1309
{
1310
52916
  return d_holder->quantConflictFind;
1311
}
1312
1578
template <> bool Options::wasSetByUser(options::quantConflictFind__option_t) const
1313
{
1314
1578
  return d_holder->quantConflictFind__setByUser__;
1315
}
1316
13571
template <> const options::qcfMode__option_t::type& Options::operator[](
1317
    options::qcfMode__option_t) const
1318
{
1319
13571
  return d_holder->qcfMode;
1320
}
1321
8997
template <> bool Options::wasSetByUser(options::qcfMode__option_t) const
1322
{
1323
8997
  return d_holder->qcfMode__setByUser__;
1324
}
1325
46858
template <> const options::qcfWhenMode__option_t::type& Options::operator[](
1326
    options::qcfWhenMode__option_t) const
1327
{
1328
46858
  return d_holder->qcfWhenMode;
1329
}
1330
template <> bool Options::wasSetByUser(options::qcfWhenMode__option_t) const
1331
{
1332
  return d_holder->qcfWhenMode__setByUser__;
1333
}
1334
4007
template <> void Options::set(
1335
    options::quantDynamicSplit__option_t,
1336
    const options::quantDynamicSplit__option_t::type& x)
1337
{
1338
4007
  d_holder->quantDynamicSplit = x;
1339
4007
}
1340
14368
template <> const options::quantDynamicSplit__option_t::type& Options::operator[](
1341
    options::quantDynamicSplit__option_t) const
1342
{
1343
14368
  return d_holder->quantDynamicSplit;
1344
}
1345
250
template <> bool Options::wasSetByUser(options::quantDynamicSplit__option_t) const
1346
{
1347
250
  return d_holder->quantDynamicSplit__setByUser__;
1348
}
1349
10560
template <> const options::quantFunWellDefined__option_t::type& Options::operator[](
1350
    options::quantFunWellDefined__option_t) const
1351
{
1352
10560
  return d_holder->quantFunWellDefined;
1353
}
1354
template <> bool Options::wasSetByUser(options::quantFunWellDefined__option_t) const
1355
{
1356
  return d_holder->quantFunWellDefined__setByUser__;
1357
}
1358
8997
template <> const options::quantInduction__option_t::type& Options::operator[](
1359
    options::quantInduction__option_t) const
1360
{
1361
8997
  return d_holder->quantInduction;
1362
}
1363
template <> bool Options::wasSetByUser(options::quantInduction__option_t) const
1364
{
1365
  return d_holder->quantInduction__setByUser__;
1366
}
1367
template <> void Options::set(
1368
    options::quantRepMode__option_t,
1369
    const options::quantRepMode__option_t::type& x)
1370
{
1371
  d_holder->quantRepMode = x;
1372
}
1373
121707
template <> const options::quantRepMode__option_t::type& Options::operator[](
1374
    options::quantRepMode__option_t) const
1375
{
1376
121707
  return d_holder->quantRepMode;
1377
}
1378
template <> bool Options::wasSetByUser(options::quantRepMode__option_t) const
1379
{
1380
  return d_holder->quantRepMode__setByUser__;
1381
}
1382
1082
template <> void Options::set(
1383
    options::quantSplit__option_t,
1384
    const options::quantSplit__option_t::type& x)
1385
{
1386
1082
  d_holder->quantSplit = x;
1387
1082
}
1388
41837
template <> const options::quantSplit__option_t::type& Options::operator[](
1389
    options::quantSplit__option_t) const
1390
{
1391
41837
  return d_holder->quantSplit;
1392
}
1393
1319
template <> bool Options::wasSetByUser(options::quantSplit__option_t) const
1394
{
1395
1319
  return d_holder->quantSplit__setByUser__;
1396
}
1397
35139
template <> const options::registerQuantBodyTerms__option_t::type& Options::operator[](
1398
    options::registerQuantBodyTerms__option_t) const
1399
{
1400
35139
  return d_holder->registerQuantBodyTerms;
1401
}
1402
template <> bool Options::wasSetByUser(options::registerQuantBodyTerms__option_t) const
1403
{
1404
  return d_holder->registerQuantBodyTerms__setByUser__;
1405
}
1406
60553
template <> const options::relationalTriggers__option_t::type& Options::operator[](
1407
    options::relationalTriggers__option_t) const
1408
{
1409
60553
  return d_holder->relationalTriggers;
1410
}
1411
template <> bool Options::wasSetByUser(options::relationalTriggers__option_t) const
1412
{
1413
  return d_holder->relationalTriggers__setByUser__;
1414
}
1415
27245
template <> const options::relevantTriggers__option_t::type& Options::operator[](
1416
    options::relevantTriggers__option_t) const
1417
{
1418
27245
  return d_holder->relevantTriggers;
1419
}
1420
template <> bool Options::wasSetByUser(options::relevantTriggers__option_t) const
1421
{
1422
  return d_holder->relevantTriggers__setByUser__;
1423
}
1424
30294
template <> const options::strictTriggers__option_t::type& Options::operator[](
1425
    options::strictTriggers__option_t) const
1426
{
1427
30294
  return d_holder->strictTriggers;
1428
}
1429
template <> bool Options::wasSetByUser(options::strictTriggers__option_t) const
1430
{
1431
  return d_holder->strictTriggers__setByUser__;
1432
}
1433
1319
template <> void Options::set(
1434
    options::sygus__option_t,
1435
    const options::sygus__option_t::type& x)
1436
{
1437
1319
  d_holder->sygus = x;
1438
1319
}
1439
28333
template <> const options::sygus__option_t::type& Options::operator[](
1440
    options::sygus__option_t) const
1441
{
1442
28333
  return d_holder->sygus;
1443
}
1444
template <> bool Options::wasSetByUser(options::sygus__option_t) const
1445
{
1446
  return d_holder->sygus__setByUser__;
1447
}
1448
template <> void Options::set(
1449
    options::sygusActiveGenEnumConsts__option_t,
1450
    const options::sygusActiveGenEnumConsts__option_t::type& x)
1451
{
1452
  d_holder->sygusActiveGenEnumConsts = x;
1453
}
1454
13
template <> const options::sygusActiveGenEnumConsts__option_t::type& Options::operator[](
1455
    options::sygusActiveGenEnumConsts__option_t) const
1456
{
1457
13
  return d_holder->sygusActiveGenEnumConsts;
1458
}
1459
template <> bool Options::wasSetByUser(options::sygusActiveGenEnumConsts__option_t) const
1460
{
1461
  return d_holder->sygusActiveGenEnumConsts__setByUser__;
1462
}
1463
1664
template <> const options::sygusActiveGenMode__option_t::type& Options::operator[](
1464
    options::sygusActiveGenMode__option_t) const
1465
{
1466
1664
  return d_holder->sygusActiveGenMode;
1467
}
1468
template <> bool Options::wasSetByUser(options::sygusActiveGenMode__option_t) const
1469
{
1470
  return d_holder->sygusActiveGenMode__setByUser__;
1471
}
1472
506
template <> const options::sygusAddConstGrammar__option_t::type& Options::operator[](
1473
    options::sygusAddConstGrammar__option_t) const
1474
{
1475
506
  return d_holder->sygusAddConstGrammar;
1476
}
1477
template <> bool Options::wasSetByUser(options::sygusAddConstGrammar__option_t) const
1478
{
1479
  return d_holder->sygusAddConstGrammar__setByUser__;
1480
}
1481
template <> void Options::set(
1482
    options::sygusArgRelevant__option_t,
1483
    const options::sygusArgRelevant__option_t::type& x)
1484
{
1485
  d_holder->sygusArgRelevant = x;
1486
}
1487
506
template <> const options::sygusArgRelevant__option_t::type& Options::operator[](
1488
    options::sygusArgRelevant__option_t) const
1489
{
1490
506
  return d_holder->sygusArgRelevant;
1491
}
1492
template <> bool Options::wasSetByUser(options::sygusArgRelevant__option_t) const
1493
{
1494
  return d_holder->sygusArgRelevant__setByUser__;
1495
}
1496
47
template <> const options::sygusInvAutoUnfold__option_t::type& Options::operator[](
1497
    options::sygusInvAutoUnfold__option_t) const
1498
{
1499
47
  return d_holder->sygusInvAutoUnfold;
1500
}
1501
template <> bool Options::wasSetByUser(options::sygusInvAutoUnfold__option_t) const
1502
{
1503
  return d_holder->sygusInvAutoUnfold__setByUser__;
1504
}
1505
template <> void Options::set(
1506
    options::sygusBoolIteReturnConst__option_t,
1507
    const options::sygusBoolIteReturnConst__option_t::type& x)
1508
{
1509
  d_holder->sygusBoolIteReturnConst = x;
1510
}
1511
23
template <> const options::sygusBoolIteReturnConst__option_t::type& Options::operator[](
1512
    options::sygusBoolIteReturnConst__option_t) const
1513
{
1514
23
  return d_holder->sygusBoolIteReturnConst;
1515
}
1516
template <> bool Options::wasSetByUser(options::sygusBoolIteReturnConst__option_t) const
1517
{
1518
  return d_holder->sygusBoolIteReturnConst__setByUser__;
1519
}
1520
template <> void Options::set(
1521
    options::sygusCoreConnective__option_t,
1522
    const options::sygusCoreConnective__option_t::type& x)
1523
{
1524
  d_holder->sygusCoreConnective = x;
1525
}
1526
11187
template <> const options::sygusCoreConnective__option_t::type& Options::operator[](
1527
    options::sygusCoreConnective__option_t) const
1528
{
1529
11187
  return d_holder->sygusCoreConnective;
1530
}
1531
template <> bool Options::wasSetByUser(options::sygusCoreConnective__option_t) const
1532
{
1533
  return d_holder->sygusCoreConnective__setByUser__;
1534
}
1535
13
template <> const options::sygusConstRepairAbort__option_t::type& Options::operator[](
1536
    options::sygusConstRepairAbort__option_t) const
1537
{
1538
13
  return d_holder->sygusConstRepairAbort;
1539
}
1540
template <> bool Options::wasSetByUser(options::sygusConstRepairAbort__option_t) const
1541
{
1542
  return d_holder->sygusConstRepairAbort__setByUser__;
1543
}
1544
template <> void Options::set(
1545
    options::sygusEvalOpt__option_t,
1546
    const options::sygusEvalOpt__option_t::type& x)
1547
{
1548
  d_holder->sygusEvalOpt = x;
1549
}
1550
196250
template <> const options::sygusEvalOpt__option_t::type& Options::operator[](
1551
    options::sygusEvalOpt__option_t) const
1552
{
1553
196250
  return d_holder->sygusEvalOpt;
1554
}
1555
template <> bool Options::wasSetByUser(options::sygusEvalOpt__option_t) const
1556
{
1557
  return d_holder->sygusEvalOpt__setByUser__;
1558
}
1559
601520
template <> const options::sygusEvalUnfold__option_t::type& Options::operator[](
1560
    options::sygusEvalUnfold__option_t) const
1561
{
1562
601520
  return d_holder->sygusEvalUnfold;
1563
}
1564
template <> bool Options::wasSetByUser(options::sygusEvalUnfold__option_t) const
1565
{
1566
  return d_holder->sygusEvalUnfold__setByUser__;
1567
}
1568
15739
template <> const options::sygusEvalUnfoldBool__option_t::type& Options::operator[](
1569
    options::sygusEvalUnfoldBool__option_t) const
1570
{
1571
15739
  return d_holder->sygusEvalUnfoldBool;
1572
}
1573
template <> bool Options::wasSetByUser(options::sygusEvalUnfoldBool__option_t) const
1574
{
1575
  return d_holder->sygusEvalUnfoldBool__setByUser__;
1576
}
1577
template <> void Options::set(
1578
    options::sygusExprMinerCheckTimeout__option_t,
1579
    const options::sygusExprMinerCheckTimeout__option_t::type& x)
1580
{
1581
  d_holder->sygusExprMinerCheckTimeout = x;
1582
}
1583
template <> const options::sygusExprMinerCheckTimeout__option_t::type& Options::operator[](
1584
    options::sygusExprMinerCheckTimeout__option_t) const
1585
{
1586
  return d_holder->sygusExprMinerCheckTimeout;
1587
}
1588
template <> bool Options::wasSetByUser(options::sygusExprMinerCheckTimeout__option_t) const
1589
{
1590
  return d_holder->sygusExprMinerCheckTimeout__setByUser__;
1591
}
1592
template <> void Options::set(
1593
    options::sygusExtRew__option_t,
1594
    const options::sygusExtRew__option_t::type& x)
1595
{
1596
  d_holder->sygusExtRew = x;
1597
}
1598
321294
template <> const options::sygusExtRew__option_t::type& Options::operator[](
1599
    options::sygusExtRew__option_t) const
1600
{
1601
321294
  return d_holder->sygusExtRew;
1602
}
1603
template <> bool Options::wasSetByUser(options::sygusExtRew__option_t) const
1604
{
1605
  return d_holder->sygusExtRew__setByUser__;
1606
}
1607
template <> void Options::set(
1608
    options::sygusFilterSolRevSubsume__option_t,
1609
    const options::sygusFilterSolRevSubsume__option_t::type& x)
1610
{
1611
  d_holder->sygusFilterSolRevSubsume = x;
1612
}
1613
42
template <> const options::sygusFilterSolRevSubsume__option_t::type& Options::operator[](
1614
    options::sygusFilterSolRevSubsume__option_t) const
1615
{
1616
42
  return d_holder->sygusFilterSolRevSubsume;
1617
}
1618
template <> bool Options::wasSetByUser(options::sygusFilterSolRevSubsume__option_t) const
1619
{
1620
  return d_holder->sygusFilterSolRevSubsume__setByUser__;
1621
}
1622
24
template <> void Options::set(
1623
    options::sygusFilterSolMode__option_t,
1624
    const options::sygusFilterSolMode__option_t::type& x)
1625
{
1626
24
  d_holder->sygusFilterSolMode = x;
1627
24
}
1628
140
template <> const options::sygusFilterSolMode__option_t::type& Options::operator[](
1629
    options::sygusFilterSolMode__option_t) const
1630
{
1631
140
  return d_holder->sygusFilterSolMode;
1632
}
1633
24
template <> bool Options::wasSetByUser(options::sygusFilterSolMode__option_t) const
1634
{
1635
24
  return d_holder->sygusFilterSolMode__setByUser__;
1636
}
1637
template <> void Options::set(
1638
    options::sygusGrammarConsMode__option_t,
1639
    const options::sygusGrammarConsMode__option_t::type& x)
1640
{
1641
  d_holder->sygusGrammarConsMode = x;
1642
}
1643
936
template <> const options::sygusGrammarConsMode__option_t::type& Options::operator[](
1644
    options::sygusGrammarConsMode__option_t) const
1645
{
1646
936
  return d_holder->sygusGrammarConsMode;
1647
}
1648
template <> bool Options::wasSetByUser(options::sygusGrammarConsMode__option_t) const
1649
{
1650
  return d_holder->sygusGrammarConsMode__setByUser__;
1651
}
1652
702
template <> const options::sygusGrammarNorm__option_t::type& Options::operator[](
1653
    options::sygusGrammarNorm__option_t) const
1654
{
1655
702
  return d_holder->sygusGrammarNorm;
1656
}
1657
template <> bool Options::wasSetByUser(options::sygusGrammarNorm__option_t) const
1658
{
1659
  return d_holder->sygusGrammarNorm__setByUser__;
1660
}
1661
template <> void Options::set(
1662
    options::sygusInference__option_t,
1663
    const options::sygusInference__option_t::type& x)
1664
{
1665
  d_holder->sygusInference = x;
1666
}
1667
17812
template <> const options::sygusInference__option_t::type& Options::operator[](
1668
    options::sygusInference__option_t) const
1669
{
1670
17812
  return d_holder->sygusInference;
1671
}
1672
template <> bool Options::wasSetByUser(options::sygusInference__option_t) const
1673
{
1674
  return d_holder->sygusInference__setByUser__;
1675
}
1676
template <> void Options::set(
1677
    options::sygusInst__option_t,
1678
    const options::sygusInst__option_t::type& x)
1679
{
1680
  d_holder->sygusInst = x;
1681
}
1682
25105
template <> const options::sygusInst__option_t::type& Options::operator[](
1683
    options::sygusInst__option_t) const
1684
{
1685
25105
  return d_holder->sygusInst;
1686
}
1687
template <> bool Options::wasSetByUser(options::sygusInst__option_t) const
1688
{
1689
  return d_holder->sygusInst__setByUser__;
1690
}
1691
template <> void Options::set(
1692
    options::sygusInstMode__option_t,
1693
    const options::sygusInstMode__option_t::type& x)
1694
{
1695
  d_holder->sygusInstMode = x;
1696
}
1697
85
template <> const options::sygusInstMode__option_t::type& Options::operator[](
1698
    options::sygusInstMode__option_t) const
1699
{
1700
85
  return d_holder->sygusInstMode;
1701
}
1702
template <> bool Options::wasSetByUser(options::sygusInstMode__option_t) const
1703
{
1704
  return d_holder->sygusInstMode__setByUser__;
1705
}
1706
template <> void Options::set(
1707
    options::sygusInstScope__option_t,
1708
    const options::sygusInstScope__option_t::type& x)
1709
{
1710
  d_holder->sygusInstScope = x;
1711
}
1712
108
template <> const options::sygusInstScope__option_t::type& Options::operator[](
1713
    options::sygusInstScope__option_t) const
1714
{
1715
108
  return d_holder->sygusInstScope;
1716
}
1717
template <> bool Options::wasSetByUser(options::sygusInstScope__option_t) const
1718
{
1719
  return d_holder->sygusInstScope__setByUser__;
1720
}
1721
template <> void Options::set(
1722
    options::sygusInstTermSel__option_t,
1723
    const options::sygusInstTermSel__option_t::type& x)
1724
{
1725
  d_holder->sygusInstTermSel = x;
1726
}
1727
123
template <> const options::sygusInstTermSel__option_t::type& Options::operator[](
1728
    options::sygusInstTermSel__option_t) const
1729
{
1730
123
  return d_holder->sygusInstTermSel;
1731
}
1732
template <> bool Options::wasSetByUser(options::sygusInstTermSel__option_t) const
1733
{
1734
  return d_holder->sygusInstTermSel__setByUser__;
1735
}
1736
template <> void Options::set(
1737
    options::sygusInvTemplWhenSyntax__option_t,
1738
    const options::sygusInvTemplWhenSyntax__option_t::type& x)
1739
{
1740
  d_holder->sygusInvTemplWhenSyntax = x;
1741
}
1742
115
template <> const options::sygusInvTemplWhenSyntax__option_t::type& Options::operator[](
1743
    options::sygusInvTemplWhenSyntax__option_t) const
1744
{
1745
115
  return d_holder->sygusInvTemplWhenSyntax;
1746
}
1747
template <> bool Options::wasSetByUser(options::sygusInvTemplWhenSyntax__option_t) const
1748
{
1749
  return d_holder->sygusInvTemplWhenSyntax__setByUser__;
1750
}
1751
38
template <> void Options::set(
1752
    options::sygusInvTemplMode__option_t,
1753
    const options::sygusInvTemplMode__option_t::type& x)
1754
{
1755
38
  d_holder->sygusInvTemplMode = x;
1756
38
}
1757
506
template <> const options::sygusInvTemplMode__option_t::type& Options::operator[](
1758
    options::sygusInvTemplMode__option_t) const
1759
{
1760
506
  return d_holder->sygusInvTemplMode;
1761
}
1762
38
template <> bool Options::wasSetByUser(options::sygusInvTemplMode__option_t) const
1763
{
1764
38
  return d_holder->sygusInvTemplMode__setByUser__;
1765
}
1766
729
template <> const options::sygusMinGrammar__option_t::type& Options::operator[](
1767
    options::sygusMinGrammar__option_t) const
1768
{
1769
729
  return d_holder->sygusMinGrammar;
1770
}
1771
template <> bool Options::wasSetByUser(options::sygusMinGrammar__option_t) const
1772
{
1773
  return d_holder->sygusMinGrammar__setByUser__;
1774
}
1775
38
template <> void Options::set(
1776
    options::sygusUnifPbe__option_t,
1777
    const options::sygusUnifPbe__option_t::type& x)
1778
{
1779
38
  d_holder->sygusUnifPbe = x;
1780
38
}
1781
383
template <> const options::sygusUnifPbe__option_t::type& Options::operator[](
1782
    options::sygusUnifPbe__option_t) const
1783
{
1784
383
  return d_holder->sygusUnifPbe;
1785
}
1786
38
template <> bool Options::wasSetByUser(options::sygusUnifPbe__option_t) const
1787
{
1788
38
  return d_holder->sygusUnifPbe__setByUser__;
1789
}
1790
template <> void Options::set(
1791
    options::sygusPbeMultiFair__option_t,
1792
    const options::sygusPbeMultiFair__option_t::type& x)
1793
{
1794
  d_holder->sygusPbeMultiFair = x;
1795
}
1796
8070
template <> const options::sygusPbeMultiFair__option_t::type& Options::operator[](
1797
    options::sygusPbeMultiFair__option_t) const
1798
{
1799
8070
  return d_holder->sygusPbeMultiFair;
1800
}
1801
template <> bool Options::wasSetByUser(options::sygusPbeMultiFair__option_t) const
1802
{
1803
  return d_holder->sygusPbeMultiFair__setByUser__;
1804
}
1805
template <> void Options::set(
1806
    options::sygusPbeMultiFairDiff__option_t,
1807
    const options::sygusPbeMultiFairDiff__option_t::type& x)
1808
{
1809
  d_holder->sygusPbeMultiFairDiff = x;
1810
}
1811
891
template <> const options::sygusPbeMultiFairDiff__option_t::type& Options::operator[](
1812
    options::sygusPbeMultiFairDiff__option_t) const
1813
{
1814
891
  return d_holder->sygusPbeMultiFairDiff;
1815
}
1816
template <> bool Options::wasSetByUser(options::sygusPbeMultiFairDiff__option_t) const
1817
{
1818
  return d_holder->sygusPbeMultiFairDiff__setByUser__;
1819
}
1820
1022
template <> const options::sygusQePreproc__option_t::type& Options::operator[](
1821
    options::sygusQePreproc__option_t) const
1822
{
1823
1022
  return d_holder->sygusQePreproc;
1824
}
1825
template <> bool Options::wasSetByUser(options::sygusQePreproc__option_t) const
1826
{
1827
  return d_holder->sygusQePreproc__setByUser__;
1828
}
1829
template <> void Options::set(
1830
    options::sygusQueryGen__option_t,
1831
    const options::sygusQueryGen__option_t::type& x)
1832
{
1833
  d_holder->sygusQueryGen = x;
1834
}
1835
1447
template <> const options::sygusQueryGen__option_t::type& Options::operator[](
1836
    options::sygusQueryGen__option_t) const
1837
{
1838
1447
  return d_holder->sygusQueryGen;
1839
}
1840
template <> bool Options::wasSetByUser(options::sygusQueryGen__option_t) const
1841
{
1842
  return d_holder->sygusQueryGen__setByUser__;
1843
}
1844
template <> void Options::set(
1845
    options::sygusQueryGenCheck__option_t,
1846
    const options::sygusQueryGenCheck__option_t::type& x)
1847
{
1848
  d_holder->sygusQueryGenCheck = x;
1849
}
1850
template <> const options::sygusQueryGenCheck__option_t::type& Options::operator[](
1851
    options::sygusQueryGenCheck__option_t) const
1852
{
1853
  return d_holder->sygusQueryGenCheck;
1854
}
1855
template <> bool Options::wasSetByUser(options::sygusQueryGenCheck__option_t) const
1856
{
1857
  return d_holder->sygusQueryGenCheck__setByUser__;
1858
}
1859
template <> void Options::set(
1860
    options::sygusQueryGenDumpFiles__option_t,
1861
    const options::sygusQueryGenDumpFiles__option_t::type& x)
1862
{
1863
  d_holder->sygusQueryGenDumpFiles = x;
1864
}
1865
template <> const options::sygusQueryGenDumpFiles__option_t::type& Options::operator[](
1866
    options::sygusQueryGenDumpFiles__option_t) const
1867
{
1868
  return d_holder->sygusQueryGenDumpFiles;
1869
}
1870
template <> bool Options::wasSetByUser(options::sygusQueryGenDumpFiles__option_t) const
1871
{
1872
  return d_holder->sygusQueryGenDumpFiles__setByUser__;
1873
}
1874
template <> void Options::set(
1875
    options::sygusQueryGenThresh__option_t,
1876
    const options::sygusQueryGenThresh__option_t::type& x)
1877
{
1878
  d_holder->sygusQueryGenThresh = x;
1879
}
1880
template <> const options::sygusQueryGenThresh__option_t::type& Options::operator[](
1881
    options::sygusQueryGenThresh__option_t) const
1882
{
1883
  return d_holder->sygusQueryGenThresh;
1884
}
1885
template <> bool Options::wasSetByUser(options::sygusQueryGenThresh__option_t) const
1886
{
1887
  return d_holder->sygusQueryGenThresh__setByUser__;
1888
}
1889
166
template <> void Options::set(
1890
    options::sygusRecFun__option_t,
1891
    const options::sygusRecFun__option_t::type& x)
1892
{
1893
166
  d_holder->sygusRecFun = x;
1894
166
}
1895
249879
template <> const options::sygusRecFun__option_t::type& Options::operator[](
1896
    options::sygusRecFun__option_t) const
1897
{
1898
249879
  return d_holder->sygusRecFun;
1899
}
1900
template <> bool Options::wasSetByUser(options::sygusRecFun__option_t) const
1901
{
1902
  return d_holder->sygusRecFun__setByUser__;
1903
}
1904
template <> void Options::set(
1905
    options::sygusRecFunEvalLimit__option_t,
1906
    const options::sygusRecFunEvalLimit__option_t::type& x)
1907
{
1908
  d_holder->sygusRecFunEvalLimit = x;
1909
}
1910
6420
template <> const options::sygusRecFunEvalLimit__option_t::type& Options::operator[](
1911
    options::sygusRecFunEvalLimit__option_t) const
1912
{
1913
6420
  return d_holder->sygusRecFunEvalLimit;
1914
}
1915
template <> bool Options::wasSetByUser(options::sygusRecFunEvalLimit__option_t) const
1916
{
1917
  return d_holder->sygusRecFunEvalLimit__setByUser__;
1918
}
1919
template <> void Options::set(
1920
    options::sygusRepairConst__option_t,
1921
    const options::sygusRepairConst__option_t::type& x)
1922
{
1923
  d_holder->sygusRepairConst = x;
1924
}
1925
58795
template <> const options::sygusRepairConst__option_t::type& Options::operator[](
1926
    options::sygusRepairConst__option_t) const
1927
{
1928
58795
  return d_holder->sygusRepairConst;
1929
}
1930
template <> bool Options::wasSetByUser(options::sygusRepairConst__option_t) const
1931
{
1932
  return d_holder->sygusRepairConst__setByUser__;
1933
}
1934
template <> void Options::set(
1935
    options::sygusRepairConstTimeout__option_t,
1936
    const options::sygusRepairConstTimeout__option_t::type& x)
1937
{
1938
  d_holder->sygusRepairConstTimeout = x;
1939
}
1940
237
template <> const options::sygusRepairConstTimeout__option_t::type& Options::operator[](
1941
    options::sygusRepairConstTimeout__option_t) const
1942
{
1943
237
  return d_holder->sygusRepairConstTimeout;
1944
}
1945
237
template <> bool Options::wasSetByUser(options::sygusRepairConstTimeout__option_t) const
1946
{
1947
237
  return d_holder->sygusRepairConstTimeout__setByUser__;
1948
}
1949
1319
template <> const options::sygusRew__option_t::type& Options::operator[](
1950
    options::sygusRew__option_t) const
1951
{
1952
1319
  return d_holder->sygusRew;
1953
}
1954
template <> bool Options::wasSetByUser(options::sygusRew__option_t) const
1955
{
1956
  return d_holder->sygusRew__setByUser__;
1957
}
1958
6
template <> void Options::set(
1959
    options::sygusRewSynth__option_t,
1960
    const options::sygusRewSynth__option_t::type& x)
1961
{
1962
6
  d_holder->sygusRewSynth = x;
1963
6
}
1964
2832
template <> const options::sygusRewSynth__option_t::type& Options::operator[](
1965
    options::sygusRewSynth__option_t) const
1966
{
1967
2832
  return d_holder->sygusRewSynth;
1968
}
1969
template <> bool Options::wasSetByUser(options::sygusRewSynth__option_t) const
1970
{
1971
  return d_holder->sygusRewSynth__setByUser__;
1972
}
1973
template <> void Options::set(
1974
    options::sygusRewSynthAccel__option_t,
1975
    const options::sygusRewSynthAccel__option_t::type& x)
1976
{
1977
  d_holder->sygusRewSynthAccel = x;
1978
}
1979
12
template <> const options::sygusRewSynthAccel__option_t::type& Options::operator[](
1980
    options::sygusRewSynthAccel__option_t) const
1981
{
1982
12
  return d_holder->sygusRewSynthAccel;
1983
}
1984
template <> bool Options::wasSetByUser(options::sygusRewSynthAccel__option_t) const
1985
{
1986
  return d_holder->sygusRewSynthAccel__setByUser__;
1987
}
1988
template <> void Options::set(
1989
    options::sygusRewSynthCheck__option_t,
1990
    const options::sygusRewSynthCheck__option_t::type& x)
1991
{
1992
  d_holder->sygusRewSynthCheck = x;
1993
}
1994
5543
template <> const options::sygusRewSynthCheck__option_t::type& Options::operator[](
1995
    options::sygusRewSynthCheck__option_t) const
1996
{
1997
5543
  return d_holder->sygusRewSynthCheck;
1998
}
1999
template <> bool Options::wasSetByUser(options::sygusRewSynthCheck__option_t) const
2000
{
2001
  return d_holder->sygusRewSynthCheck__setByUser__;
2002
}
2003
template <> void Options::set(
2004
    options::sygusRewSynthFilterCong__option_t,
2005
    const options::sygusRewSynthFilterCong__option_t::type& x)
2006
{
2007
  d_holder->sygusRewSynthFilterCong = x;
2008
}
2009
1179
template <> const options::sygusRewSynthFilterCong__option_t::type& Options::operator[](
2010
    options::sygusRewSynthFilterCong__option_t) const
2011
{
2012
1179
  return d_holder->sygusRewSynthFilterCong;
2013
}
2014
template <> bool Options::wasSetByUser(options::sygusRewSynthFilterCong__option_t) const
2015
{
2016
  return d_holder->sygusRewSynthFilterCong__setByUser__;
2017
}
2018
template <> void Options::set(
2019
    options::sygusRewSynthFilterMatch__option_t,
2020
    const options::sygusRewSynthFilterMatch__option_t::type& x)
2021
{
2022
  d_holder->sygusRewSynthFilterMatch = x;
2023
}
2024
312
template <> const options::sygusRewSynthFilterMatch__option_t::type& Options::operator[](
2025
    options::sygusRewSynthFilterMatch__option_t) const
2026
{
2027
312
  return d_holder->sygusRewSynthFilterMatch;
2028
}
2029
template <> bool Options::wasSetByUser(options::sygusRewSynthFilterMatch__option_t) const
2030
{
2031
  return d_holder->sygusRewSynthFilterMatch__setByUser__;
2032
}
2033
template <> void Options::set(
2034
    options::sygusRewSynthFilterNonLinear__option_t,
2035
    const options::sygusRewSynthFilterNonLinear__option_t::type& x)
2036
{
2037
  d_holder->sygusRewSynthFilterNonLinear = x;
2038
}
2039
626
template <> const options::sygusRewSynthFilterNonLinear__option_t::type& Options::operator[](
2040
    options::sygusRewSynthFilterNonLinear__option_t) const
2041
{
2042
626
  return d_holder->sygusRewSynthFilterNonLinear;
2043
}
2044
template <> bool Options::wasSetByUser(options::sygusRewSynthFilterNonLinear__option_t) const
2045
{
2046
  return d_holder->sygusRewSynthFilterNonLinear__setByUser__;
2047
}
2048
template <> void Options::set(
2049
    options::sygusRewSynthFilterOrder__option_t,
2050
    const options::sygusRewSynthFilterOrder__option_t::type& x)
2051
{
2052
  d_holder->sygusRewSynthFilterOrder = x;
2053
}
2054
939
template <> const options::sygusRewSynthFilterOrder__option_t::type& Options::operator[](
2055
    options::sygusRewSynthFilterOrder__option_t) const
2056
{
2057
939
  return d_holder->sygusRewSynthFilterOrder;
2058
}
2059
template <> bool Options::wasSetByUser(options::sygusRewSynthFilterOrder__option_t) const
2060
{
2061
  return d_holder->sygusRewSynthFilterOrder__setByUser__;
2062
}
2063
template <> void Options::set(
2064
    options::sygusRewSynthInput__option_t,
2065
    const options::sygusRewSynthInput__option_t::type& x)
2066
{
2067
  d_holder->sygusRewSynthInput = x;
2068
}
2069
16159
template <> const options::sygusRewSynthInput__option_t::type& Options::operator[](
2070
    options::sygusRewSynthInput__option_t) const
2071
{
2072
16159
  return d_holder->sygusRewSynthInput;
2073
}
2074
template <> bool Options::wasSetByUser(options::sygusRewSynthInput__option_t) const
2075
{
2076
  return d_holder->sygusRewSynthInput__setByUser__;
2077
}
2078
template <> void Options::set(
2079
    options::sygusRewSynthInputNVars__option_t,
2080
    const options::sygusRewSynthInputNVars__option_t::type& x)
2081
{
2082
  d_holder->sygusRewSynthInputNVars = x;
2083
}
2084
template <> const options::sygusRewSynthInputNVars__option_t::type& Options::operator[](
2085
    options::sygusRewSynthInputNVars__option_t) const
2086
{
2087
  return d_holder->sygusRewSynthInputNVars;
2088
}
2089
template <> bool Options::wasSetByUser(options::sygusRewSynthInputNVars__option_t) const
2090
{
2091
  return d_holder->sygusRewSynthInputNVars__setByUser__;
2092
}
2093
template <> void Options::set(
2094
    options::sygusRewSynthInputUseBool__option_t,
2095
    const options::sygusRewSynthInputUseBool__option_t::type& x)
2096
{
2097
  d_holder->sygusRewSynthInputUseBool = x;
2098
}
2099
template <> const options::sygusRewSynthInputUseBool__option_t::type& Options::operator[](
2100
    options::sygusRewSynthInputUseBool__option_t) const
2101
{
2102
  return d_holder->sygusRewSynthInputUseBool;
2103
}
2104
template <> bool Options::wasSetByUser(options::sygusRewSynthInputUseBool__option_t) const
2105
{
2106
  return d_holder->sygusRewSynthInputUseBool__setByUser__;
2107
}
2108
template <> void Options::set(
2109
    options::sygusRewSynthRec__option_t,
2110
    const options::sygusRewSynthRec__option_t::type& x)
2111
{
2112
  d_holder->sygusRewSynthRec = x;
2113
}
2114
1377
template <> const options::sygusRewSynthRec__option_t::type& Options::operator[](
2115
    options::sygusRewSynthRec__option_t) const
2116
{
2117
1377
  return d_holder->sygusRewSynthRec;
2118
}
2119
template <> bool Options::wasSetByUser(options::sygusRewSynthRec__option_t) const
2120
{
2121
  return d_holder->sygusRewSynthRec__setByUser__;
2122
}
2123
6
template <> void Options::set(
2124
    options::sygusRewVerify__option_t,
2125
    const options::sygusRewVerify__option_t::type& x)
2126
{
2127
6
  d_holder->sygusRewVerify = x;
2128
6
}
2129
72854
template <> const options::sygusRewVerify__option_t::type& Options::operator[](
2130
    options::sygusRewVerify__option_t) const
2131
{
2132
72854
  return d_holder->sygusRewVerify;
2133
}
2134
template <> bool Options::wasSetByUser(options::sygusRewVerify__option_t) const
2135
{
2136
  return d_holder->sygusRewVerify__setByUser__;
2137
}
2138
template <> void Options::set(
2139
    options::sygusRewVerifyAbort__option_t,
2140
    const options::sygusRewVerifyAbort__option_t::type& x)
2141
{
2142
  d_holder->sygusRewVerifyAbort = x;
2143
}
2144
template <> const options::sygusRewVerifyAbort__option_t::type& Options::operator[](
2145
    options::sygusRewVerifyAbort__option_t) const
2146
{
2147
  return d_holder->sygusRewVerifyAbort;
2148
}
2149
template <> bool Options::wasSetByUser(options::sygusRewVerifyAbort__option_t) const
2150
{
2151
  return d_holder->sygusRewVerifyAbort__setByUser__;
2152
}
2153
template <> void Options::set(
2154
    options::sygusSampleFpUniform__option_t,
2155
    const options::sygusSampleFpUniform__option_t::type& x)
2156
{
2157
  d_holder->sygusSampleFpUniform = x;
2158
}
2159
template <> const options::sygusSampleFpUniform__option_t::type& Options::operator[](
2160
    options::sygusSampleFpUniform__option_t) const
2161
{
2162
  return d_holder->sygusSampleFpUniform;
2163
}
2164
template <> bool Options::wasSetByUser(options::sygusSampleFpUniform__option_t) const
2165
{
2166
  return d_holder->sygusSampleFpUniform__setByUser__;
2167
}
2168
536359
template <> const options::sygusSampleGrammar__option_t::type& Options::operator[](
2169
    options::sygusSampleGrammar__option_t) const
2170
{
2171
536359
  return d_holder->sygusSampleGrammar;
2172
}
2173
template <> bool Options::wasSetByUser(options::sygusSampleGrammar__option_t) const
2174
{
2175
  return d_holder->sygusSampleGrammar__setByUser__;
2176
}
2177
template <> void Options::set(
2178
    options::sygusSamples__option_t,
2179
    const options::sygusSamples__option_t::type& x)
2180
{
2181
  d_holder->sygusSamples = x;
2182
}
2183
28
template <> const options::sygusSamples__option_t::type& Options::operator[](
2184
    options::sygusSamples__option_t) const
2185
{
2186
28
  return d_holder->sygusSamples;
2187
}
2188
template <> bool Options::wasSetByUser(options::sygusSamples__option_t) const
2189
{
2190
  return d_holder->sygusSamples__setByUser__;
2191
}
2192
376
template <> const options::cegqiSingleInvAbort__option_t::type& Options::operator[](
2193
    options::cegqiSingleInvAbort__option_t) const
2194
{
2195
376
  return d_holder->cegqiSingleInvAbort;
2196
}
2197
template <> bool Options::wasSetByUser(options::cegqiSingleInvAbort__option_t) const
2198
{
2199
  return d_holder->cegqiSingleInvAbort__setByUser__;
2200
}
2201
template <> const options::cegqiSingleInvPartial__option_t::type& Options::operator[](
2202
    options::cegqiSingleInvPartial__option_t) const
2203
{
2204
  return d_holder->cegqiSingleInvPartial;
2205
}
2206
template <> bool Options::wasSetByUser(options::cegqiSingleInvPartial__option_t) const
2207
{
2208
  return d_holder->cegqiSingleInvPartial__setByUser__;
2209
}
2210
15
template <> const options::cegqiSingleInvReconstructLimit__option_t::type& Options::operator[](
2211
    options::cegqiSingleInvReconstructLimit__option_t) const
2212
{
2213
15
  return d_holder->cegqiSingleInvReconstructLimit;
2214
}
2215
template <> bool Options::wasSetByUser(options::cegqiSingleInvReconstructLimit__option_t) const
2216
{
2217
  return d_holder->cegqiSingleInvReconstructLimit__setByUser__;
2218
}
2219
template <> void Options::set(
2220
    options::cegqiSingleInvReconstruct__option_t,
2221
    const options::cegqiSingleInvReconstruct__option_t::type& x)
2222
{
2223
  d_holder->cegqiSingleInvReconstruct = x;
2224
}
2225
195
template <> const options::cegqiSingleInvReconstruct__option_t::type& Options::operator[](
2226
    options::cegqiSingleInvReconstruct__option_t) const
2227
{
2228
195
  return d_holder->cegqiSingleInvReconstruct;
2229
}
2230
template <> bool Options::wasSetByUser(options::cegqiSingleInvReconstruct__option_t) const
2231
{
2232
  return d_holder->cegqiSingleInvReconstruct__setByUser__;
2233
}
2234
27
template <> const options::cegqiSingleInvReconstructConst__option_t::type& Options::operator[](
2235
    options::cegqiSingleInvReconstructConst__option_t) const
2236
{
2237
27
  return d_holder->cegqiSingleInvReconstructConst;
2238
}
2239
template <> bool Options::wasSetByUser(options::cegqiSingleInvReconstructConst__option_t) const
2240
{
2241
  return d_holder->cegqiSingleInvReconstructConst__setByUser__;
2242
}
2243
1145
template <> void Options::set(
2244
    options::cegqiSingleInvMode__option_t,
2245
    const options::cegqiSingleInvMode__option_t::type& x)
2246
{
2247
1145
  d_holder->cegqiSingleInvMode = x;
2248
1145
}
2249
875
template <> const options::cegqiSingleInvMode__option_t::type& Options::operator[](
2250
    options::cegqiSingleInvMode__option_t) const
2251
{
2252
875
  return d_holder->cegqiSingleInvMode;
2253
}
2254
1357
template <> bool Options::wasSetByUser(options::cegqiSingleInvMode__option_t) const
2255
{
2256
1357
  return d_holder->cegqiSingleInvMode__setByUser__;
2257
}
2258
8
template <> void Options::set(
2259
    options::sygusStream__option_t,
2260
    const options::sygusStream__option_t::type& x)
2261
{
2262
8
  d_holder->sygusStream = x;
2263
8
}
2264
3377
template <> const options::sygusStream__option_t::type& Options::operator[](
2265
    options::sygusStream__option_t) const
2266
{
2267
3377
  return d_holder->sygusStream;
2268
}
2269
template <> bool Options::wasSetByUser(options::sygusStream__option_t) const
2270
{
2271
  return d_holder->sygusStream__setByUser__;
2272
}
2273
111
template <> const options::sygusTemplEmbedGrammar__option_t::type& Options::operator[](
2274
    options::sygusTemplEmbedGrammar__option_t) const
2275
{
2276
111
  return d_holder->sygusTemplEmbedGrammar;
2277
}
2278
template <> bool Options::wasSetByUser(options::sygusTemplEmbedGrammar__option_t) const
2279
{
2280
  return d_holder->sygusTemplEmbedGrammar__setByUser__;
2281
}
2282
template <> void Options::set(
2283
    options::sygusUnifCondIndNoRepeatSol__option_t,
2284
    const options::sygusUnifCondIndNoRepeatSol__option_t::type& x)
2285
{
2286
  d_holder->sygusUnifCondIndNoRepeatSol = x;
2287
}
2288
template <> const options::sygusUnifCondIndNoRepeatSol__option_t::type& Options::operator[](
2289
    options::sygusUnifCondIndNoRepeatSol__option_t) const
2290
{
2291
  return d_holder->sygusUnifCondIndNoRepeatSol;
2292
}
2293
template <> bool Options::wasSetByUser(options::sygusUnifCondIndNoRepeatSol__option_t) const
2294
{
2295
  return d_holder->sygusUnifCondIndNoRepeatSol__setByUser__;
2296
}
2297
template <> void Options::set(
2298
    options::sygusUnifPi__option_t,
2299
    const options::sygusUnifPi__option_t::type& x)
2300
{
2301
  d_holder->sygusUnifPi = x;
2302
}
2303
4907
template <> const options::sygusUnifPi__option_t::type& Options::operator[](
2304
    options::sygusUnifPi__option_t) const
2305
{
2306
4907
  return d_holder->sygusUnifPi;
2307
}
2308
38
template <> bool Options::wasSetByUser(options::sygusUnifPi__option_t) const
2309
{
2310
38
  return d_holder->sygusUnifPi__setByUser__;
2311
}
2312
template <> void Options::set(
2313
    options::sygusUnifShuffleCond__option_t,
2314
    const options::sygusUnifShuffleCond__option_t::type& x)
2315
{
2316
  d_holder->sygusUnifShuffleCond = x;
2317
}
2318
template <> const options::sygusUnifShuffleCond__option_t::type& Options::operator[](
2319
    options::sygusUnifShuffleCond__option_t) const
2320
{
2321
  return d_holder->sygusUnifShuffleCond;
2322
}
2323
template <> bool Options::wasSetByUser(options::sygusUnifShuffleCond__option_t) const
2324
{
2325
  return d_holder->sygusUnifShuffleCond__setByUser__;
2326
}
2327
template <> void Options::set(
2328
    options::termDbCd__option_t,
2329
    const options::termDbCd__option_t::type& x)
2330
{
2331
  d_holder->termDbCd = x;
2332
}
2333
141922
template <> const options::termDbCd__option_t::type& Options::operator[](
2334
    options::termDbCd__option_t) const
2335
{
2336
141922
  return d_holder->termDbCd;
2337
}
2338
template <> bool Options::wasSetByUser(options::termDbCd__option_t) const
2339
{
2340
  return d_holder->termDbCd__setByUser__;
2341
}
2342
template <> void Options::set(
2343
    options::termDbMode__option_t,
2344
    const options::termDbMode__option_t::type& x)
2345
{
2346
  d_holder->termDbMode = x;
2347
}
2348
4751715
template <> const options::termDbMode__option_t::type& Options::operator[](
2349
    options::termDbMode__option_t) const
2350
{
2351
4751715
  return d_holder->termDbMode;
2352
}
2353
template <> bool Options::wasSetByUser(options::termDbMode__option_t) const
2354
{
2355
  return d_holder->termDbMode__setByUser__;
2356
}
2357
template <> void Options::set(
2358
    options::triggerActiveSelMode__option_t,
2359
    const options::triggerActiveSelMode__option_t::type& x)
2360
{
2361
  d_holder->triggerActiveSelMode = x;
2362
}
2363
27605
template <> const options::triggerActiveSelMode__option_t::type& Options::operator[](
2364
    options::triggerActiveSelMode__option_t) const
2365
{
2366
27605
  return d_holder->triggerActiveSelMode;
2367
}
2368
template <> bool Options::wasSetByUser(options::triggerActiveSelMode__option_t) const
2369
{
2370
  return d_holder->triggerActiveSelMode__setByUser__;
2371
}
2372
template <> void Options::set(
2373
    options::triggerSelMode__option_t,
2374
    const options::triggerSelMode__option_t::type& x)
2375
{
2376
  d_holder->triggerSelMode = x;
2377
}
2378
5825
template <> const options::triggerSelMode__option_t::type& Options::operator[](
2379
    options::triggerSelMode__option_t) const
2380
{
2381
5825
  return d_holder->triggerSelMode;
2382
}
2383
template <> bool Options::wasSetByUser(options::triggerSelMode__option_t) const
2384
{
2385
  return d_holder->triggerSelMode__setByUser__;
2386
}
2387
template <> void Options::set(
2388
    options::userPatternsQuant__option_t,
2389
    const options::userPatternsQuant__option_t::type& x)
2390
{
2391
  d_holder->userPatternsQuant = x;
2392
}
2393
364348
template <> const options::userPatternsQuant__option_t::type& Options::operator[](
2394
    options::userPatternsQuant__option_t) const
2395
{
2396
364348
  return d_holder->userPatternsQuant;
2397
}
2398
template <> bool Options::wasSetByUser(options::userPatternsQuant__option_t) const
2399
{
2400
  return d_holder->userPatternsQuant__setByUser__;
2401
}
2402
517871
template <> const options::varElimQuant__option_t::type& Options::operator[](
2403
    options::varElimQuant__option_t) const
2404
{
2405
517871
  return d_holder->varElimQuant;
2406
}
2407
template <> bool Options::wasSetByUser(options::varElimQuant__option_t) const
2408
{
2409
  return d_holder->varElimQuant__setByUser__;
2410
}
2411
96219
template <> const options::varIneqElimQuant__option_t::type& Options::operator[](
2412
    options::varIneqElimQuant__option_t) const
2413
{
2414
96219
  return d_holder->varIneqElimQuant;
2415
}
2416
template <> bool Options::wasSetByUser(options::varIneqElimQuant__option_t) const
2417
{
2418
  return d_holder->varIneqElimQuant__setByUser__;
2419
}
2420
2421
2422
namespace options {
2423
2424
thread_local struct aggressiveMiniscopeQuant__option_t aggressiveMiniscopeQuant;
2425
thread_local struct cegisSample__option_t cegisSample;
2426
thread_local struct cegqi__option_t cegqi;
2427
thread_local struct cegqiAll__option_t cegqiAll;
2428
thread_local struct cegqiBv__option_t cegqiBv;
2429
thread_local struct cegqiBvConcInv__option_t cegqiBvConcInv;
2430
thread_local struct cegqiBvIneqMode__option_t cegqiBvIneqMode;
2431
thread_local struct cegqiBvInterleaveValue__option_t cegqiBvInterleaveValue;
2432
thread_local struct cegqiBvLinearize__option_t cegqiBvLinearize;
2433
thread_local struct cegqiBvRmExtract__option_t cegqiBvRmExtract;
2434
thread_local struct cegqiBvSolveNl__option_t cegqiBvSolveNl;
2435
thread_local struct cegqiFullEffort__option_t cegqiFullEffort;
2436
thread_local struct cegqiInnermost__option_t cegqiInnermost;
2437
thread_local struct cegqiMidpoint__option_t cegqiMidpoint;
2438
thread_local struct cegqiMinBounds__option_t cegqiMinBounds;
2439
thread_local struct cegqiModel__option_t cegqiModel;
2440
thread_local struct cegqiMultiInst__option_t cegqiMultiInst;
2441
thread_local struct cegqiNestedQE__option_t cegqiNestedQE;
2442
thread_local struct cegqiNopt__option_t cegqiNopt;
2443
thread_local struct cegqiRepeatLit__option_t cegqiRepeatLit;
2444
thread_local struct cegqiRoundUpLowerLia__option_t cegqiRoundUpLowerLia;
2445
thread_local struct cegqiSat__option_t cegqiSat;
2446
thread_local struct cegqiUseInfInt__option_t cegqiUseInfInt;
2447
thread_local struct cegqiUseInfReal__option_t cegqiUseInfReal;
2448
thread_local struct condVarSplitQuantAgg__option_t condVarSplitQuantAgg;
2449
thread_local struct condVarSplitQuant__option_t condVarSplitQuant;
2450
thread_local struct conjectureFilterActiveTerms__option_t conjectureFilterActiveTerms;
2451
thread_local struct conjectureFilterCanonical__option_t conjectureFilterCanonical;
2452
thread_local struct conjectureFilterModel__option_t conjectureFilterModel;
2453
thread_local struct conjectureGen__option_t conjectureGen;
2454
thread_local struct conjectureGenGtEnum__option_t conjectureGenGtEnum;
2455
thread_local struct conjectureGenMaxDepth__option_t conjectureGenMaxDepth;
2456
thread_local struct conjectureGenPerRound__option_t conjectureGenPerRound;
2457
thread_local struct conjectureUeeIntro__option_t conjectureUeeIntro;
2458
thread_local struct conjectureNoFilter__option_t conjectureNoFilter;
2459
thread_local struct debugInst__option_t debugInst;
2460
thread_local struct debugSygus__option_t debugSygus;
2461
thread_local struct dtStcInduction__option_t dtStcInduction;
2462
thread_local struct dtVarExpandQuant__option_t dtVarExpandQuant;
2463
thread_local struct eMatching__option_t eMatching;
2464
thread_local struct elimTautQuant__option_t elimTautQuant;
2465
thread_local struct extRewriteQuant__option_t extRewriteQuant;
2466
thread_local struct finiteModelFind__option_t finiteModelFind;
2467
thread_local struct fmfBound__option_t fmfBound;
2468
thread_local struct fmfBoundInt__option_t fmfBoundInt;
2469
thread_local struct fmfBoundLazy__option_t fmfBoundLazy;
2470
thread_local struct fmfFmcSimple__option_t fmfFmcSimple;
2471
thread_local struct fmfFreshDistConst__option_t fmfFreshDistConst;
2472
thread_local struct fmfFunWellDefined__option_t fmfFunWellDefined;
2473
thread_local struct fmfFunWellDefinedRelevant__option_t fmfFunWellDefinedRelevant;
2474
thread_local struct fmfInstEngine__option_t fmfInstEngine;
2475
thread_local struct fmfTypeCompletionThresh__option_t fmfTypeCompletionThresh;
2476
thread_local struct fullSaturateInterleave__option_t fullSaturateInterleave;
2477
thread_local struct fullSaturateStratify__option_t fullSaturateStratify;
2478
thread_local struct fullSaturateSum__option_t fullSaturateSum;
2479
thread_local struct fullSaturateQuant__option_t fullSaturateQuant;
2480
thread_local struct fullSaturateLimit__option_t fullSaturateLimit;
2481
thread_local struct fullSaturateQuantRd__option_t fullSaturateQuantRd;
2482
thread_local struct globalNegate__option_t globalNegate;
2483
thread_local struct hoElim__option_t hoElim;
2484
thread_local struct hoElimStoreAx__option_t hoElimStoreAx;
2485
thread_local struct hoMatching__option_t hoMatching;
2486
thread_local struct hoMatchingVarArgPriority__option_t hoMatchingVarArgPriority;
2487
thread_local struct hoMergeTermDb__option_t hoMergeTermDb;
2488
thread_local struct incrementTriggers__option_t incrementTriggers;
2489
thread_local struct instLevelInputOnly__option_t instLevelInputOnly;
2490
thread_local struct instMaxLevel__option_t instMaxLevel;
2491
thread_local struct instNoEntail__option_t instNoEntail;
2492
thread_local struct instWhenPhase__option_t instWhenPhase;
2493
thread_local struct instWhenStrictInterleave__option_t instWhenStrictInterleave;
2494
thread_local struct instWhenTcFirst__option_t instWhenTcFirst;
2495
thread_local struct instWhenMode__option_t instWhenMode;
2496
thread_local struct intWfInduction__option_t intWfInduction;
2497
thread_local struct iteDtTesterSplitQuant__option_t iteDtTesterSplitQuant;
2498
thread_local struct iteLiftQuant__option_t iteLiftQuant;
2499
thread_local struct literalMatchMode__option_t literalMatchMode;
2500
thread_local struct macrosQuant__option_t macrosQuant;
2501
thread_local struct macrosQuantMode__option_t macrosQuantMode;
2502
thread_local struct mbqiInterleave__option_t mbqiInterleave;
2503
thread_local struct fmfOneInstPerRound__option_t fmfOneInstPerRound;
2504
thread_local struct mbqiMode__option_t mbqiMode;
2505
thread_local struct miniscopeQuant__option_t miniscopeQuant;
2506
thread_local struct miniscopeQuantFreeVar__option_t miniscopeQuantFreeVar;
2507
thread_local struct multiTriggerCache__option_t multiTriggerCache;
2508
thread_local struct multiTriggerLinear__option_t multiTriggerLinear;
2509
thread_local struct multiTriggerPriority__option_t multiTriggerPriority;
2510
thread_local struct multiTriggerWhenSingle__option_t multiTriggerWhenSingle;
2511
thread_local struct partialTriggers__option_t partialTriggers;
2512
thread_local struct preSkolemQuant__option_t preSkolemQuant;
2513
thread_local struct preSkolemQuantAgg__option_t preSkolemQuantAgg;
2514
thread_local struct preSkolemQuantNested__option_t preSkolemQuantNested;
2515
thread_local struct prenexQuantUser__option_t prenexQuantUser;
2516
thread_local struct prenexQuant__option_t prenexQuant;
2517
thread_local struct purifyTriggers__option_t purifyTriggers;
2518
thread_local struct qcfAllConflict__option_t qcfAllConflict;
2519
thread_local struct qcfEagerCheckRd__option_t qcfEagerCheckRd;
2520
thread_local struct qcfEagerTest__option_t qcfEagerTest;
2521
thread_local struct qcfNestedConflict__option_t qcfNestedConflict;
2522
thread_local struct qcfSkipRd__option_t qcfSkipRd;
2523
thread_local struct qcfTConstraint__option_t qcfTConstraint;
2524
thread_local struct qcfVoExp__option_t qcfVoExp;
2525
thread_local struct quantAlphaEquiv__option_t quantAlphaEquiv;
2526
thread_local struct quantConflictFind__option_t quantConflictFind;
2527
thread_local struct qcfMode__option_t qcfMode;
2528
thread_local struct qcfWhenMode__option_t qcfWhenMode;
2529
thread_local struct quantDynamicSplit__option_t quantDynamicSplit;
2530
thread_local struct quantFunWellDefined__option_t quantFunWellDefined;
2531
thread_local struct quantInduction__option_t quantInduction;
2532
thread_local struct quantRepMode__option_t quantRepMode;
2533
thread_local struct quantSplit__option_t quantSplit;
2534
thread_local struct registerQuantBodyTerms__option_t registerQuantBodyTerms;
2535
thread_local struct relationalTriggers__option_t relationalTriggers;
2536
thread_local struct relevantTriggers__option_t relevantTriggers;
2537
thread_local struct strictTriggers__option_t strictTriggers;
2538
thread_local struct sygus__option_t sygus;
2539
thread_local struct sygusActiveGenEnumConsts__option_t sygusActiveGenEnumConsts;
2540
thread_local struct sygusActiveGenMode__option_t sygusActiveGenMode;
2541
thread_local struct sygusAddConstGrammar__option_t sygusAddConstGrammar;
2542
thread_local struct sygusArgRelevant__option_t sygusArgRelevant;
2543
thread_local struct sygusInvAutoUnfold__option_t sygusInvAutoUnfold;
2544
thread_local struct sygusBoolIteReturnConst__option_t sygusBoolIteReturnConst;
2545
thread_local struct sygusCoreConnective__option_t sygusCoreConnective;
2546
thread_local struct sygusConstRepairAbort__option_t sygusConstRepairAbort;
2547
thread_local struct sygusEvalOpt__option_t sygusEvalOpt;
2548
thread_local struct sygusEvalUnfold__option_t sygusEvalUnfold;
2549
thread_local struct sygusEvalUnfoldBool__option_t sygusEvalUnfoldBool;
2550
thread_local struct sygusExprMinerCheckTimeout__option_t sygusExprMinerCheckTimeout;
2551
thread_local struct sygusExtRew__option_t sygusExtRew;
2552
thread_local struct sygusFilterSolRevSubsume__option_t sygusFilterSolRevSubsume;
2553
thread_local struct sygusFilterSolMode__option_t sygusFilterSolMode;
2554
thread_local struct sygusGrammarConsMode__option_t sygusGrammarConsMode;
2555
thread_local struct sygusGrammarNorm__option_t sygusGrammarNorm;
2556
thread_local struct sygusInference__option_t sygusInference;
2557
thread_local struct sygusInst__option_t sygusInst;
2558
thread_local struct sygusInstMode__option_t sygusInstMode;
2559
thread_local struct sygusInstScope__option_t sygusInstScope;
2560
thread_local struct sygusInstTermSel__option_t sygusInstTermSel;
2561
thread_local struct sygusInvTemplWhenSyntax__option_t sygusInvTemplWhenSyntax;
2562
thread_local struct sygusInvTemplMode__option_t sygusInvTemplMode;
2563
thread_local struct sygusMinGrammar__option_t sygusMinGrammar;
2564
thread_local struct sygusUnifPbe__option_t sygusUnifPbe;
2565
thread_local struct sygusPbeMultiFair__option_t sygusPbeMultiFair;
2566
thread_local struct sygusPbeMultiFairDiff__option_t sygusPbeMultiFairDiff;
2567
thread_local struct sygusQePreproc__option_t sygusQePreproc;
2568
thread_local struct sygusQueryGen__option_t sygusQueryGen;
2569
thread_local struct sygusQueryGenCheck__option_t sygusQueryGenCheck;
2570
thread_local struct sygusQueryGenDumpFiles__option_t sygusQueryGenDumpFiles;
2571
thread_local struct sygusQueryGenThresh__option_t sygusQueryGenThresh;
2572
thread_local struct sygusRecFun__option_t sygusRecFun;
2573
thread_local struct sygusRecFunEvalLimit__option_t sygusRecFunEvalLimit;
2574
thread_local struct sygusRepairConst__option_t sygusRepairConst;
2575
thread_local struct sygusRepairConstTimeout__option_t sygusRepairConstTimeout;
2576
thread_local struct sygusRew__option_t sygusRew;
2577
thread_local struct sygusRewSynth__option_t sygusRewSynth;
2578
thread_local struct sygusRewSynthAccel__option_t sygusRewSynthAccel;
2579
thread_local struct sygusRewSynthCheck__option_t sygusRewSynthCheck;
2580
thread_local struct sygusRewSynthFilterCong__option_t sygusRewSynthFilterCong;
2581
thread_local struct sygusRewSynthFilterMatch__option_t sygusRewSynthFilterMatch;
2582
thread_local struct sygusRewSynthFilterNonLinear__option_t sygusRewSynthFilterNonLinear;
2583
thread_local struct sygusRewSynthFilterOrder__option_t sygusRewSynthFilterOrder;
2584
thread_local struct sygusRewSynthInput__option_t sygusRewSynthInput;
2585
thread_local struct sygusRewSynthInputNVars__option_t sygusRewSynthInputNVars;
2586
thread_local struct sygusRewSynthInputUseBool__option_t sygusRewSynthInputUseBool;
2587
thread_local struct sygusRewSynthRec__option_t sygusRewSynthRec;
2588
thread_local struct sygusRewVerify__option_t sygusRewVerify;
2589
thread_local struct sygusRewVerifyAbort__option_t sygusRewVerifyAbort;
2590
thread_local struct sygusSampleFpUniform__option_t sygusSampleFpUniform;
2591
thread_local struct sygusSampleGrammar__option_t sygusSampleGrammar;
2592
thread_local struct sygusSamples__option_t sygusSamples;
2593
thread_local struct cegqiSingleInvAbort__option_t cegqiSingleInvAbort;
2594
thread_local struct cegqiSingleInvPartial__option_t cegqiSingleInvPartial;
2595
thread_local struct cegqiSingleInvReconstructLimit__option_t cegqiSingleInvReconstructLimit;
2596
thread_local struct cegqiSingleInvReconstruct__option_t cegqiSingleInvReconstruct;
2597
thread_local struct cegqiSingleInvReconstructConst__option_t cegqiSingleInvReconstructConst;
2598
thread_local struct cegqiSingleInvMode__option_t cegqiSingleInvMode;
2599
thread_local struct sygusStream__option_t sygusStream;
2600
thread_local struct sygusTemplEmbedGrammar__option_t sygusTemplEmbedGrammar;
2601
thread_local struct sygusUnifCondIndNoRepeatSol__option_t sygusUnifCondIndNoRepeatSol;
2602
thread_local struct sygusUnifPi__option_t sygusUnifPi;
2603
thread_local struct sygusUnifShuffleCond__option_t sygusUnifShuffleCond;
2604
thread_local struct termDbCd__option_t termDbCd;
2605
thread_local struct termDbMode__option_t termDbMode;
2606
thread_local struct triggerActiveSelMode__option_t triggerActiveSelMode;
2607
thread_local struct triggerSelMode__option_t triggerSelMode;
2608
thread_local struct userPatternsQuant__option_t userPatternsQuant;
2609
thread_local struct varElimQuant__option_t varElimQuant;
2610
thread_local struct varIneqElimQuant__option_t varIneqElimQuant;
2611
2612
2613
std::ostream&
2614
operator<<(std::ostream& os, CegisSampleMode mode)
2615
{
2616
  os << "CegisSampleMode::";
2617
  switch(mode) {
2618
    case CegisSampleMode::TRUST:
2619
      os << "TRUST";
2620
      break;
2621
    case CegisSampleMode::NONE:
2622
      os << "NONE";
2623
      break;
2624
    case CegisSampleMode::USE:
2625
      os << "USE";
2626
      break;
2627
    default:
2628
        Unreachable();
2629
  }
2630
  return os;
2631
}
2632
2633
CegisSampleMode
2634
5
stringToCegisSampleMode(const std::string& option, const std::string& optarg)
2635
{
2636
5
  if (optarg == "trust")
2637
  {
2638
1
    return CegisSampleMode::TRUST;
2639
  }
2640
4
  else if (optarg == "none")
2641
  {
2642
    return CegisSampleMode::NONE;
2643
  }
2644
4
  else if (optarg == "use")
2645
  {
2646
4
    return CegisSampleMode::USE;
2647
  }
2648
  else if (optarg == "help")
2649
  {
2650
    puts("Modes for sampling with counterexample-guided inductive synthesis (CEGIS).\n"
2651
         "Available modes for --cegis-sample are:\n"
2652
         "+ trust\n"
2653
         "  Trust that when a solution for a conjecture is always true under sampling,\n"
2654
         "  then it is indeed a solution. Note this option may print out spurious\n"
2655
         "  solutions for synthesis conjectures.\n"
2656
         "+ none (default)\n"
2657
         "  Do not use sampling with CEGIS.\n"
2658
         "+ use\n"
2659
         "  Use sampling to accelerate CEGIS. This will rule out solutions for a\n"
2660
         "  conjecture when they are not satisfied by a sample point.\n");
2661
    exit(1);
2662
  }
2663
  else
2664
  {
2665
    throw OptionException(std::string("unknown option for --cegis-sample: `") +
2666
                          optarg + "'.  Try --cegis-sample=help.");
2667
  }
2668
}
2669
2670
std::ostream&
2671
operator<<(std::ostream& os, CegqiBvIneqMode mode)
2672
{
2673
  os << "CegqiBvIneqMode::";
2674
  switch(mode) {
2675
    case CegqiBvIneqMode::KEEP:
2676
      os << "KEEP";
2677
      break;
2678
    case CegqiBvIneqMode::EQ_BOUNDARY:
2679
      os << "EQ_BOUNDARY";
2680
      break;
2681
    case CegqiBvIneqMode::EQ_SLACK:
2682
      os << "EQ_SLACK";
2683
      break;
2684
    default:
2685
        Unreachable();
2686
  }
2687
  return os;
2688
}
2689
2690
CegqiBvIneqMode
2691
82
stringToCegqiBvIneqMode(const std::string& option, const std::string& optarg)
2692
{
2693
82
  if (optarg == "keep")
2694
  {
2695
79
    return CegqiBvIneqMode::KEEP;
2696
  }
2697
3
  else if (optarg == "eq-boundary")
2698
  {
2699
3
    return CegqiBvIneqMode::EQ_BOUNDARY;
2700
  }
2701
  else if (optarg == "eq-slack")
2702
  {
2703
    return CegqiBvIneqMode::EQ_SLACK;
2704
  }
2705
  else if (optarg == "help")
2706
  {
2707
    puts("Modes for handling bit-vector inequalities in counterexample-guided\n"
2708
         "instantiation.\n"
2709
         "Available modes for --cegqi-bv-ineq are:\n"
2710
         "+ keep\n"
2711
         "  Solve for the inequality directly using side conditions for invertibility.\n"
2712
         "+ eq-boundary (default)\n"
2713
         "  Solve for the boundary point of the inequality, e.g., t > s becomes t = s+1.\n"
2714
         "+ eq-slack\n"
2715
         "  Solve for the inequality using the slack value in the model, e.g., t > s\n"
2716
         "  becomes t = s + ( t-s )^M.\n");
2717
    exit(1);
2718
  }
2719
  else
2720
  {
2721
    throw OptionException(std::string("unknown option for --cegqi-bv-ineq: `") +
2722
                          optarg + "'.  Try --cegqi-bv-ineq=help.");
2723
  }
2724
}
2725
2726
std::ostream&
2727
operator<<(std::ostream& os, InstWhenMode mode)
2728
{
2729
  os << "InstWhenMode::";
2730
  switch(mode) {
2731
    case InstWhenMode::FULL:
2732
      os << "FULL";
2733
      break;
2734
    case InstWhenMode::LAST_CALL:
2735
      os << "LAST_CALL";
2736
      break;
2737
    case InstWhenMode::FULL_LAST_CALL:
2738
      os << "FULL_LAST_CALL";
2739
      break;
2740
    case InstWhenMode::FULL_DELAY_LAST_CALL:
2741
      os << "FULL_DELAY_LAST_CALL";
2742
      break;
2743
    case InstWhenMode::FULL_DELAY:
2744
      os << "FULL_DELAY";
2745
      break;
2746
    case InstWhenMode::PRE_FULL:
2747
      os << "PRE_FULL";
2748
      break;
2749
    default:
2750
        Unreachable();
2751
  }
2752
  return os;
2753
}
2754
2755
InstWhenMode
2756
3
stringToInstWhenMode(const std::string& option, const std::string& optarg)
2757
{
2758
3
  if (optarg == "full")
2759
  {
2760
3
    return InstWhenMode::FULL;
2761
  }
2762
  else if (optarg == "last-call")
2763
  {
2764
    return InstWhenMode::LAST_CALL;
2765
  }
2766
  else if (optarg == "full-last-call")
2767
  {
2768
    return InstWhenMode::FULL_LAST_CALL;
2769
  }
2770
  else if (optarg == "full-delay-last-call")
2771
  {
2772
    return InstWhenMode::FULL_DELAY_LAST_CALL;
2773
  }
2774
  else if (optarg == "full-delay")
2775
  {
2776
    return InstWhenMode::FULL_DELAY;
2777
  }
2778
  else if (optarg == "pre-full")
2779
  {
2780
    return InstWhenMode::PRE_FULL;
2781
  }
2782
  else if (optarg == "help")
2783
  {
2784
    puts("Instantiation modes.\n"
2785
         "Available modes for --inst-when are:\n"
2786
         "+ full\n"
2787
         "  Run instantiation round at full effort, before theory combination.\n"
2788
         "+ last-call\n"
2789
         "  Run instantiation at last call effort, after theory combination and and\n"
2790
         "  theories report sat.\n"
2791
         "+ full-last-call (default)\n"
2792
         "  Alternate running instantiation rounds at full effort and last call.  In other\n"
2793
         "  words, interleave instantiation and theory combination.\n"
2794
         "+ full-delay-last-call\n"
2795
         "  Alternate running instantiation rounds at full effort after all other theories\n"
2796
         "  have finished, and last call.\n"
2797
         "+ full-delay\n"
2798
         "  Run instantiation round at full effort, before theory combination, after all\n"
2799
         "  other theories have finished.\n"
2800
         "+ pre-full\n"
2801
         "  Run instantiation round before full effort (possibly at standard effort).\n");
2802
    exit(1);
2803
  }
2804
  else
2805
  {
2806
    throw OptionException(std::string("unknown option for --inst-when: `") +
2807
                          optarg + "'.  Try --inst-when=help.");
2808
  }
2809
}
2810
2811
std::ostream&
2812
operator<<(std::ostream& os, IteLiftQuantMode mode)
2813
{
2814
  os << "IteLiftQuantMode::";
2815
  switch(mode) {
2816
    case IteLiftQuantMode::ALL:
2817
      os << "ALL";
2818
      break;
2819
    case IteLiftQuantMode::SIMPLE:
2820
      os << "SIMPLE";
2821
      break;
2822
    case IteLiftQuantMode::NONE:
2823
      os << "NONE";
2824
      break;
2825
    default:
2826
        Unreachable();
2827
  }
2828
  return os;
2829
}
2830
2831
IteLiftQuantMode
2832
stringToIteLiftQuantMode(const std::string& option, const std::string& optarg)
2833
{
2834
  if (optarg == "all")
2835
  {
2836
    return IteLiftQuantMode::ALL;
2837
  }
2838
  else if (optarg == "simple")
2839
  {
2840
    return IteLiftQuantMode::SIMPLE;
2841
  }
2842
  else if (optarg == "none")
2843
  {
2844
    return IteLiftQuantMode::NONE;
2845
  }
2846
  else if (optarg == "help")
2847
  {
2848
    puts("ITE lifting modes for quantified formulas.\n"
2849
         "Available modes for --ite-lift-quant are:\n"
2850
         "+ all\n"
2851
         "  Lift if-then-else in quantified formulas.\n"
2852
         "+ simple (default)\n"
2853
         "  Lift if-then-else in quantified formulas if results in smaller term size.\n"
2854
         "+ none\n"
2855
         "  Do not lift if-then-else in quantified formulas.\n");
2856
    exit(1);
2857
  }
2858
  else
2859
  {
2860
    throw OptionException(std::string("unknown option for --ite-lift-quant: `") +
2861
                          optarg + "'.  Try --ite-lift-quant=help.");
2862
  }
2863
}
2864
2865
std::ostream&
2866
operator<<(std::ostream& os, LiteralMatchMode mode)
2867
{
2868
  os << "LiteralMatchMode::";
2869
  switch(mode) {
2870
    case LiteralMatchMode::AGG_PREDICATE:
2871
      os << "AGG_PREDICATE";
2872
      break;
2873
    case LiteralMatchMode::AGG:
2874
      os << "AGG";
2875
      break;
2876
    case LiteralMatchMode::NONE:
2877
      os << "NONE";
2878
      break;
2879
    case LiteralMatchMode::USE:
2880
      os << "USE";
2881
      break;
2882
    default:
2883
        Unreachable();
2884
  }
2885
  return os;
2886
}
2887
2888
LiteralMatchMode
2889
stringToLiteralMatchMode(const std::string& option, const std::string& optarg)
2890
{
2891
  if (optarg == "agg-predicate")
2892
  {
2893
    return LiteralMatchMode::AGG_PREDICATE;
2894
  }
2895
  else if (optarg == "agg")
2896
  {
2897
    return LiteralMatchMode::AGG;
2898
  }
2899
  else if (optarg == "none")
2900
  {
2901
    return LiteralMatchMode::NONE;
2902
  }
2903
  else if (optarg == "use")
2904
  {
2905
    return LiteralMatchMode::USE;
2906
  }
2907
  else if (optarg == "help")
2908
  {
2909
    puts("Literal match modes.\n"
2910
         "Available modes for --literal-matching are:\n"
2911
         "+ agg-predicate\n"
2912
         "  Consider phase requirements aggressively for predicates. In the above example,\n"
2913
         "  only match P( x ) with terms that are in the equivalence class of false.\n"
2914
         "+ agg\n"
2915
         "  Consider the phase requirements aggressively for all triggers.\n"
2916
         "+ none\n"
2917
         "  Do not use literal matching.\n"
2918
         "+ use (default)\n"
2919
         "  Consider phase requirements of triggers conservatively. For example, the\n"
2920
         "  trigger P( x ) in forall( x ). ( P( x ) V ~Q( x ) ) will not be matched with\n"
2921
         "  terms in the equivalence class of true, and likewise Q( x ) will not be\n"
2922
         "  matched terms in the equivalence class of false. Extends to equality.\n");
2923
    exit(1);
2924
  }
2925
  else
2926
  {
2927
    throw OptionException(std::string("unknown option for --literal-matching: `") +
2928
                          optarg + "'.  Try --literal-matching=help.");
2929
  }
2930
}
2931
2932
std::ostream&
2933
operator<<(std::ostream& os, MacrosQuantMode mode)
2934
{
2935
  os << "MacrosQuantMode::";
2936
  switch(mode) {
2937
    case MacrosQuantMode::ALL:
2938
      os << "ALL";
2939
      break;
2940
    case MacrosQuantMode::GROUND_UF:
2941
      os << "GROUND_UF";
2942
      break;
2943
    case MacrosQuantMode::GROUND:
2944
      os << "GROUND";
2945
      break;
2946
    default:
2947
        Unreachable();
2948
  }
2949
  return os;
2950
}
2951
2952
MacrosQuantMode
2953
2
stringToMacrosQuantMode(const std::string& option, const std::string& optarg)
2954
{
2955
2
  if (optarg == "all")
2956
  {
2957
    return MacrosQuantMode::ALL;
2958
  }
2959
2
  else if (optarg == "ground-uf")
2960
  {
2961
    return MacrosQuantMode::GROUND_UF;
2962
  }
2963
2
  else if (optarg == "ground")
2964
  {
2965
2
    return MacrosQuantMode::GROUND;
2966
  }
2967
  else if (optarg == "help")
2968
  {
2969
    puts("Modes for quantifiers macro expansion.\n"
2970
         "Available modes for --macros-quant-mode are:\n"
2971
         "+ all\n"
2972
         "  Infer definitions for functions, including those containing quantified\n"
2973
         "  formulas.\n"
2974
         "+ ground-uf (default)\n"
2975
         "  Only infer ground definitions for functions that result in triggers for all\n"
2976
         "  free variables.\n"
2977
         "+ ground\n"
2978
         "  Only infer ground definitions for functions.\n");
2979
    exit(1);
2980
  }
2981
  else
2982
  {
2983
    throw OptionException(std::string("unknown option for --macros-quant-mode: `") +
2984
                          optarg + "'.  Try --macros-quant-mode=help.");
2985
  }
2986
}
2987
2988
std::ostream&
2989
operator<<(std::ostream& os, MbqiMode mode)
2990
{
2991
  os << "MbqiMode::";
2992
  switch(mode) {
2993
    case MbqiMode::TRUST:
2994
      os << "TRUST";
2995
      break;
2996
    case MbqiMode::NONE:
2997
      os << "NONE";
2998
      break;
2999
    case MbqiMode::FMC:
3000
      os << "FMC";
3001
      break;
3002
    default:
3003
        Unreachable();
3004
  }
3005
  return os;
3006
}
3007
3008
MbqiMode
3009
stringToMbqiMode(const std::string& option, const std::string& optarg)
3010
{
3011
  if (optarg == "trust")
3012
  {
3013
    return MbqiMode::TRUST;
3014
  }
3015
  else if (optarg == "none")
3016
  {
3017
    return MbqiMode::NONE;
3018
  }
3019
  else if (optarg == "fmc")
3020
  {
3021
    return MbqiMode::FMC;
3022
  }
3023
  else if (optarg == "help")
3024
  {
3025
    puts("Model-based quantifier instantiation modes.\n"
3026
         "Available modes for --mbqi are:\n"
3027
         "+ trust\n"
3028
         "  Do not instantiate quantified formulas (incomplete technique).\n"
3029
         "+ none\n"
3030
         "  Disable model-based quantifier instantiation.\n"
3031
         "+ fmc (default)\n"
3032
         "  Use algorithm from Section 5.4.2 of thesis Finite Model Finding in\n"
3033
         "  Satisfiability Modulo Theories.\n");
3034
    exit(1);
3035
  }
3036
  else
3037
  {
3038
    throw OptionException(std::string("unknown option for --mbqi: `") +
3039
                          optarg + "'.  Try --mbqi=help.");
3040
  }
3041
}
3042
3043
std::ostream&
3044
operator<<(std::ostream& os, PrenexQuantMode mode)
3045
{
3046
  os << "PrenexQuantMode::";
3047
  switch(mode) {
3048
    case PrenexQuantMode::NORMAL:
3049
      os << "NORMAL";
3050
      break;
3051
    case PrenexQuantMode::SIMPLE:
3052
      os << "SIMPLE";
3053
      break;
3054
    case PrenexQuantMode::NONE:
3055
      os << "NONE";
3056
      break;
3057
    default:
3058
        Unreachable();
3059
  }
3060
  return os;
3061
}
3062
3063
PrenexQuantMode
3064
stringToPrenexQuantMode(const std::string& option, const std::string& optarg)
3065
{
3066
  if (optarg == "norm")
3067
  {
3068
    return PrenexQuantMode::NORMAL;
3069
  }
3070
  else if (optarg == "simple")
3071
  {
3072
    return PrenexQuantMode::SIMPLE;
3073
  }
3074
  else if (optarg == "none")
3075
  {
3076
    return PrenexQuantMode::NONE;
3077
  }
3078
  else if (optarg == "help")
3079
  {
3080
    puts("Prenex quantifiers modes.\n"
3081
         "Available modes for --prenex-quant are:\n"
3082
         "+ norm\n"
3083
         "  Prenex to prenex normal form.\n"
3084
         "+ simple (default)\n"
3085
         "  Do simple prenexing of same sign quantifiers.\n"
3086
         "+ none\n"
3087
         "  Do no prenex nested quantifiers.\n");
3088
    exit(1);
3089
  }
3090
  else
3091
  {
3092
    throw OptionException(std::string("unknown option for --prenex-quant: `") +
3093
                          optarg + "'.  Try --prenex-quant=help.");
3094
  }
3095
}
3096
3097
std::ostream&
3098
operator<<(std::ostream& os, QcfMode mode)
3099
{
3100
  os << "QcfMode::";
3101
  switch(mode) {
3102
    case QcfMode::CONFLICT_ONLY:
3103
      os << "CONFLICT_ONLY";
3104
      break;
3105
    case QcfMode::PARTIAL:
3106
      os << "PARTIAL";
3107
      break;
3108
    case QcfMode::PROP_EQ:
3109
      os << "PROP_EQ";
3110
      break;
3111
    default:
3112
        Unreachable();
3113
  }
3114
  return os;
3115
}
3116
3117
QcfMode
3118
stringToQcfMode(const std::string& option, const std::string& optarg)
3119
{
3120
  if (optarg == "conflict")
3121
  {
3122
    return QcfMode::CONFLICT_ONLY;
3123
  }
3124
  else if (optarg == "partial")
3125
  {
3126
    return QcfMode::PARTIAL;
3127
  }
3128
  else if (optarg == "prop-eq")
3129
  {
3130
    return QcfMode::PROP_EQ;
3131
  }
3132
  else if (optarg == "help")
3133
  {
3134
    puts("Quantifier conflict find modes.\n"
3135
         "Available modes for --quant-cf-mode are:\n"
3136
         "+ conflict\n"
3137
         "  Apply QCF algorithm to find conflicts only.\n"
3138
         "+ partial\n"
3139
         "  Use QCF for conflicts, propagations and heuristic instantiations.\n"
3140
         "+ prop-eq (default)\n"
3141
         "  Apply QCF algorithm to propagate equalities as well as conflicts.\n");
3142
    exit(1);
3143
  }
3144
  else
3145
  {
3146
    throw OptionException(std::string("unknown option for --quant-cf-mode: `") +
3147
                          optarg + "'.  Try --quant-cf-mode=help.");
3148
  }
3149
}
3150
3151
std::ostream&
3152
operator<<(std::ostream& os, QcfWhenMode mode)
3153
{
3154
  os << "QcfWhenMode::";
3155
  switch(mode) {
3156
    case QcfWhenMode::STD:
3157
      os << "STD";
3158
      break;
3159
    case QcfWhenMode::LAST_CALL:
3160
      os << "LAST_CALL";
3161
      break;
3162
    case QcfWhenMode::DEFAULT:
3163
      os << "DEFAULT";
3164
      break;
3165
    case QcfWhenMode::STD_H:
3166
      os << "STD_H";
3167
      break;
3168
    default:
3169
        Unreachable();
3170
  }
3171
  return os;
3172
}
3173
3174
QcfWhenMode
3175
stringToQcfWhenMode(const std::string& option, const std::string& optarg)
3176
{
3177
  if (optarg == "std")
3178
  {
3179
    return QcfWhenMode::STD;
3180
  }
3181
  else if (optarg == "last-call")
3182
  {
3183
    return QcfWhenMode::LAST_CALL;
3184
  }
3185
  else if (optarg == "default")
3186
  {
3187
    return QcfWhenMode::DEFAULT;
3188
  }
3189
  else if (optarg == "std-h")
3190
  {
3191
    return QcfWhenMode::STD_H;
3192
  }
3193
  else if (optarg == "help")
3194
  {
3195
    puts("Quantifier conflict find modes.\n"
3196
         "Available modes for --quant-cf-when are:\n"
3197
         "+ std\n"
3198
         "  Apply conflict finding at standard effort.\n"
3199
         "+ last-call\n"
3200
         "  Apply conflict finding at last call, after theory combination and and all\n"
3201
         "  theories report sat.\n"
3202
         "+ default\n"
3203
         "  Default, apply conflict finding at full effort.\n"
3204
         "+ std-h\n"
3205
         "  Apply conflict finding at standard effort when heuristic says to.\n");
3206
    exit(1);
3207
  }
3208
  else
3209
  {
3210
    throw OptionException(std::string("unknown option for --quant-cf-when: `") +
3211
                          optarg + "'.  Try --quant-cf-when=help.");
3212
  }
3213
}
3214
3215
std::ostream&
3216
operator<<(std::ostream& os, QuantDSplitMode mode)
3217
{
3218
  os << "QuantDSplitMode::";
3219
  switch(mode) {
3220
    case QuantDSplitMode::AGG:
3221
      os << "AGG";
3222
      break;
3223
    case QuantDSplitMode::DEFAULT:
3224
      os << "DEFAULT";
3225
      break;
3226
    case QuantDSplitMode::NONE:
3227
      os << "NONE";
3228
      break;
3229
    default:
3230
        Unreachable();
3231
  }
3232
  return os;
3233
}
3234
3235
QuantDSplitMode
3236
stringToQuantDSplitMode(const std::string& option, const std::string& optarg)
3237
{
3238
  if (optarg == "agg")
3239
  {
3240
    return QuantDSplitMode::AGG;
3241
  }
3242
  else if (optarg == "default")
3243
  {
3244
    return QuantDSplitMode::DEFAULT;
3245
  }
3246
  else if (optarg == "none")
3247
  {
3248
    return QuantDSplitMode::NONE;
3249
  }
3250
  else if (optarg == "help")
3251
  {
3252
    puts("Modes for quantifiers splitting.\n"
3253
         "Available modes for --quant-dsplit-mode are:\n"
3254
         "+ agg\n"
3255
         "  Aggressively split quantified formulas.\n"
3256
         "+ default\n"
3257
         "  Split quantified formulas over some finite datatypes when finite model finding\n"
3258
         "  is enabled.\n"
3259
         "+ none\n"
3260
         "  Never split quantified formulas.\n");
3261
    exit(1);
3262
  }
3263
  else
3264
  {
3265
    throw OptionException(std::string("unknown option for --quant-dsplit-mode: `") +
3266
                          optarg + "'.  Try --quant-dsplit-mode=help.");
3267
  }
3268
}
3269
3270
std::ostream&
3271
operator<<(std::ostream& os, QuantRepMode mode)
3272
{
3273
  os << "QuantRepMode::";
3274
  switch(mode) {
3275
    case QuantRepMode::FIRST:
3276
      os << "FIRST";
3277
      break;
3278
    case QuantRepMode::EE:
3279
      os << "EE";
3280
      break;
3281
    case QuantRepMode::DEPTH:
3282
      os << "DEPTH";
3283
      break;
3284
    default:
3285
        Unreachable();
3286
  }
3287
  return os;
3288
}
3289
3290
QuantRepMode
3291
stringToQuantRepMode(const std::string& option, const std::string& optarg)
3292
{
3293
  if (optarg == "first")
3294
  {
3295
    return QuantRepMode::FIRST;
3296
  }
3297
  else if (optarg == "ee")
3298
  {
3299
    return QuantRepMode::EE;
3300
  }
3301
  else if (optarg == "depth")
3302
  {
3303
    return QuantRepMode::DEPTH;
3304
  }
3305
  else if (optarg == "help")
3306
  {
3307
    puts("Modes for quantifiers representative selection.\n"
3308
         "Available modes for --quant-rep-mode are:\n"
3309
         "+ first (default)\n"
3310
         "  Choose terms that appear first.\n"
3311
         "+ ee\n"
3312
         "  Let equality engine choose representatives.\n"
3313
         "+ depth\n"
3314
         "  Choose terms that are of minimal depth.\n");
3315
    exit(1);
3316
  }
3317
  else
3318
  {
3319
    throw OptionException(std::string("unknown option for --quant-rep-mode: `") +
3320
                          optarg + "'.  Try --quant-rep-mode=help.");
3321
  }
3322
}
3323
3324
std::ostream&
3325
operator<<(std::ostream& os, SygusActiveGenMode mode)
3326
{
3327
  os << "SygusActiveGenMode::";
3328
  switch(mode) {
3329
    case SygusActiveGenMode::AUTO:
3330
      os << "AUTO";
3331
      break;
3332
    case SygusActiveGenMode::ENUM_BASIC:
3333
      os << "ENUM_BASIC";
3334
      break;
3335
    case SygusActiveGenMode::VAR_AGNOSTIC:
3336
      os << "VAR_AGNOSTIC";
3337
      break;
3338
    case SygusActiveGenMode::NONE:
3339
      os << "NONE";
3340
      break;
3341
    case SygusActiveGenMode::ENUM:
3342
      os << "ENUM";
3343
      break;
3344
    default:
3345
        Unreachable();
3346
  }
3347
  return os;
3348
}
3349
3350
SygusActiveGenMode
3351
20
stringToSygusActiveGenMode(const std::string& option, const std::string& optarg)
3352
{
3353
20
  if (optarg == "auto")
3354
  {
3355
    return SygusActiveGenMode::AUTO;
3356
  }
3357
20
  else if (optarg == "basic")
3358
  {
3359
    return SygusActiveGenMode::ENUM_BASIC;
3360
  }
3361
20
  else if (optarg == "var-agnostic")
3362
  {
3363
2
    return SygusActiveGenMode::VAR_AGNOSTIC;
3364
  }
3365
18
  else if (optarg == "none")
3366
  {
3367
6
    return SygusActiveGenMode::NONE;
3368
  }
3369
12
  else if (optarg == "enum")
3370
  {
3371
12
    return SygusActiveGenMode::ENUM;
3372
  }
3373
  else if (optarg == "help")
3374
  {
3375
    puts("Modes for actively-generated sygus enumerators.\n"
3376
         "Available modes for --sygus-active-gen are:\n"
3377
         "+ auto (default)\n"
3378
         "  Internally decide the best policy for each enumerator.\n"
3379
         "+ basic\n"
3380
         "  Use basic type enumerator for actively-generated sygus enumerators.\n"
3381
         "+ var-agnostic\n"
3382
         "  Use sygus solver to enumerate terms that are agnostic to variables.\n"
3383
         "+ none\n"
3384
         "  Do not use actively-generated sygus enumerators.\n"
3385
         "+ enum\n"
3386
         "  Use optimized enumerator for actively-generated sygus enumerators.\n");
3387
    exit(1);
3388
  }
3389
  else
3390
  {
3391
    throw OptionException(std::string("unknown option for --sygus-active-gen: `") +
3392
                          optarg + "'.  Try --sygus-active-gen=help.");
3393
  }
3394
}
3395
3396
std::ostream&
3397
operator<<(std::ostream& os, SygusFilterSolMode mode)
3398
{
3399
  os << "SygusFilterSolMode::";
3400
  switch(mode) {
3401
    case SygusFilterSolMode::WEAK:
3402
      os << "WEAK";
3403
      break;
3404
    case SygusFilterSolMode::STRONG:
3405
      os << "STRONG";
3406
      break;
3407
    case SygusFilterSolMode::NONE:
3408
      os << "NONE";
3409
      break;
3410
    default:
3411
        Unreachable();
3412
  }
3413
  return os;
3414
}
3415
3416
SygusFilterSolMode
3417
stringToSygusFilterSolMode(const std::string& option, const std::string& optarg)
3418
{
3419
  if (optarg == "weak")
3420
  {
3421
    return SygusFilterSolMode::WEAK;
3422
  }
3423
  else if (optarg == "strong")
3424
  {
3425
    return SygusFilterSolMode::STRONG;
3426
  }
3427
  else if (optarg == "none")
3428
  {
3429
    return SygusFilterSolMode::NONE;
3430
  }
3431
  else if (optarg == "help")
3432
  {
3433
    puts("Modes for filtering sygus solutions.\n"
3434
         "Available modes for --sygus-filter-sol are:\n"
3435
         "+ weak\n"
3436
         "  Filter solutions that are logically weaker than others.\n"
3437
         "+ strong\n"
3438
         "  Filter solutions that are logically stronger than others.\n"
3439
         "+ none (default)\n"
3440
         "  Do not filter sygus solutions.\n");
3441
    exit(1);
3442
  }
3443
  else
3444
  {
3445
    throw OptionException(std::string("unknown option for --sygus-filter-sol: `") +
3446
                          optarg + "'.  Try --sygus-filter-sol=help.");
3447
  }
3448
}
3449
3450
std::ostream&
3451
operator<<(std::ostream& os, SygusGrammarConsMode mode)
3452
{
3453
  os << "SygusGrammarConsMode::";
3454
  switch(mode) {
3455
    case SygusGrammarConsMode::ANY_CONST:
3456
      os << "ANY_CONST";
3457
      break;
3458
    case SygusGrammarConsMode::SIMPLE:
3459
      os << "SIMPLE";
3460
      break;
3461
    case SygusGrammarConsMode::ANY_TERM_CONCISE:
3462
      os << "ANY_TERM_CONCISE";
3463
      break;
3464
    case SygusGrammarConsMode::ANY_TERM:
3465
      os << "ANY_TERM";
3466
      break;
3467
    default:
3468
        Unreachable();
3469
  }
3470
  return os;
3471
}
3472
3473
SygusGrammarConsMode
3474
12
stringToSygusGrammarConsMode(const std::string& option, const std::string& optarg)
3475
{
3476
12
  if (optarg == "any-const")
3477
  {
3478
4
    return SygusGrammarConsMode::ANY_CONST;
3479
  }
3480
8
  else if (optarg == "simple")
3481
  {
3482
    return SygusGrammarConsMode::SIMPLE;
3483
  }
3484
8
  else if (optarg == "any-term-concise")
3485
  {
3486
4
    return SygusGrammarConsMode::ANY_TERM_CONCISE;
3487
  }
3488
4
  else if (optarg == "any-term")
3489
  {
3490
4
    return SygusGrammarConsMode::ANY_TERM;
3491
  }
3492
  else if (optarg == "help")
3493
  {
3494
    puts("Modes for default SyGuS grammars.\n"
3495
         "Available modes for --sygus-grammar-cons are:\n"
3496
         "+ any-const\n"
3497
         "  Use symoblic constant constructors.\n"
3498
         "+ simple (default)\n"
3499
         "  Use simple grammar construction (no symbolic terms or constants).\n"
3500
         "+ any-term-concise\n"
3501
         "  When applicable, use constructors corresponding to any symbolic term, favoring\n"
3502
         "  conciseness over generality. This option is equivalent to any-term but enables\n"
3503
         "  a polynomial grammar for arithmetic when not in a combined theory.\n"
3504
         "+ any-term\n"
3505
         "  When applicable, use constructors corresponding to any symbolic term. This\n"
3506
         "  option enables a sum-of-monomials grammar for arithmetic. For all other types,\n"
3507
         "  it enables symbolic constant constructors.\n");
3508
    exit(1);
3509
  }
3510
  else
3511
  {
3512
    throw OptionException(std::string("unknown option for --sygus-grammar-cons: `") +
3513
                          optarg + "'.  Try --sygus-grammar-cons=help.");
3514
  }
3515
}
3516
3517
std::ostream&
3518
operator<<(std::ostream& os, SygusInstMode mode)
3519
{
3520
  os << "SygusInstMode::";
3521
  switch(mode) {
3522
    case SygusInstMode::PRIORITY_INST:
3523
      os << "PRIORITY_INST";
3524
      break;
3525
    case SygusInstMode::INTERLEAVE:
3526
      os << "INTERLEAVE";
3527
      break;
3528
    case SygusInstMode::PRIORITY_EVAL:
3529
      os << "PRIORITY_EVAL";
3530
      break;
3531
    default:
3532
        Unreachable();
3533
  }
3534
  return os;
3535
}
3536
3537
SygusInstMode
3538
stringToSygusInstMode(const std::string& option, const std::string& optarg)
3539
{
3540
  if (optarg == "priority-inst")
3541
  {
3542
    return SygusInstMode::PRIORITY_INST;
3543
  }
3544
  else if (optarg == "interleave")
3545
  {
3546
    return SygusInstMode::INTERLEAVE;
3547
  }
3548
  else if (optarg == "priority-eval")
3549
  {
3550
    return SygusInstMode::PRIORITY_EVAL;
3551
  }
3552
  else if (optarg == "help")
3553
  {
3554
    puts("SyGuS instantiation lemma modes.\n"
3555
         "Available modes for --sygus-inst-mode are:\n"
3556
         "+ priority-inst (default)\n"
3557
         "  add instantiation lemmas first, add evaluation unfolding if instantiation\n"
3558
         "  fails.\n"
3559
         "+ interleave\n"
3560
         "  add instantiation and evaluation unfolding lemmas in the same step.\n"
3561
         "+ priority-eval\n"
3562
         "  add evaluation unfolding lemma first, add instantiation lemma if unfolding\n"
3563
         "  lemmas already added.\n");
3564
    exit(1);
3565
  }
3566
  else
3567
  {
3568
    throw OptionException(std::string("unknown option for --sygus-inst-mode: `") +
3569
                          optarg + "'.  Try --sygus-inst-mode=help.");
3570
  }
3571
}
3572
3573
std::ostream&
3574
operator<<(std::ostream& os, SygusInstScope mode)
3575
{
3576
  os << "SygusInstScope::";
3577
  switch(mode) {
3578
    case SygusInstScope::BOTH:
3579
      os << "BOTH";
3580
      break;
3581
    case SygusInstScope::OUT:
3582
      os << "OUT";
3583
      break;
3584
    case SygusInstScope::IN:
3585
      os << "IN";
3586
      break;
3587
    default:
3588
        Unreachable();
3589
  }
3590
  return os;
3591
}
3592
3593
SygusInstScope
3594
stringToSygusInstScope(const std::string& option, const std::string& optarg)
3595
{
3596
  if (optarg == "both")
3597
  {
3598
    return SygusInstScope::BOTH;
3599
  }
3600
  else if (optarg == "out")
3601
  {
3602
    return SygusInstScope::OUT;
3603
  }
3604
  else if (optarg == "in")
3605
  {
3606
    return SygusInstScope::IN;
3607
  }
3608
  else if (optarg == "help")
3609
  {
3610
    puts("scope for collecting ground terms for the grammar.\n"
3611
         "Available modes for --sygus-inst-scope are:\n"
3612
         "+ both\n"
3613
         "  combines inside and outside.\n"
3614
         "+ out\n"
3615
         "  use ground terms outside of quantified formulas only.\n"
3616
         "+ in (default)\n"
3617
         "  use ground terms inside given quantified formula only.\n");
3618
    exit(1);
3619
  }
3620
  else
3621
  {
3622
    throw OptionException(std::string("unknown option for --sygus-inst-scope: `") +
3623
                          optarg + "'.  Try --sygus-inst-scope=help.");
3624
  }
3625
}
3626
3627
std::ostream&
3628
operator<<(std::ostream& os, SygusInstTermSelMode mode)
3629
{
3630
  os << "SygusInstTermSelMode::";
3631
  switch(mode) {
3632
    case SygusInstTermSelMode::BOTH:
3633
      os << "BOTH";
3634
      break;
3635
    case SygusInstTermSelMode::MIN:
3636
      os << "MIN";
3637
      break;
3638
    case SygusInstTermSelMode::MAX:
3639
      os << "MAX";
3640
      break;
3641
    default:
3642
        Unreachable();
3643
  }
3644
  return os;
3645
}
3646
3647
SygusInstTermSelMode
3648
stringToSygusInstTermSelMode(const std::string& option, const std::string& optarg)
3649
{
3650
  if (optarg == "both")
3651
  {
3652
    return SygusInstTermSelMode::BOTH;
3653
  }
3654
  else if (optarg == "min")
3655
  {
3656
    return SygusInstTermSelMode::MIN;
3657
  }
3658
  else if (optarg == "max")
3659
  {
3660
    return SygusInstTermSelMode::MAX;
3661
  }
3662
  else if (optarg == "help")
3663
  {
3664
    puts("Ground term selection modes.\n"
3665
         "Available modes for --sygus-inst-term-sel are:\n"
3666
         "+ both\n"
3667
         "  combines minimal and maximal .\n"
3668
         "+ min (default)\n"
3669
         "  collect minimal ground terms only.\n"
3670
         "+ max\n"
3671
         "  collect maximal ground terms only.\n");
3672
    exit(1);
3673
  }
3674
  else
3675
  {
3676
    throw OptionException(std::string("unknown option for --sygus-inst-term-sel: `") +
3677
                          optarg + "'.  Try --sygus-inst-term-sel=help.");
3678
  }
3679
}
3680
3681
std::ostream&
3682
operator<<(std::ostream& os, SygusInvTemplMode mode)
3683
{
3684
  os << "SygusInvTemplMode::";
3685
  switch(mode) {
3686
    case SygusInvTemplMode::POST:
3687
      os << "POST";
3688
      break;
3689
    case SygusInvTemplMode::PRE:
3690
      os << "PRE";
3691
      break;
3692
    case SygusInvTemplMode::NONE:
3693
      os << "NONE";
3694
      break;
3695
    default:
3696
        Unreachable();
3697
  }
3698
  return os;
3699
}
3700
3701
SygusInvTemplMode
3702
6
stringToSygusInvTemplMode(const std::string& option, const std::string& optarg)
3703
{
3704
6
  if (optarg == "post")
3705
  {
3706
4
    return SygusInvTemplMode::POST;
3707
  }
3708
2
  else if (optarg == "pre")
3709
  {
3710
2
    return SygusInvTemplMode::PRE;
3711
  }
3712
  else if (optarg == "none")
3713
  {
3714
    return SygusInvTemplMode::NONE;
3715
  }
3716
  else if (optarg == "help")
3717
  {
3718
    puts("Template modes for sygus invariant synthesis.\n"
3719
         "Available modes for --sygus-inv-templ are:\n"
3720
         "+ post (default)\n"
3721
         "  Synthesize invariant based on strengthening of postcondition.\n"
3722
         "+ pre\n"
3723
         "  Synthesize invariant based on weakening of precondition.\n"
3724
         "+ none\n"
3725
         "  Synthesize invariant directly.\n");
3726
    exit(1);
3727
  }
3728
  else
3729
  {
3730
    throw OptionException(std::string("unknown option for --sygus-inv-templ: `") +
3731
                          optarg + "'.  Try --sygus-inv-templ=help.");
3732
  }
3733
}
3734
3735
std::ostream&
3736
operator<<(std::ostream& os, SygusQueryDumpFilesMode mode)
3737
{
3738
  os << "SygusQueryDumpFilesMode::";
3739
  switch(mode) {
3740
    case SygusQueryDumpFilesMode::ALL:
3741
      os << "ALL";
3742
      break;
3743
    case SygusQueryDumpFilesMode::UNSOLVED:
3744
      os << "UNSOLVED";
3745
      break;
3746
    case SygusQueryDumpFilesMode::NONE:
3747
      os << "NONE";
3748
      break;
3749
    default:
3750
        Unreachable();
3751
  }
3752
  return os;
3753
}
3754
3755
SygusQueryDumpFilesMode
3756
stringToSygusQueryDumpFilesMode(const std::string& option, const std::string& optarg)
3757
{
3758
  if (optarg == "all")
3759
  {
3760
    return SygusQueryDumpFilesMode::ALL;
3761
  }
3762
  else if (optarg == "unsolved")
3763
  {
3764
    return SygusQueryDumpFilesMode::UNSOLVED;
3765
  }
3766
  else if (optarg == "none")
3767
  {
3768
    return SygusQueryDumpFilesMode::NONE;
3769
  }
3770
  else if (optarg == "help")
3771
  {
3772
    puts("Query file options.\n"
3773
         "Available modes for --sygus-query-gen-dump-files are:\n"
3774
         "+ all\n"
3775
         "  Dump all query files.\n"
3776
         "+ unsolved\n"
3777
         "  Dump query files that the subsolver did not solve.\n"
3778
         "+ none (default)\n"
3779
         "  Do not dump query files when using --sygus-query-gen.\n");
3780
    exit(1);
3781
  }
3782
  else
3783
  {
3784
    throw OptionException(std::string("unknown option for --sygus-query-gen-dump-files: `") +
3785
                          optarg + "'.  Try --sygus-query-gen-dump-files=help.");
3786
  }
3787
}
3788
3789
std::ostream&
3790
operator<<(std::ostream& os, CegqiSingleInvRconsMode mode)
3791
{
3792
  os << "CegqiSingleInvRconsMode::";
3793
  switch(mode) {
3794
    case CegqiSingleInvRconsMode::ALL_LIMIT:
3795
      os << "ALL_LIMIT";
3796
      break;
3797
    case CegqiSingleInvRconsMode::ALL:
3798
      os << "ALL";
3799
      break;
3800
    case CegqiSingleInvRconsMode::TRY:
3801
      os << "TRY";
3802
      break;
3803
    case CegqiSingleInvRconsMode::NONE:
3804
      os << "NONE";
3805
      break;
3806
    default:
3807
        Unreachable();
3808
  }
3809
  return os;
3810
}
3811
3812
CegqiSingleInvRconsMode
3813
2
stringToCegqiSingleInvRconsMode(const std::string& option, const std::string& optarg)
3814
{
3815
2
  if (optarg == "all-limit")
3816
  {
3817
    return CegqiSingleInvRconsMode::ALL_LIMIT;
3818
  }
3819
2
  else if (optarg == "all")
3820
  {
3821
    return CegqiSingleInvRconsMode::ALL;
3822
  }
3823
2
  else if (optarg == "try")
3824
  {
3825
2
    return CegqiSingleInvRconsMode::TRY;
3826
  }
3827
  else if (optarg == "none")
3828
  {
3829
    return CegqiSingleInvRconsMode::NONE;
3830
  }
3831
  else if (optarg == "help")
3832
  {
3833
    puts("Modes for reconstruction solutions while using single invocation techniques.\n"
3834
         "Available modes for --sygus-si-rcons are:\n"
3835
         "+ all-limit (default)\n"
3836
         "  Try to reconstruct solutions in the original grammar, but termintate if a\n"
3837
         "  maximum number of rounds for reconstruction is exceeded.\n"
3838
         "+ all\n"
3839
         "  Try to reconstruct solutions in the original grammar. In this mode, we do not\n"
3840
         "  terminate until a solution is successfully reconstructed.\n"
3841
         "+ try\n"
3842
         "  Try to reconstruct solutions in the original grammar when using single\n"
3843
         "  invocation techniques in an incomplete (fail-fast) manner.\n"
3844
         "+ none\n"
3845
         "  Do not try to reconstruct solutions in the original (user-provided) grammar\n"
3846
         "  when using single invocation techniques. In this mode, solutions produced by\n"
3847
         "  CVC4 may violate grammar restrictions.\n");
3848
    exit(1);
3849
  }
3850
  else
3851
  {
3852
    throw OptionException(std::string("unknown option for --sygus-si-rcons: `") +
3853
                          optarg + "'.  Try --sygus-si-rcons=help.");
3854
  }
3855
}
3856
3857
std::ostream&
3858
operator<<(std::ostream& os, CegqiSingleInvMode mode)
3859
{
3860
  os << "CegqiSingleInvMode::";
3861
  switch(mode) {
3862
    case CegqiSingleInvMode::ALL:
3863
      os << "ALL";
3864
      break;
3865
    case CegqiSingleInvMode::NONE:
3866
      os << "NONE";
3867
      break;
3868
    case CegqiSingleInvMode::USE:
3869
      os << "USE";
3870
      break;
3871
    default:
3872
        Unreachable();
3873
  }
3874
  return os;
3875
}
3876
3877
CegqiSingleInvMode
3878
87
stringToCegqiSingleInvMode(const std::string& option, const std::string& optarg)
3879
{
3880
87
  if (optarg == "all")
3881
  {
3882
44
    return CegqiSingleInvMode::ALL;
3883
  }
3884
43
  else if (optarg == "none")
3885
  {
3886
43
    return CegqiSingleInvMode::NONE;
3887
  }
3888
  else if (optarg == "use")
3889
  {
3890
    return CegqiSingleInvMode::USE;
3891
  }
3892
  else if (optarg == "help")
3893
  {
3894
    puts("Modes for single invocation techniques.\n"
3895
         "Available modes for --sygus-si are:\n"
3896
         "+ all\n"
3897
         "  Always use single invocation techniques.\n"
3898
         "+ none (default)\n"
3899
         "  Do not use single invocation techniques.\n"
3900
         "+ use\n"
3901
         "  Use single invocation techniques only if grammar is not restrictive.\n");
3902
    exit(1);
3903
  }
3904
  else
3905
  {
3906
    throw OptionException(std::string("unknown option for --sygus-si: `") +
3907
                          optarg + "'.  Try --sygus-si=help.");
3908
  }
3909
}
3910
3911
std::ostream&
3912
operator<<(std::ostream& os, SygusUnifPiMode mode)
3913
{
3914
  os << "SygusUnifPiMode::";
3915
  switch(mode) {
3916
    case SygusUnifPiMode::CENUM_IGAIN:
3917
      os << "CENUM_IGAIN";
3918
      break;
3919
    case SygusUnifPiMode::CENUM:
3920
      os << "CENUM";
3921
      break;
3922
    case SygusUnifPiMode::NONE:
3923
      os << "NONE";
3924
      break;
3925
    case SygusUnifPiMode::COMPLETE:
3926
      os << "COMPLETE";
3927
      break;
3928
    default:
3929
        Unreachable();
3930
  }
3931
  return os;
3932
}
3933
3934
SygusUnifPiMode
3935
16
stringToSygusUnifPiMode(const std::string& option, const std::string& optarg)
3936
{
3937
16
  if (optarg == "cond-enum-igain")
3938
  {
3939
    return SygusUnifPiMode::CENUM_IGAIN;
3940
  }
3941
16
  else if (optarg == "cond-enum")
3942
  {
3943
    return SygusUnifPiMode::CENUM;
3944
  }
3945
16
  else if (optarg == "none")
3946
  {
3947
    return SygusUnifPiMode::NONE;
3948
  }
3949
16
  else if (optarg == "complete")
3950
  {
3951
16
    return SygusUnifPiMode::COMPLETE;
3952
  }
3953
  else if (optarg == "help")
3954
  {
3955
    puts("Modes for piecewise-independent unification.\n"
3956
         "Available modes for --sygus-unif-pi are:\n"
3957
         "+ cond-enum-igain\n"
3958
         "  Same as cond-enum, but additionally uses an information gain heuristic when\n"
3959
         "  doing decision tree learning.\n"
3960
         "+ cond-enum\n"
3961
         "  Use unconstrained condition enumeration for piecewise-independent unification\n"
3962
         "  (see Section 4 of Barbosa et al FMCAD 2019).\n"
3963
         "+ none (default)\n"
3964
         "  Do not use piecewise-independent unification.\n"
3965
         "+ complete\n"
3966
         "  Use complete approach for piecewise-independent unification (see Section 3 of\n"
3967
         "  Barbosa et al FMCAD 2019)\n");
3968
    exit(1);
3969
  }
3970
  else
3971
  {
3972
    throw OptionException(std::string("unknown option for --sygus-unif-pi: `") +
3973
                          optarg + "'.  Try --sygus-unif-pi=help.");
3974
  }
3975
}
3976
3977
std::ostream&
3978
operator<<(std::ostream& os, TermDbMode mode)
3979
{
3980
  os << "TermDbMode::";
3981
  switch(mode) {
3982
    case TermDbMode::ALL:
3983
      os << "ALL";
3984
      break;
3985
    case TermDbMode::RELEVANT:
3986
      os << "RELEVANT";
3987
      break;
3988
    default:
3989
        Unreachable();
3990
  }
3991
  return os;
3992
}
3993
3994
TermDbMode
3995
stringToTermDbMode(const std::string& option, const std::string& optarg)
3996
{
3997
  if (optarg == "all")
3998
  {
3999
    return TermDbMode::ALL;
4000
  }
4001
  else if (optarg == "relevant")
4002
  {
4003
    return TermDbMode::RELEVANT;
4004
  }
4005
  else if (optarg == "help")
4006
  {
4007
    puts("Modes for terms included in the quantifiers term database.\n"
4008
         "Available modes for --term-db-mode are:\n"
4009
         "+ all (default)\n"
4010
         "  Quantifiers module considers all ground terms.\n"
4011
         "+ relevant\n"
4012
         "  Quantifiers module considers only ground terms connected to current\n"
4013
         "  assertions.\n");
4014
    exit(1);
4015
  }
4016
  else
4017
  {
4018
    throw OptionException(std::string("unknown option for --term-db-mode: `") +
4019
                          optarg + "'.  Try --term-db-mode=help.");
4020
  }
4021
}
4022
4023
std::ostream&
4024
operator<<(std::ostream& os, TriggerActiveSelMode mode)
4025
{
4026
  os << "TriggerActiveSelMode::";
4027
  switch(mode) {
4028
    case TriggerActiveSelMode::ALL:
4029
      os << "ALL";
4030
      break;
4031
    case TriggerActiveSelMode::MIN:
4032
      os << "MIN";
4033
      break;
4034
    case TriggerActiveSelMode::MAX:
4035
      os << "MAX";
4036
      break;
4037
    default:
4038
        Unreachable();
4039
  }
4040
  return os;
4041
}
4042
4043
TriggerActiveSelMode
4044
stringToTriggerActiveSelMode(const std::string& option, const std::string& optarg)
4045
{
4046
  if (optarg == "all")
4047
  {
4048
    return TriggerActiveSelMode::ALL;
4049
  }
4050
  else if (optarg == "min")
4051
  {
4052
    return TriggerActiveSelMode::MIN;
4053
  }
4054
  else if (optarg == "max")
4055
  {
4056
    return TriggerActiveSelMode::MAX;
4057
  }
4058
  else if (optarg == "help")
4059
  {
4060
    puts("Trigger active selection modes.\n"
4061
         "Available modes for --trigger-active-sel are:\n"
4062
         "+ all (default)\n"
4063
         "  Make all triggers active.\n"
4064
         "+ min\n"
4065
         "  Activate triggers with minimal ground terms.\n"
4066
         "+ max\n"
4067
         "  Activate triggers with maximal ground terms.\n");
4068
    exit(1);
4069
  }
4070
  else
4071
  {
4072
    throw OptionException(std::string("unknown option for --trigger-active-sel: `") +
4073
                          optarg + "'.  Try --trigger-active-sel=help.");
4074
  }
4075
}
4076
4077
std::ostream&
4078
operator<<(std::ostream& os, TriggerSelMode mode)
4079
{
4080
  os << "TriggerSelMode::";
4081
  switch(mode) {
4082
    case TriggerSelMode::MIN_SINGLE_ALL:
4083
      os << "MIN_SINGLE_ALL";
4084
      break;
4085
    case TriggerSelMode::MIN:
4086
      os << "MIN";
4087
      break;
4088
    case TriggerSelMode::MIN_SINGLE_MAX:
4089
      os << "MIN_SINGLE_MAX";
4090
      break;
4091
    case TriggerSelMode::MAX:
4092
      os << "MAX";
4093
      break;
4094
    case TriggerSelMode::ALL:
4095
      os << "ALL";
4096
      break;
4097
    default:
4098
        Unreachable();
4099
  }
4100
  return os;
4101
}
4102
4103
TriggerSelMode
4104
stringToTriggerSelMode(const std::string& option, const std::string& optarg)
4105
{
4106
  if (optarg == "min-s-all")
4107
  {
4108
    return TriggerSelMode::MIN_SINGLE_ALL;
4109
  }
4110
  else if (optarg == "min")
4111
  {
4112
    return TriggerSelMode::MIN;
4113
  }
4114
  else if (optarg == "min-s-max")
4115
  {
4116
    return TriggerSelMode::MIN_SINGLE_MAX;
4117
  }
4118
  else if (optarg == "max")
4119
  {
4120
    return TriggerSelMode::MAX;
4121
  }
4122
  else if (optarg == "all")
4123
  {
4124
    return TriggerSelMode::ALL;
4125
  }
4126
  else if (optarg == "help")
4127
  {
4128
    puts("Trigger selection modes.\n"
4129
         "Available modes for --trigger-sel are:\n"
4130
         "+ min-s-all\n"
4131
         "  Consider only minimal subterms that meet criteria for single triggers, all\n"
4132
         "  otherwise.\n"
4133
         "+ min (default)\n"
4134
         "  Consider only minimal subterms that meet criteria for triggers.\n"
4135
         "+ min-s-max\n"
4136
         "  Consider only minimal subterms that meet criteria for single triggers, maximal\n"
4137
         "  otherwise.\n"
4138
         "+ max\n"
4139
         "  Consider only maximal subterms that meet criteria for triggers.\n"
4140
         "+ all\n"
4141
         "  Consider all subterms that meet criteria for triggers.\n");
4142
    exit(1);
4143
  }
4144
  else
4145
  {
4146
    throw OptionException(std::string("unknown option for --trigger-sel: `") +
4147
                          optarg + "'.  Try --trigger-sel=help.");
4148
  }
4149
}
4150
4151
std::ostream&
4152
operator<<(std::ostream& os, UserPatMode mode)
4153
{
4154
  os << "UserPatMode::";
4155
  switch(mode) {
4156
    case UserPatMode::TRUST:
4157
      os << "TRUST";
4158
      break;
4159
    case UserPatMode::RESORT:
4160
      os << "RESORT";
4161
      break;
4162
    case UserPatMode::INTERLEAVE:
4163
      os << "INTERLEAVE";
4164
      break;
4165
    case UserPatMode::IGNORE:
4166
      os << "IGNORE";
4167
      break;
4168
    case UserPatMode::USE:
4169
      os << "USE";
4170
      break;
4171
    default:
4172
        Unreachable();
4173
  }
4174
  return os;
4175
}
4176
4177
UserPatMode
4178
stringToUserPatMode(const std::string& option, const std::string& optarg)
4179
{
4180
  if (optarg == "trust")
4181
  {
4182
    return UserPatMode::TRUST;
4183
  }
4184
  else if (optarg == "resort")
4185
  {
4186
    return UserPatMode::RESORT;
4187
  }
4188
  else if (optarg == "interleave")
4189
  {
4190
    return UserPatMode::INTERLEAVE;
4191
  }
4192
  else if (optarg == "ignore")
4193
  {
4194
    return UserPatMode::IGNORE;
4195
  }
4196
  else if (optarg == "use")
4197
  {
4198
    return UserPatMode::USE;
4199
  }
4200
  else if (optarg == "help")
4201
  {
4202
    puts("These modes determine how user provided patterns (triggers) are used during\n"
4203
         "E-matching. The modes vary on when instantiation based on user-provided\n"
4204
         "triggers is combined with instantiation based on automatically selected\n"
4205
         "triggers.\n"
4206
         "Available modes for --user-pat are:\n"
4207
         "+ trust (default)\n"
4208
         "  When provided, use only user-provided patterns for a quantified formula.\n"
4209
         "+ resort\n"
4210
         "  Use user-provided patterns only after auto-generated patterns saturate.\n"
4211
         "+ interleave\n"
4212
         "  Alternate between use/resort.\n"
4213
         "+ ignore\n"
4214
         "  Ignore user-provided patterns.\n"
4215
         "+ use\n"
4216
         "  Use both user-provided and auto-generated patterns when patterns are provided\n"
4217
         "  for a quantified formula.\n");
4218
    exit(1);
4219
  }
4220
  else
4221
  {
4222
    throw OptionException(std::string("unknown option for --user-pat: `") +
4223
                          optarg + "'.  Try --user-pat=help.");
4224
  }
4225
}
4226
4227
4228
}  // namespace options
4229
26685
}  // namespace CVC4