GCC Code Coverage Report
Directory: . Exec Total Coverage
File: build-coverage/src/options/arith_options.cpp Lines: 124 442 28.1 %
Date: 2021-03-22 Branches: 6 109 5.5 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file module_template.cpp
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Mathias Preiner
6
 ** This file is part of the CVC4 project.
7
 ** Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
8
 ** in the top-level source directory and their institutional affiliations.
9
 ** All rights reserved.  See the file COPYING in the top-level source
10
 ** directory for licensing information.\endverbatim
11
 **
12
 ** \brief Option template for option modules.
13
 **
14
 ** For each <module>_options.toml configuration file, mkoptions.py
15
 ** expands this template and generates a <module>_options.cpp file.
16
 **/
17
18
#include "options/options_holder.h"
19
#include "base/check.h"
20
21
namespace CVC4 {
22
23
template <> void Options::set(
24
    options::maxApproxDepth__option_t,
25
    const options::maxApproxDepth__option_t::type& x)
26
{
27
  d_holder->maxApproxDepth = x;
28
}
29
template <> const options::maxApproxDepth__option_t::type& Options::operator[](
30
    options::maxApproxDepth__option_t) const
31
{
32
  return d_holder->maxApproxDepth;
33
}
34
template <> bool Options::wasSetByUser(options::maxApproxDepth__option_t) const
35
{
36
  return d_holder->maxApproxDepth__setByUser__;
37
}
38
882
template <> const options::brabTest__option_t::type& Options::operator[](
39
    options::brabTest__option_t) const
40
{
41
882
  return d_holder->brabTest;
42
}
43
template <> bool Options::wasSetByUser(options::brabTest__option_t) const
44
{
45
  return d_holder->brabTest__setByUser__;
46
}
47
582
template <> const options::arithNoPartialFun__option_t::type& Options::operator[](
48
    options::arithNoPartialFun__option_t) const
49
{
50
582
  return d_holder->arithNoPartialFun;
51
}
52
template <> bool Options::wasSetByUser(options::arithNoPartialFun__option_t) const
53
{
54
  return d_holder->arithNoPartialFun__setByUser__;
55
}
56
template <> void Options::set(
57
    options::arithPropAsLemmaLength__option_t,
58
    const options::arithPropAsLemmaLength__option_t::type& x)
59
{
60
  d_holder->arithPropAsLemmaLength = x;
61
}
62
121578
template <> const options::arithPropAsLemmaLength__option_t::type& Options::operator[](
63
    options::arithPropAsLemmaLength__option_t) const
64
{
65
121578
  return d_holder->arithPropAsLemmaLength;
66
}
67
template <> bool Options::wasSetByUser(options::arithPropAsLemmaLength__option_t) const
68
{
69
  return d_holder->arithPropAsLemmaLength__setByUser__;
70
}
71
9568168
template <> const options::arithPropagationMode__option_t::type& Options::operator[](
72
    options::arithPropagationMode__option_t) const
73
{
74
9568168
  return d_holder->arithPropagationMode;
75
}
76
template <> bool Options::wasSetByUser(options::arithPropagationMode__option_t) const
77
{
78
  return d_holder->arithPropagationMode__setByUser__;
79
}
80
8990
template <> void Options::set(
81
    options::arithRewriteEq__option_t,
82
    const options::arithRewriteEq__option_t::type& x)
83
{
84
8990
  d_holder->arithRewriteEq = x;
85
8990
}
86
28681
template <> const options::arithRewriteEq__option_t::type& Options::operator[](
87
    options::arithRewriteEq__option_t) const
88
{
89
28681
  return d_holder->arithRewriteEq;
90
}
91
8995
template <> bool Options::wasSetByUser(options::arithRewriteEq__option_t) const
92
{
93
8995
  return d_holder->arithRewriteEq__setByUser__;
94
}
95
template <> void Options::set(
96
    options::collectPivots__option_t,
97
    const options::collectPivots__option_t::type& x)
98
{
99
  d_holder->collectPivots = x;
100
}
101
1769324
template <> const options::collectPivots__option_t::type& Options::operator[](
102
    options::collectPivots__option_t) const
103
{
104
1769324
  return d_holder->collectPivots;
105
}
106
template <> bool Options::wasSetByUser(options::collectPivots__option_t) const
107
{
108
  return d_holder->collectPivots__setByUser__;
109
}
110
template <> void Options::set(
111
    options::doCutAllBounded__option_t,
112
    const options::doCutAllBounded__option_t::type& x)
113
{
114
  d_holder->doCutAllBounded = x;
115
}
116
template <> const options::doCutAllBounded__option_t::type& Options::operator[](
117
    options::doCutAllBounded__option_t) const
118
{
119
  return d_holder->doCutAllBounded;
120
}
121
template <> bool Options::wasSetByUser(options::doCutAllBounded__option_t) const
122
{
123
  return d_holder->doCutAllBounded__setByUser__;
124
}
125
template <> void Options::set(
126
    options::exportDioDecompositions__option_t,
127
    const options::exportDioDecompositions__option_t::type& x)
128
{
129
  d_holder->exportDioDecompositions = x;
130
}
131
190
template <> const options::exportDioDecompositions__option_t::type& Options::operator[](
132
    options::exportDioDecompositions__option_t) const
133
{
134
190
  return d_holder->exportDioDecompositions;
135
}
136
template <> bool Options::wasSetByUser(options::exportDioDecompositions__option_t) const
137
{
138
  return d_holder->exportDioDecompositions__setByUser__;
139
}
140
template <> const options::dioRepeat__option_t::type& Options::operator[](
141
    options::dioRepeat__option_t) const
142
{
143
  return d_holder->dioRepeat;
144
}
145
template <> bool Options::wasSetByUser(options::dioRepeat__option_t) const
146
{
147
  return d_holder->dioRepeat__setByUser__;
148
}
149
4296
template <> const options::arithDioSolver__option_t::type& Options::operator[](
150
    options::arithDioSolver__option_t) const
151
{
152
4296
  return d_holder->arithDioSolver;
153
}
154
template <> bool Options::wasSetByUser(options::arithDioSolver__option_t) const
155
{
156
  return d_holder->arithDioSolver__setByUser__;
157
}
158
357
template <> const options::dioSolverTurns__option_t::type& Options::operator[](
159
    options::dioSolverTurns__option_t) const
160
{
161
357
  return d_holder->dioSolverTurns;
162
}
163
template <> bool Options::wasSetByUser(options::dioSolverTurns__option_t) const
164
{
165
  return d_holder->dioSolverTurns__setByUser__;
166
}
167
35980
template <> const options::arithErrorSelectionRule__option_t::type& Options::operator[](
168
    options::arithErrorSelectionRule__option_t) const
169
{
170
35980
  return d_holder->arithErrorSelectionRule;
171
}
172
template <> bool Options::wasSetByUser(options::arithErrorSelectionRule__option_t) const
173
{
174
  return d_holder->arithErrorSelectionRule__setByUser__;
175
}
176
template <> void Options::set(
177
    options::havePenalties__option_t,
178
    const options::havePenalties__option_t::type& x)
179
{
180
  d_holder->havePenalties = x;
181
}
182
template <> const options::havePenalties__option_t::type& Options::operator[](
183
    options::havePenalties__option_t) const
184
{
185
  return d_holder->havePenalties;
186
}
187
template <> bool Options::wasSetByUser(options::havePenalties__option_t) const
188
{
189
  return d_holder->havePenalties__setByUser__;
190
}
191
8995
template <> void Options::set(
192
    options::arithHeuristicPivots__option_t,
193
    const options::arithHeuristicPivots__option_t::type& x)
194
{
195
8995
  d_holder->arithHeuristicPivots = x;
196
8995
}
197
160472
template <> const options::arithHeuristicPivots__option_t::type& Options::operator[](
198
    options::arithHeuristicPivots__option_t) const
199
{
200
160472
  return d_holder->arithHeuristicPivots;
201
}
202
8995
template <> bool Options::wasSetByUser(options::arithHeuristicPivots__option_t) const
203
{
204
8995
  return d_holder->arithHeuristicPivots__setByUser__;
205
}
206
template <> const options::replayFailureLemma__option_t::type& Options::operator[](
207
    options::replayFailureLemma__option_t) const
208
{
209
  return d_holder->replayFailureLemma;
210
}
211
template <> bool Options::wasSetByUser(options::replayFailureLemma__option_t) const
212
{
213
  return d_holder->replayFailureLemma__setByUser__;
214
}
215
2215
template <> const options::maxCutsInContext__option_t::type& Options::operator[](
216
    options::maxCutsInContext__option_t) const
217
{
218
2215
  return d_holder->maxCutsInContext;
219
}
220
template <> bool Options::wasSetByUser(options::maxCutsInContext__option_t) const
221
{
222
  return d_holder->maxCutsInContext__setByUser__;
223
}
224
1529
template <> void Options::set(
225
    options::arithMLTrick__option_t,
226
    const options::arithMLTrick__option_t::type& x)
227
{
228
1529
  d_holder->arithMLTrick = x;
229
1529
}
230
17703
template <> const options::arithMLTrick__option_t::type& Options::operator[](
231
    options::arithMLTrick__option_t) const
232
{
233
17703
  return d_holder->arithMLTrick;
234
}
235
template <> bool Options::wasSetByUser(options::arithMLTrick__option_t) const
236
{
237
  return d_holder->arithMLTrick__setByUser__;
238
}
239
template <> const options::arithMLTrickSubstitutions__option_t::type& Options::operator[](
240
    options::arithMLTrickSubstitutions__option_t) const
241
{
242
  return d_holder->arithMLTrickSubstitutions;
243
}
244
template <> bool Options::wasSetByUser(options::arithMLTrickSubstitutions__option_t) const
245
{
246
  return d_holder->arithMLTrickSubstitutions__setByUser__;
247
}
248
template <> void Options::set(
249
    options::newProp__option_t,
250
    const options::newProp__option_t::type& x)
251
{
252
  d_holder->newProp = x;
253
}
254
1091428
template <> const options::newProp__option_t::type& Options::operator[](
255
    options::newProp__option_t) const
256
{
257
1091428
  return d_holder->newProp;
258
}
259
template <> bool Options::wasSetByUser(options::newProp__option_t) const
260
{
261
  return d_holder->newProp__setByUser__;
262
}
263
template <> void Options::set(
264
    options::nlCad__option_t,
265
    const options::nlCad__option_t::type& x)
266
{
267
  d_holder->nlCad = x;
268
}
269
10027
template <> const options::nlCad__option_t::type& Options::operator[](
270
    options::nlCad__option_t) const
271
{
272
10027
  return d_holder->nlCad;
273
}
274
template <> bool Options::wasSetByUser(options::nlCad__option_t) const
275
{
276
  return d_holder->nlCad__setByUser__;
277
}
278
template <> void Options::set(
279
    options::nlCadUseInitial__option_t,
280
    const options::nlCadUseInitial__option_t::type& x)
281
{
282
  d_holder->nlCadUseInitial = x;
283
}
284
template <> const options::nlCadUseInitial__option_t::type& Options::operator[](
285
    options::nlCadUseInitial__option_t) const
286
{
287
  return d_holder->nlCadUseInitial;
288
}
289
template <> bool Options::wasSetByUser(options::nlCadUseInitial__option_t) const
290
{
291
  return d_holder->nlCadUseInitial__setByUser__;
292
}
293
template <> void Options::set(
294
    options::nlExt__option_t,
295
    const options::nlExt__option_t::type& x)
296
{
297
  d_holder->nlExt = x;
298
}
299
1067
template <> const options::nlExt__option_t::type& Options::operator[](
300
    options::nlExt__option_t) const
301
{
302
1067
  return d_holder->nlExt;
303
}
304
template <> bool Options::wasSetByUser(options::nlExt__option_t) const
305
{
306
  return d_holder->nlExt__setByUser__;
307
}
308
8581
template <> const options::nlExtEntailConflicts__option_t::type& Options::operator[](
309
    options::nlExtEntailConflicts__option_t) const
310
{
311
8581
  return d_holder->nlExtEntailConflicts;
312
}
313
template <> bool Options::wasSetByUser(options::nlExtEntailConflicts__option_t) const
314
{
315
  return d_holder->nlExtEntailConflicts__setByUser__;
316
}
317
405
template <> const options::nlExtFactor__option_t::type& Options::operator[](
318
    options::nlExtFactor__option_t) const
319
{
320
405
  return d_holder->nlExtFactor;
321
}
322
template <> bool Options::wasSetByUser(options::nlExtFactor__option_t) const
323
{
324
  return d_holder->nlExtFactor__setByUser__;
325
}
326
35
template <> const options::nlExtIncPrecision__option_t::type& Options::operator[](
327
    options::nlExtIncPrecision__option_t) const
328
{
329
35
  return d_holder->nlExtIncPrecision;
330
}
331
template <> bool Options::wasSetByUser(options::nlExtIncPrecision__option_t) const
332
{
333
  return d_holder->nlExtIncPrecision__setByUser__;
334
}
335
11323
template <> const options::nlExtPurify__option_t::type& Options::operator[](
336
    options::nlExtPurify__option_t) const
337
{
338
11323
  return d_holder->nlExtPurify;
339
}
340
template <> bool Options::wasSetByUser(options::nlExtPurify__option_t) const
341
{
342
  return d_holder->nlExtPurify__setByUser__;
343
}
344
405
template <> const options::nlExtResBound__option_t::type& Options::operator[](
345
    options::nlExtResBound__option_t) const
346
{
347
405
  return d_holder->nlExtResBound;
348
}
349
template <> bool Options::wasSetByUser(options::nlExtResBound__option_t) const
350
{
351
  return d_holder->nlExtResBound__setByUser__;
352
}
353
25957
template <> const options::nlExtRewrites__option_t::type& Options::operator[](
354
    options::nlExtRewrites__option_t) const
355
{
356
25957
  return d_holder->nlExtRewrites;
357
}
358
template <> bool Options::wasSetByUser(options::nlExtRewrites__option_t) const
359
{
360
  return d_holder->nlExtRewrites__setByUser__;
361
}
362
405
template <> const options::nlExtSplitZero__option_t::type& Options::operator[](
363
    options::nlExtSplitZero__option_t) const
364
{
365
405
  return d_holder->nlExtSplitZero;
366
}
367
template <> bool Options::wasSetByUser(options::nlExtSplitZero__option_t) const
368
{
369
  return d_holder->nlExtSplitZero__setByUser__;
370
}
371
template <> void Options::set(
372
    options::nlExtTfTaylorDegree__option_t,
373
    const options::nlExtTfTaylorDegree__option_t::type& x)
374
{
375
  d_holder->nlExtTfTaylorDegree = x;
376
}
377
4389
template <> const options::nlExtTfTaylorDegree__option_t::type& Options::operator[](
378
    options::nlExtTfTaylorDegree__option_t) const
379
{
380
4389
  return d_holder->nlExtTfTaylorDegree;
381
}
382
template <> bool Options::wasSetByUser(options::nlExtTfTaylorDegree__option_t) const
383
{
384
  return d_holder->nlExtTfTaylorDegree__setByUser__;
385
}
386
405
template <> const options::nlExtTfTangentPlanes__option_t::type& Options::operator[](
387
    options::nlExtTfTangentPlanes__option_t) const
388
{
389
405
  return d_holder->nlExtTfTangentPlanes;
390
}
391
template <> bool Options::wasSetByUser(options::nlExtTfTangentPlanes__option_t) const
392
{
393
  return d_holder->nlExtTfTangentPlanes__setByUser__;
394
}
395
1294
template <> void Options::set(
396
    options::nlExtTangentPlanes__option_t,
397
    const options::nlExtTangentPlanes__option_t::type& x)
398
{
399
1294
  d_holder->nlExtTangentPlanes = x;
400
1294
}
401
64387
template <> const options::nlExtTangentPlanes__option_t::type& Options::operator[](
402
    options::nlExtTangentPlanes__option_t) const
403
{
404
64387
  return d_holder->nlExtTangentPlanes;
405
}
406
1319
template <> bool Options::wasSetByUser(options::nlExtTangentPlanes__option_t) const
407
{
408
1319
  return d_holder->nlExtTangentPlanes__setByUser__;
409
}
410
269
template <> void Options::set(
411
    options::nlExtTangentPlanesInterleave__option_t,
412
    const options::nlExtTangentPlanesInterleave__option_t::type& x)
413
{
414
269
  d_holder->nlExtTangentPlanesInterleave = x;
415
269
}
416
168
template <> const options::nlExtTangentPlanesInterleave__option_t::type& Options::operator[](
417
    options::nlExtTangentPlanesInterleave__option_t) const
418
{
419
168
  return d_holder->nlExtTangentPlanesInterleave;
420
}
421
269
template <> bool Options::wasSetByUser(options::nlExtTangentPlanesInterleave__option_t) const
422
{
423
269
  return d_holder->nlExtTangentPlanesInterleave__setByUser__;
424
}
425
template <> void Options::set(
426
    options::nlICP__option_t,
427
    const options::nlICP__option_t::type& x)
428
{
429
  d_holder->nlICP = x;
430
}
431
405
template <> const options::nlICP__option_t::type& Options::operator[](
432
    options::nlICP__option_t) const
433
{
434
405
  return d_holder->nlICP;
435
}
436
template <> bool Options::wasSetByUser(options::nlICP__option_t) const
437
{
438
  return d_holder->nlICP__setByUser__;
439
}
440
template <> void Options::set(
441
    options::nlRlvMode__option_t,
442
    const options::nlRlvMode__option_t::type& x)
443
{
444
  d_holder->nlRlvMode = x;
445
}
446
10241
template <> const options::nlRlvMode__option_t::type& Options::operator[](
447
    options::nlRlvMode__option_t) const
448
{
449
10241
  return d_holder->nlRlvMode;
450
}
451
template <> bool Options::wasSetByUser(options::nlRlvMode__option_t) const
452
{
453
  return d_holder->nlRlvMode__setByUser__;
454
}
455
template <> void Options::set(
456
    options::pbRewrites__option_t,
457
    const options::pbRewrites__option_t::type& x)
458
{
459
  d_holder->pbRewrites = x;
460
}
461
13140
template <> const options::pbRewrites__option_t::type& Options::operator[](
462
    options::pbRewrites__option_t) const
463
{
464
13140
  return d_holder->pbRewrites;
465
}
466
template <> bool Options::wasSetByUser(options::pbRewrites__option_t) const
467
{
468
  return d_holder->pbRewrites__setByUser__;
469
}
470
8995
template <> void Options::set(
471
    options::arithPivotThreshold__option_t,
472
    const options::arithPivotThreshold__option_t::type& x)
473
{
474
8995
  d_holder->arithPivotThreshold = x;
475
8995
}
476
389774
template <> const options::arithPivotThreshold__option_t::type& Options::operator[](
477
    options::arithPivotThreshold__option_t) const
478
{
479
389774
  return d_holder->arithPivotThreshold;
480
}
481
8995
template <> bool Options::wasSetByUser(options::arithPivotThreshold__option_t) const
482
{
483
8995
  return d_holder->arithPivotThreshold__setByUser__;
484
}
485
1502
template <> const options::ppAssertMaxSubSize__option_t::type& Options::operator[](
486
    options::ppAssertMaxSubSize__option_t) const
487
{
488
1502
  return d_holder->ppAssertMaxSubSize;
489
}
490
template <> bool Options::wasSetByUser(options::ppAssertMaxSubSize__option_t) const
491
{
492
  return d_holder->ppAssertMaxSubSize__setByUser__;
493
}
494
10342546
template <> const options::arithPropagateMaxLength__option_t::type& Options::operator[](
495
    options::arithPropagateMaxLength__option_t) const
496
{
497
10342546
  return d_holder->arithPropagateMaxLength;
498
}
499
template <> bool Options::wasSetByUser(options::arithPropagateMaxLength__option_t) const
500
{
501
  return d_holder->arithPropagateMaxLength__setByUser__;
502
}
503
template <> const options::replayEarlyCloseDepths__option_t::type& Options::operator[](
504
    options::replayEarlyCloseDepths__option_t) const
505
{
506
  return d_holder->replayEarlyCloseDepths;
507
}
508
template <> bool Options::wasSetByUser(options::replayEarlyCloseDepths__option_t) const
509
{
510
  return d_holder->replayEarlyCloseDepths__setByUser__;
511
}
512
template <> const options::replayFailurePenalty__option_t::type& Options::operator[](
513
    options::replayFailurePenalty__option_t) const
514
{
515
  return d_holder->replayFailurePenalty;
516
}
517
template <> bool Options::wasSetByUser(options::replayFailurePenalty__option_t) const
518
{
519
  return d_holder->replayFailurePenalty__setByUser__;
520
}
521
template <> const options::lemmaRejectCutSize__option_t::type& Options::operator[](
522
    options::lemmaRejectCutSize__option_t) const
523
{
524
  return d_holder->lemmaRejectCutSize;
525
}
526
template <> bool Options::wasSetByUser(options::lemmaRejectCutSize__option_t) const
527
{
528
  return d_holder->lemmaRejectCutSize__setByUser__;
529
}
530
template <> const options::replayNumericFailurePenalty__option_t::type& Options::operator[](
531
    options::replayNumericFailurePenalty__option_t) const
532
{
533
  return d_holder->replayNumericFailurePenalty;
534
}
535
template <> bool Options::wasSetByUser(options::replayNumericFailurePenalty__option_t) const
536
{
537
  return d_holder->replayNumericFailurePenalty__setByUser__;
538
}
539
template <> const options::replayRejectCutSize__option_t::type& Options::operator[](
540
    options::replayRejectCutSize__option_t) const
541
{
542
  return d_holder->replayRejectCutSize;
543
}
544
template <> bool Options::wasSetByUser(options::replayRejectCutSize__option_t) const
545
{
546
  return d_holder->replayRejectCutSize__setByUser__;
547
}
548
template <> const options::soiApproxMajorFailurePen__option_t::type& Options::operator[](
549
    options::soiApproxMajorFailurePen__option_t) const
550
{
551
  return d_holder->soiApproxMajorFailurePen;
552
}
553
template <> bool Options::wasSetByUser(options::soiApproxMajorFailurePen__option_t) const
554
{
555
  return d_holder->soiApproxMajorFailurePen__setByUser__;
556
}
557
template <> const options::soiApproxMajorFailure__option_t::type& Options::operator[](
558
    options::soiApproxMajorFailure__option_t) const
559
{
560
  return d_holder->soiApproxMajorFailure;
561
}
562
template <> bool Options::wasSetByUser(options::soiApproxMajorFailure__option_t) const
563
{
564
  return d_holder->soiApproxMajorFailure__setByUser__;
565
}
566
template <> const options::soiApproxMinorFailurePen__option_t::type& Options::operator[](
567
    options::soiApproxMinorFailurePen__option_t) const
568
{
569
  return d_holder->soiApproxMinorFailurePen;
570
}
571
template <> bool Options::wasSetByUser(options::soiApproxMinorFailurePen__option_t) const
572
{
573
  return d_holder->soiApproxMinorFailurePen__setByUser__;
574
}
575
template <> const options::soiApproxMinorFailure__option_t::type& Options::operator[](
576
    options::soiApproxMinorFailure__option_t) const
577
{
578
  return d_holder->soiApproxMinorFailure;
579
}
580
template <> bool Options::wasSetByUser(options::soiApproxMinorFailure__option_t) const
581
{
582
  return d_holder->soiApproxMinorFailure__setByUser__;
583
}
584
template <> void Options::set(
585
    options::restrictedPivots__option_t,
586
    const options::restrictedPivots__option_t::type& x)
587
{
588
  d_holder->restrictedPivots = x;
589
}
590
1758046
template <> const options::restrictedPivots__option_t::type& Options::operator[](
591
    options::restrictedPivots__option_t) const
592
{
593
1758046
  return d_holder->restrictedPivots;
594
}
595
template <> bool Options::wasSetByUser(options::restrictedPivots__option_t) const
596
{
597
  return d_holder->restrictedPivots__setByUser__;
598
}
599
18531
template <> const options::revertArithModels__option_t::type& Options::operator[](
600
    options::revertArithModels__option_t) const
601
{
602
18531
  return d_holder->revertArithModels;
603
}
604
template <> bool Options::wasSetByUser(options::revertArithModels__option_t) const
605
{
606
  return d_holder->revertArithModels__setByUser__;
607
}
608
106
template <> const options::rrTurns__option_t::type& Options::operator[](
609
    options::rrTurns__option_t) const
610
{
611
106
  return d_holder->rrTurns;
612
}
613
template <> bool Options::wasSetByUser(options::rrTurns__option_t) const
614
{
615
  return d_holder->rrTurns__setByUser__;
616
}
617
template <> const options::trySolveIntStandardEffort__option_t::type& Options::operator[](
618
    options::trySolveIntStandardEffort__option_t) const
619
{
620
  return d_holder->trySolveIntStandardEffort;
621
}
622
template <> bool Options::wasSetByUser(options::trySolveIntStandardEffort__option_t) const
623
{
624
  return d_holder->trySolveIntStandardEffort__setByUser__;
625
}
626
87301
template <> const options::arithSimplexCheckPeriod__option_t::type& Options::operator[](
627
    options::arithSimplexCheckPeriod__option_t) const
628
{
629
87301
  return d_holder->arithSimplexCheckPeriod;
630
}
631
template <> bool Options::wasSetByUser(options::arithSimplexCheckPeriod__option_t) const
632
{
633
  return d_holder->arithSimplexCheckPeriod__setByUser__;
634
}
635
template <> void Options::set(
636
    options::soiQuickExplain__option_t,
637
    const options::soiQuickExplain__option_t::type& x)
638
{
639
  d_holder->soiQuickExplain = x;
640
}
641
template <> const options::soiQuickExplain__option_t::type& Options::operator[](
642
    options::soiQuickExplain__option_t) const
643
{
644
  return d_holder->soiQuickExplain;
645
}
646
template <> bool Options::wasSetByUser(options::soiQuickExplain__option_t) const
647
{
648
  return d_holder->soiQuickExplain__setByUser__;
649
}
650
8995
template <> void Options::set(
651
    options::arithStandardCheckVarOrderPivots__option_t,
652
    const options::arithStandardCheckVarOrderPivots__option_t::type& x)
653
{
654
8995
  d_holder->arithStandardCheckVarOrderPivots = x;
655
8995
}
656
111205
template <> const options::arithStandardCheckVarOrderPivots__option_t::type& Options::operator[](
657
    options::arithStandardCheckVarOrderPivots__option_t) const
658
{
659
111205
  return d_holder->arithStandardCheckVarOrderPivots;
660
}
661
8995
template <> bool Options::wasSetByUser(options::arithStandardCheckVarOrderPivots__option_t) const
662
{
663
8995
  return d_holder->arithStandardCheckVarOrderPivots__setByUser__;
664
}
665
7407
template <> const options::arithUnateLemmaMode__option_t::type& Options::operator[](
666
    options::arithUnateLemmaMode__option_t) const
667
{
668
7407
  return d_holder->arithUnateLemmaMode;
669
}
670
template <> bool Options::wasSetByUser(options::arithUnateLemmaMode__option_t) const
671
{
672
  return d_holder->arithUnateLemmaMode__setByUser__;
673
}
674
template <> void Options::set(
675
    options::useApprox__option_t,
676
    const options::useApprox__option_t::type& x)
677
{
678
  d_holder->useApprox = x;
679
}
680
5317756
template <> const options::useApprox__option_t::type& Options::operator[](
681
    options::useApprox__option_t) const
682
{
683
5317756
  return d_holder->useApprox;
684
}
685
template <> bool Options::wasSetByUser(options::useApprox__option_t) const
686
{
687
  return d_holder->useApprox__setByUser__;
688
}
689
template <> void Options::set(
690
    options::useFC__option_t,
691
    const options::useFC__option_t::type& x)
692
{
693
  d_holder->useFC = x;
694
}
695
1830593
template <> const options::useFC__option_t::type& Options::operator[](
696
    options::useFC__option_t) const
697
{
698
1830593
  return d_holder->useFC;
699
}
700
template <> bool Options::wasSetByUser(options::useFC__option_t) const
701
{
702
  return d_holder->useFC__setByUser__;
703
}
704
template <> void Options::set(
705
    options::useSOI__option_t,
706
    const options::useSOI__option_t::type& x)
707
{
708
  d_holder->useSOI = x;
709
}
710
6043
template <> const options::useSOI__option_t::type& Options::operator[](
711
    options::useSOI__option_t) const
712
{
713
6043
  return d_holder->useSOI;
714
}
715
template <> bool Options::wasSetByUser(options::useSOI__option_t) const
716
{
717
  return d_holder->useSOI__setByUser__;
718
}
719
720
721
namespace options {
722
723
thread_local struct maxApproxDepth__option_t maxApproxDepth;
724
thread_local struct brabTest__option_t brabTest;
725
thread_local struct arithNoPartialFun__option_t arithNoPartialFun;
726
thread_local struct arithPropAsLemmaLength__option_t arithPropAsLemmaLength;
727
thread_local struct arithPropagationMode__option_t arithPropagationMode;
728
thread_local struct arithRewriteEq__option_t arithRewriteEq;
729
thread_local struct collectPivots__option_t collectPivots;
730
thread_local struct doCutAllBounded__option_t doCutAllBounded;
731
thread_local struct exportDioDecompositions__option_t exportDioDecompositions;
732
thread_local struct dioRepeat__option_t dioRepeat;
733
thread_local struct arithDioSolver__option_t arithDioSolver;
734
thread_local struct dioSolverTurns__option_t dioSolverTurns;
735
thread_local struct arithErrorSelectionRule__option_t arithErrorSelectionRule;
736
thread_local struct havePenalties__option_t havePenalties;
737
thread_local struct arithHeuristicPivots__option_t arithHeuristicPivots;
738
thread_local struct replayFailureLemma__option_t replayFailureLemma;
739
thread_local struct maxCutsInContext__option_t maxCutsInContext;
740
thread_local struct arithMLTrick__option_t arithMLTrick;
741
thread_local struct arithMLTrickSubstitutions__option_t arithMLTrickSubstitutions;
742
thread_local struct newProp__option_t newProp;
743
thread_local struct nlCad__option_t nlCad;
744
thread_local struct nlCadUseInitial__option_t nlCadUseInitial;
745
thread_local struct nlExt__option_t nlExt;
746
thread_local struct nlExtEntailConflicts__option_t nlExtEntailConflicts;
747
thread_local struct nlExtFactor__option_t nlExtFactor;
748
thread_local struct nlExtIncPrecision__option_t nlExtIncPrecision;
749
thread_local struct nlExtPurify__option_t nlExtPurify;
750
thread_local struct nlExtResBound__option_t nlExtResBound;
751
thread_local struct nlExtRewrites__option_t nlExtRewrites;
752
thread_local struct nlExtSplitZero__option_t nlExtSplitZero;
753
thread_local struct nlExtTfTaylorDegree__option_t nlExtTfTaylorDegree;
754
thread_local struct nlExtTfTangentPlanes__option_t nlExtTfTangentPlanes;
755
thread_local struct nlExtTangentPlanes__option_t nlExtTangentPlanes;
756
thread_local struct nlExtTangentPlanesInterleave__option_t nlExtTangentPlanesInterleave;
757
thread_local struct nlICP__option_t nlICP;
758
thread_local struct nlRlvMode__option_t nlRlvMode;
759
thread_local struct pbRewrites__option_t pbRewrites;
760
thread_local struct arithPivotThreshold__option_t arithPivotThreshold;
761
thread_local struct ppAssertMaxSubSize__option_t ppAssertMaxSubSize;
762
thread_local struct arithPropagateMaxLength__option_t arithPropagateMaxLength;
763
thread_local struct replayEarlyCloseDepths__option_t replayEarlyCloseDepths;
764
thread_local struct replayFailurePenalty__option_t replayFailurePenalty;
765
thread_local struct lemmaRejectCutSize__option_t lemmaRejectCutSize;
766
thread_local struct replayNumericFailurePenalty__option_t replayNumericFailurePenalty;
767
thread_local struct replayRejectCutSize__option_t replayRejectCutSize;
768
thread_local struct soiApproxMajorFailurePen__option_t soiApproxMajorFailurePen;
769
thread_local struct soiApproxMajorFailure__option_t soiApproxMajorFailure;
770
thread_local struct soiApproxMinorFailurePen__option_t soiApproxMinorFailurePen;
771
thread_local struct soiApproxMinorFailure__option_t soiApproxMinorFailure;
772
thread_local struct restrictedPivots__option_t restrictedPivots;
773
thread_local struct revertArithModels__option_t revertArithModels;
774
thread_local struct rrTurns__option_t rrTurns;
775
thread_local struct trySolveIntStandardEffort__option_t trySolveIntStandardEffort;
776
thread_local struct arithSimplexCheckPeriod__option_t arithSimplexCheckPeriod;
777
thread_local struct soiQuickExplain__option_t soiQuickExplain;
778
thread_local struct arithStandardCheckVarOrderPivots__option_t arithStandardCheckVarOrderPivots;
779
thread_local struct arithUnateLemmaMode__option_t arithUnateLemmaMode;
780
thread_local struct useApprox__option_t useApprox;
781
thread_local struct useFC__option_t useFC;
782
thread_local struct useSOI__option_t useSOI;
783
784
785
std::ostream&
786
operator<<(std::ostream& os, ArithPropagationMode mode)
787
{
788
  os << "ArithPropagationMode::";
789
  switch(mode) {
790
    case ArithPropagationMode::NO_PROP:
791
      os << "NO_PROP";
792
      break;
793
    case ArithPropagationMode::BOUND_INFERENCE_PROP:
794
      os << "BOUND_INFERENCE_PROP";
795
      break;
796
    case ArithPropagationMode::UNATE_PROP:
797
      os << "UNATE_PROP";
798
      break;
799
    case ArithPropagationMode::BOTH_PROP:
800
      os << "BOTH_PROP";
801
      break;
802
    default:
803
        Unreachable();
804
  }
805
  return os;
806
}
807
808
ArithPropagationMode
809
stringToArithPropagationMode(const std::string& option, const std::string& optarg)
810
{
811
  if (optarg == "none")
812
  {
813
    return ArithPropagationMode::NO_PROP;
814
  }
815
  else if (optarg == "bi")
816
  {
817
    return ArithPropagationMode::BOUND_INFERENCE_PROP;
818
  }
819
  else if (optarg == "unate")
820
  {
821
    return ArithPropagationMode::UNATE_PROP;
822
  }
823
  else if (optarg == "both")
824
  {
825
    return ArithPropagationMode::BOTH_PROP;
826
  }
827
  else if (optarg == "help")
828
  {
829
    puts("This decides on kind of propagation arithmetic attempts to do during the\n"
830
         "search.\n"
831
         "Available modes for --arith-prop are:\n"
832
         "+ none\n"
833
         "+ bi\n"
834
         "  (Bounds Inference) infers bounds on basic variables using the upper and lower\n"
835
         "  bounds of the non-basic variables in the tableau.\n"
836
         "+ unate\n"
837
         "  Use constraints to do unate propagation.\n"
838
         "+ both (default)\n"
839
         "  Use bounds inference and unate.\n");
840
    exit(1);
841
  }
842
  else
843
  {
844
    throw OptionException(std::string("unknown option for --arith-prop: `") +
845
                          optarg + "'.  Try --arith-prop=help.");
846
  }
847
}
848
849
std::ostream&
850
operator<<(std::ostream& os, ErrorSelectionRule mode)
851
{
852
  os << "ErrorSelectionRule::";
853
  switch(mode) {
854
    case ErrorSelectionRule::MAXIMUM_AMOUNT:
855
      os << "MAXIMUM_AMOUNT";
856
      break;
857
    case ErrorSelectionRule::MINIMUM_AMOUNT:
858
      os << "MINIMUM_AMOUNT";
859
      break;
860
    case ErrorSelectionRule::SUM_METRIC:
861
      os << "SUM_METRIC";
862
      break;
863
    case ErrorSelectionRule::VAR_ORDER:
864
      os << "VAR_ORDER";
865
      break;
866
    default:
867
        Unreachable();
868
  }
869
  return os;
870
}
871
872
ErrorSelectionRule
873
stringToErrorSelectionRule(const std::string& option, const std::string& optarg)
874
{
875
  if (optarg == "max")
876
  {
877
    return ErrorSelectionRule::MAXIMUM_AMOUNT;
878
  }
879
  else if (optarg == "min")
880
  {
881
    return ErrorSelectionRule::MINIMUM_AMOUNT;
882
  }
883
  else if (optarg == "sum")
884
  {
885
    return ErrorSelectionRule::SUM_METRIC;
886
  }
887
  else if (optarg == "varord")
888
  {
889
    return ErrorSelectionRule::VAR_ORDER;
890
  }
891
  else if (optarg == "help")
892
  {
893
    puts("This decides on the rule used by simplex during heuristic rounds for deciding\n"
894
         "the next basic variable to select.\n"
895
         "Available modes for --error-selection-rule are:\n"
896
         "+ max\n"
897
         "  The maximum violation the bound.\n"
898
         "+ min (default)\n"
899
         "  The minimum abs() value of the variable's violation of its bound.\n"
900
         "+ sum\n"
901
         "+ varord\n"
902
         "  The variable order.\n");
903
    exit(1);
904
  }
905
  else
906
  {
907
    throw OptionException(std::string("unknown option for --error-selection-rule: `") +
908
                          optarg + "'.  Try --error-selection-rule=help.");
909
  }
910
}
911
912
std::ostream&
913
operator<<(std::ostream& os, NlRlvMode mode)
914
{
915
  os << "NlRlvMode::";
916
  switch(mode) {
917
    case NlRlvMode::NONE:
918
      os << "NONE";
919
      break;
920
    case NlRlvMode::INTERLEAVE:
921
      os << "INTERLEAVE";
922
      break;
923
    case NlRlvMode::ALWAYS:
924
      os << "ALWAYS";
925
      break;
926
    default:
927
        Unreachable();
928
  }
929
  return os;
930
}
931
932
NlRlvMode
933
8
stringToNlRlvMode(const std::string& option, const std::string& optarg)
934
{
935
8
  if (optarg == "none")
936
  {
937
1
    return NlRlvMode::NONE;
938
  }
939
7
  else if (optarg == "interleave")
940
  {
941
    return NlRlvMode::INTERLEAVE;
942
  }
943
7
  else if (optarg == "always")
944
  {
945
7
    return NlRlvMode::ALWAYS;
946
  }
947
  else if (optarg == "help")
948
  {
949
    puts("Modes for using relevance of assertoins in non-linear arithmetic.\n"
950
         "Available modes for --nl-rlv are:\n"
951
         "+ none (default)\n"
952
         "  Do not use relevance.\n"
953
         "+ interleave\n"
954
         "  Alternate rounds using relevance.\n"
955
         "+ always\n"
956
         "  Always use relevance.\n");
957
    exit(1);
958
  }
959
  else
960
  {
961
    throw OptionException(std::string("unknown option for --nl-rlv: `") +
962
                          optarg + "'.  Try --nl-rlv=help.");
963
  }
964
}
965
966
std::ostream&
967
operator<<(std::ostream& os, ArithUnateLemmaMode mode)
968
{
969
  os << "ArithUnateLemmaMode::";
970
  switch(mode) {
971
    case ArithUnateLemmaMode::INEQUALITY:
972
      os << "INEQUALITY";
973
      break;
974
    case ArithUnateLemmaMode::NO:
975
      os << "NO";
976
      break;
977
    case ArithUnateLemmaMode::EQUALITY:
978
      os << "EQUALITY";
979
      break;
980
    case ArithUnateLemmaMode::ALL:
981
      os << "ALL";
982
      break;
983
    default:
984
        Unreachable();
985
  }
986
  return os;
987
}
988
989
ArithUnateLemmaMode
990
stringToArithUnateLemmaMode(const std::string& option, const std::string& optarg)
991
{
992
  if (optarg == "ineqs")
993
  {
994
    return ArithUnateLemmaMode::INEQUALITY;
995
  }
996
  else if (optarg == "none")
997
  {
998
    return ArithUnateLemmaMode::NO;
999
  }
1000
  else if (optarg == "eqs")
1001
  {
1002
    return ArithUnateLemmaMode::EQUALITY;
1003
  }
1004
  else if (optarg == "all")
1005
  {
1006
    return ArithUnateLemmaMode::ALL;
1007
  }
1008
  else if (optarg == "help")
1009
  {
1010
    puts("Unate lemmas are generated before SAT search begins using the relationship of\n"
1011
         "constant terms and polynomials.\n"
1012
         "Available modes for --unate-lemmas are:\n"
1013
         "+ ineqs\n"
1014
         "  Outputs lemmas of the general form (<= p c) implies (<= p d) for c < d.\n"
1015
         "+ none\n"
1016
         "+ eqs\n"
1017
         "  Outputs lemmas of the general forms (= p c) implies (<= p d) for c < d, or (=\n"
1018
         "  p c) implies (not (= p d)) for c != d.\n"
1019
         "+ all (default)\n"
1020
         "  A combination of inequalities and equalities.\n");
1021
    exit(1);
1022
  }
1023
  else
1024
  {
1025
    throw OptionException(std::string("unknown option for --unate-lemmas: `") +
1026
                          optarg + "'.  Try --unate-lemmas=help.");
1027
  }
1028
}
1029
1030
1031
}  // namespace options
1032
26676
}  // namespace CVC4