GCC Code Coverage Report
Directory: . Exec Total Coverage
File: build-coverage/src/options/smt_options.h Lines: 166 232 71.6 %
Date: 2021-03-22 Branches: 0 0 0.0 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file module_template.h
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Mathias Preiner
6
 ** This file is part of the CVC4 project.
7
 ** Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
8
 ** in the top-level source directory and their institutional affiliations.
9
 ** All rights reserved.  See the file COPYING in the top-level source
10
 ** directory for licensing information.\endverbatim
11
 **
12
 ** \brief Contains code for handling command-line options.
13
 **
14
 ** For each <module>_options.toml configuration file, mkoptions.py
15
 ** expands this template and generates a <module>_options.h file.
16
 **/
17
18
#include "cvc4_private.h"
19
20
#ifndef CVC4__OPTIONS__SMT_H
21
#define CVC4__OPTIONS__SMT_H
22
23
#include "options/options.h"
24
25
26
27
28
#define CVC4_OPTIONS__SMT__FOR_OPTION_HOLDER \
29
  abstractValues__option_t::type abstractValues;\
30
  bool abstractValues__setByUser__; \
31
  ackermann__option_t::type ackermann;\
32
  bool ackermann__setByUser__; \
33
  arithNlLemmaStep__option_t::type arithNlLemmaStep;\
34
  bool arithNlLemmaStep__setByUser__; \
35
  arithPivotStep__option_t::type arithPivotStep;\
36
  bool arithPivotStep__setByUser__; \
37
  bitblastStep__option_t::type bitblastStep;\
38
  bool bitblastStep__setByUser__; \
39
  blockModelsMode__option_t::type blockModelsMode;\
40
  bool blockModelsMode__setByUser__; \
41
  bvEagerAssertStep__option_t::type bvEagerAssertStep;\
42
  bool bvEagerAssertStep__setByUser__; \
43
  bvPropagationStep__option_t::type bvPropagationStep;\
44
  bool bvPropagationStep__setByUser__; \
45
  bvSatConflictStep__option_t::type bvSatConflictStep;\
46
  bool bvSatConflictStep__setByUser__; \
47
  bvSatPropagateStep__option_t::type bvSatPropagateStep;\
48
  bool bvSatPropagateStep__setByUser__; \
49
  bvSatSimplifyStep__option_t::type bvSatSimplifyStep;\
50
  bool bvSatSimplifyStep__setByUser__; \
51
  BVAndIntegerGranularity__option_t::type BVAndIntegerGranularity;\
52
  bool BVAndIntegerGranularity__setByUser__; \
53
  checkAbducts__option_t::type checkAbducts;\
54
  bool checkAbducts__setByUser__; \
55
  checkInterpols__option_t::type checkInterpols;\
56
  bool checkInterpols__setByUser__; \
57
  checkModels__option_t::type checkModels;\
58
  bool checkModels__setByUser__; \
59
  checkProofs__option_t::type checkProofs;\
60
  bool checkProofs__setByUser__; \
61
  checkSynthSol__option_t::type checkSynthSol;\
62
  bool checkSynthSol__setByUser__; \
63
  checkUnsatCores__option_t::type checkUnsatCores;\
64
  bool checkUnsatCores__setByUser__; \
65
  checkUnsatCoresNew__option_t::type checkUnsatCoresNew;\
66
  bool checkUnsatCoresNew__setByUser__; \
67
  cnfStep__option_t::type cnfStep;\
68
  bool cnfStep__setByUser__; \
69
  debugCheckModels__option_t::type debugCheckModels;\
70
  bool debugCheckModels__setByUser__; \
71
  decisionStep__option_t::type decisionStep;\
72
  bool decisionStep__setByUser__; \
73
  diagnosticChannelName__option_t::type diagnosticChannelName;\
74
  bool diagnosticChannelName__setByUser__; \
75
  dumpInstantiations__option_t::type dumpInstantiations;\
76
  bool dumpInstantiations__setByUser__; \
77
  dumpModels__option_t::type dumpModels;\
78
  bool dumpModels__setByUser__; \
79
  dumpProofs__option_t::type dumpProofs;\
80
  bool dumpProofs__setByUser__; \
81
  dumpToFileName__option_t::type dumpToFileName;\
82
  bool dumpToFileName__setByUser__; \
83
  dumpUnsatCores__option_t::type dumpUnsatCores;\
84
  bool dumpUnsatCores__setByUser__; \
85
  dumpUnsatCoresFull__option_t::type dumpUnsatCoresFull;\
86
  bool dumpUnsatCoresFull__setByUser__; \
87
  dumpModeString__option_t::type dumpModeString;\
88
  bool dumpModeString__setByUser__; \
89
  earlyIteRemoval__option_t::type earlyIteRemoval;\
90
  bool earlyIteRemoval__setByUser__; \
91
  expandDefinitions__option_t::type expandDefinitions;\
92
  bool expandDefinitions__setByUser__; \
93
  extRewPrep__option_t::type extRewPrep;\
94
  bool extRewPrep__setByUser__; \
95
  extRewPrepAgg__option_t::type extRewPrepAgg;\
96
  bool extRewPrepAgg__setByUser__; \
97
  forceNoLimitCpuWhileDump__option_t::type forceNoLimitCpuWhileDump;\
98
  bool forceNoLimitCpuWhileDump__setByUser__; \
99
  foreignTheoryRewrite__option_t::type foreignTheoryRewrite;\
100
  bool foreignTheoryRewrite__setByUser__; \
101
  iandMode__option_t::type iandMode;\
102
  bool iandMode__setByUser__; \
103
  incrementalSolving__option_t::type incrementalSolving;\
104
  bool incrementalSolving__setByUser__; \
105
  interactiveMode__option_t::type interactiveMode;\
106
  bool interactiveMode__setByUser__; \
107
  doITESimp__option_t::type doITESimp;\
108
  bool doITESimp__setByUser__; \
109
  lemmaStep__option_t::type lemmaStep;\
110
  bool lemmaStep__setByUser__; \
111
  modelCoresMode__option_t::type modelCoresMode;\
112
  bool modelCoresMode__setByUser__; \
113
  modelUninterpPrint__option_t::type modelUninterpPrint;\
114
  bool modelUninterpPrint__setByUser__; \
115
  modelWitnessValue__option_t::type modelWitnessValue;\
116
  bool modelWitnessValue__setByUser__; \
117
  newSkolemStep__option_t::type newSkolemStep;\
118
  bool newSkolemStep__setByUser__; \
119
  doITESimpOnRepeat__option_t::type doITESimpOnRepeat;\
120
  bool doITESimpOnRepeat__setByUser__; \
121
  parseStep__option_t::type parseStep;\
122
  bool parseStep__setByUser__; \
123
  preprocessStep__option_t::type preprocessStep;\
124
  bool preprocessStep__setByUser__; \
125
  produceAbducts__option_t::type produceAbducts;\
126
  bool produceAbducts__setByUser__; \
127
  produceAssertions__option_t::type produceAssertions;\
128
  bool produceAssertions__setByUser__; \
129
  produceAssignments__option_t::type produceAssignments;\
130
  bool produceAssignments__setByUser__; \
131
  produceInterpols__option_t::type produceInterpols;\
132
  bool produceInterpols__setByUser__; \
133
  produceModels__option_t::type produceModels;\
134
  bool produceModels__setByUser__; \
135
  produceProofs__option_t::type produceProofs;\
136
  bool produceProofs__setByUser__; \
137
  unsatAssumptions__option_t::type unsatAssumptions;\
138
  bool unsatAssumptions__setByUser__; \
139
  unsatCores__option_t::type unsatCores;\
140
  bool unsatCores__setByUser__; \
141
  quantifierStep__option_t::type quantifierStep;\
142
  bool quantifierStep__setByUser__; \
143
  regularChannelName__option_t::type regularChannelName;\
144
  bool regularChannelName__setByUser__; \
145
  repeatSimp__option_t::type repeatSimp;\
146
  bool repeatSimp__setByUser__; \
147
  restartStep__option_t::type restartStep;\
148
  bool restartStep__setByUser__; \
149
  rewriteStep__option_t::type rewriteStep;\
150
  bool rewriteStep__setByUser__; \
151
  perCallResourceLimit__option_t::type perCallResourceLimit;\
152
  bool perCallResourceLimit__setByUser__; \
153
  cumulativeResourceLimit__option_t::type cumulativeResourceLimit;\
154
  bool cumulativeResourceLimit__setByUser__; \
155
  satConflictStep__option_t::type satConflictStep;\
156
  bool satConflictStep__setByUser__; \
157
  compressItes__option_t::type compressItes;\
158
  bool compressItes__setByUser__; \
159
  zombieHuntThreshold__option_t::type zombieHuntThreshold;\
160
  bool zombieHuntThreshold__setByUser__; \
161
  simplifyWithCareEnabled__option_t::type simplifyWithCareEnabled;\
162
  bool simplifyWithCareEnabled__setByUser__; \
163
  simplificationMode__option_t::type simplificationMode;\
164
  bool simplificationMode__setByUser__; \
165
  solveBVAsInt__option_t::type solveBVAsInt;\
166
  bool solveBVAsInt__setByUser__; \
167
  solveIntAsBV__option_t::type solveIntAsBV;\
168
  bool solveIntAsBV__setByUser__; \
169
  solveRealAsInt__option_t::type solveRealAsInt;\
170
  bool solveRealAsInt__setByUser__; \
171
  sortInference__option_t::type sortInference;\
172
  bool sortInference__setByUser__; \
173
  doStaticLearning__option_t::type doStaticLearning;\
174
  bool doStaticLearning__setByUser__; \
175
  sygusOut__option_t::type sygusOut;\
176
  bool sygusOut__setByUser__; \
177
  sygusPrintCallbacks__option_t::type sygusPrintCallbacks;\
178
  bool sygusPrintCallbacks__setByUser__; \
179
  theoryCheckStep__option_t::type theoryCheckStep;\
180
  bool theoryCheckStep__setByUser__; \
181
  perCallMillisecondLimit__option_t::type perCallMillisecondLimit;\
182
  bool perCallMillisecondLimit__setByUser__; \
183
  cumulativeMillisecondLimit__option_t::type cumulativeMillisecondLimit;\
184
  bool cumulativeMillisecondLimit__setByUser__; \
185
  unconstrainedSimp__option_t::type unconstrainedSimp;\
186
  bool unconstrainedSimp__setByUser__;
187
188
189
namespace CVC4 {
190
191
namespace options {
192
193
194
enum class BlockModelsMode
195
{
196
  NONE,
197
  VALUES,
198
  LITERALS
199
};
200
std::ostream&
201
operator<<(std::ostream& os, BlockModelsMode mode);
202
BlockModelsMode
203
stringToBlockModelsMode(const std::string& option, const std::string& optarg);
204
enum class IandMode
205
{
206
  BITWISE,
207
  SUM,
208
  VALUE
209
};
210
std::ostream&
211
operator<<(std::ostream& os, IandMode mode);
212
IandMode
213
stringToIandMode(const std::string& option, const std::string& optarg);
214
enum class ModelCoresMode
215
{
216
  NON_IMPLIED,
217
  NONE,
218
  SIMPLE
219
};
220
std::ostream&
221
operator<<(std::ostream& os, ModelCoresMode mode);
222
ModelCoresMode
223
stringToModelCoresMode(const std::string& option, const std::string& optarg);
224
enum class ModelUninterpPrintMode
225
{
226
  DeclSortAndFun,
227
  None,
228
  DtEnum,
229
  DeclFun
230
};
231
std::ostream&
232
operator<<(std::ostream& os, ModelUninterpPrintMode mode);
233
ModelUninterpPrintMode
234
stringToModelUninterpPrintMode(const std::string& option, const std::string& optarg);
235
enum class ProduceInterpols
236
{
237
  CONJECTURE,
238
  NONE,
239
  SHARED,
240
  DEFAULT,
241
  ALL,
242
  ASSUMPTIONS
243
};
244
std::ostream&
245
operator<<(std::ostream& os, ProduceInterpols mode);
246
ProduceInterpols
247
stringToProduceInterpols(const std::string& option, const std::string& optarg);
248
enum class SimplificationMode
249
{
250
  NONE,
251
  BATCH
252
};
253
std::ostream&
254
operator<<(std::ostream& os, SimplificationMode mode);
255
SimplificationMode
256
stringToSimplificationMode(const std::string& option, const std::string& optarg);
257
enum class SolveBVAsIntMode
258
{
259
  IAND,
260
  OFF,
261
  SUM,
262
  BV
263
};
264
std::ostream&
265
operator<<(std::ostream& os, SolveBVAsIntMode mode);
266
SolveBVAsIntMode
267
stringToSolveBVAsIntMode(const std::string& option, const std::string& optarg);
268
enum class SygusSolutionOutMode
269
{
270
  STATUS_AND_DEF,
271
  STATUS,
272
  STATUS_OR_DEF,
273
  STANDARD
274
};
275
std::ostream&
276
operator<<(std::ostream& os, SygusSolutionOutMode mode);
277
SygusSolutionOutMode
278
stringToSygusSolutionOutMode(const std::string& option, const std::string& optarg);
279
280
extern struct abstractValues__option_t
281
{
282
  typedef bool type;
283
  type operator()() const;
284
  bool wasSetByUser() const;
285
  const char* getName() const;
286
} thread_local abstractValues;
287
extern struct ackermann__option_t
288
{
289
  typedef bool type;
290
  type operator()() const;
291
  bool wasSetByUser() const;
292
  void set(const type& v);
293
  const char* getName() const;
294
} thread_local ackermann;
295
extern struct arithNlLemmaStep__option_t
296
{
297
  typedef unsigned type;
298
  type operator()() const;
299
  bool wasSetByUser() const;
300
  const char* getName() const;
301
} thread_local arithNlLemmaStep;
302
extern struct arithPivotStep__option_t
303
{
304
  typedef unsigned type;
305
  type operator()() const;
306
  bool wasSetByUser() const;
307
  const char* getName() const;
308
} thread_local arithPivotStep;
309
extern struct bitblastStep__option_t
310
{
311
  typedef unsigned type;
312
  type operator()() const;
313
  bool wasSetByUser() const;
314
  const char* getName() const;
315
} thread_local bitblastStep;
316
extern struct blockModelsMode__option_t
317
{
318
  typedef BlockModelsMode type;
319
  type operator()() const;
320
  bool wasSetByUser() const;
321
  void set(const type& v);
322
  const char* getName() const;
323
} thread_local blockModelsMode;
324
extern struct bvEagerAssertStep__option_t
325
{
326
  typedef unsigned type;
327
  type operator()() const;
328
  bool wasSetByUser() const;
329
  const char* getName() const;
330
} thread_local bvEagerAssertStep;
331
extern struct bvPropagationStep__option_t
332
{
333
  typedef unsigned type;
334
  type operator()() const;
335
  bool wasSetByUser() const;
336
  const char* getName() const;
337
} thread_local bvPropagationStep;
338
extern struct bvSatConflictStep__option_t
339
{
340
  typedef unsigned type;
341
  type operator()() const;
342
  bool wasSetByUser() const;
343
  const char* getName() const;
344
} thread_local bvSatConflictStep;
345
extern struct bvSatPropagateStep__option_t
346
{
347
  typedef unsigned type;
348
  type operator()() const;
349
  bool wasSetByUser() const;
350
  const char* getName() const;
351
} thread_local bvSatPropagateStep;
352
extern struct bvSatSimplifyStep__option_t
353
{
354
  typedef unsigned type;
355
  type operator()() const;
356
  bool wasSetByUser() const;
357
  const char* getName() const;
358
} thread_local bvSatSimplifyStep;
359
extern struct BVAndIntegerGranularity__option_t
360
{
361
  typedef uint32_t type;
362
  type operator()() const;
363
  bool wasSetByUser() const;
364
  const char* getName() const;
365
} thread_local BVAndIntegerGranularity;
366
extern struct checkAbducts__option_t
367
{
368
  typedef bool type;
369
  type operator()() const;
370
  bool wasSetByUser() const;
371
  const char* getName() const;
372
} thread_local checkAbducts;
373
extern struct checkInterpols__option_t
374
{
375
  typedef bool type;
376
  type operator()() const;
377
  bool wasSetByUser() const;
378
  const char* getName() const;
379
} thread_local checkInterpols;
380
extern struct checkModels__option_t
381
{
382
  typedef bool type;
383
  type operator()() const;
384
  bool wasSetByUser() const;
385
  void set(const type& v);
386
  const char* getName() const;
387
} thread_local checkModels;
388
extern struct checkProofs__option_t
389
{
390
  typedef bool type;
391
  type operator()() const;
392
  bool wasSetByUser() const;
393
  void set(const type& v);
394
  const char* getName() const;
395
} thread_local checkProofs;
396
extern struct checkSynthSol__option_t
397
{
398
  typedef bool type;
399
  type operator()() const;
400
  bool wasSetByUser() const;
401
  void set(const type& v);
402
  const char* getName() const;
403
} thread_local checkSynthSol;
404
extern struct checkUnsatCores__option_t
405
{
406
  typedef bool type;
407
  type operator()() const;
408
  bool wasSetByUser() const;
409
  void set(const type& v);
410
  const char* getName() const;
411
} thread_local checkUnsatCores;
412
extern struct checkUnsatCoresNew__option_t
413
{
414
  typedef bool type;
415
  type operator()() const;
416
  bool wasSetByUser() const;
417
  void set(const type& v);
418
  const char* getName() const;
419
} thread_local checkUnsatCoresNew;
420
extern struct cnfStep__option_t
421
{
422
  typedef unsigned type;
423
  type operator()() const;
424
  bool wasSetByUser() const;
425
  const char* getName() const;
426
} thread_local cnfStep;
427
extern struct debugCheckModels__option_t
428
{
429
  typedef bool type;
430
  type operator()() const;
431
  bool wasSetByUser() const;
432
  void set(const type& v);
433
  const char* getName() const;
434
} thread_local debugCheckModels;
435
extern struct decisionStep__option_t
436
{
437
  typedef unsigned type;
438
  type operator()() const;
439
  bool wasSetByUser() const;
440
  const char* getName() const;
441
} thread_local decisionStep;
442
extern struct diagnosticChannelName__option_t
443
{
444
  typedef std::string type;
445
  type operator()() const;
446
  bool wasSetByUser() const;
447
  const char* getName() const;
448
} thread_local diagnosticChannelName;
449
extern struct dumpInstantiations__option_t
450
{
451
  typedef bool type;
452
  type operator()() const;
453
  bool wasSetByUser() const;
454
  const char* getName() const;
455
} thread_local dumpInstantiations;
456
extern struct dumpModels__option_t
457
{
458
  typedef bool type;
459
  type operator()() const;
460
  bool wasSetByUser() const;
461
  const char* getName() const;
462
} thread_local dumpModels;
463
extern struct dumpProofs__option_t
464
{
465
  typedef bool type;
466
  type operator()() const;
467
  bool wasSetByUser() const;
468
  const char* getName() const;
469
} thread_local dumpProofs;
470
extern struct dumpToFileName__option_t
471
{
472
  typedef std::string type;
473
  type operator()() const;
474
  bool wasSetByUser() const;
475
  const char* getName() const;
476
} thread_local dumpToFileName;
477
extern struct dumpUnsatCores__option_t
478
{
479
  typedef bool type;
480
  type operator()() const;
481
  bool wasSetByUser() const;
482
  void set(const type& v);
483
  const char* getName() const;
484
} thread_local dumpUnsatCores;
485
extern struct dumpUnsatCoresFull__option_t
486
{
487
  typedef bool type;
488
  type operator()() const;
489
  bool wasSetByUser() const;
490
  const char* getName() const;
491
} thread_local dumpUnsatCoresFull;
492
extern struct dumpModeString__option_t
493
{
494
  typedef std::string type;
495
  type operator()() const;
496
  bool wasSetByUser() const;
497
  const char* getName() const;
498
} thread_local dumpModeString;
499
extern struct earlyIteRemoval__option_t
500
{
501
  typedef bool type;
502
  type operator()() const;
503
  bool wasSetByUser() const;
504
  void set(const type& v);
505
  const char* getName() const;
506
} thread_local earlyIteRemoval;
507
extern struct expandDefinitions__option_t
508
{
509
  typedef bool type;
510
  type operator()() const;
511
  bool wasSetByUser() const;
512
  const char* getName() const;
513
} thread_local expandDefinitions;
514
extern struct extRewPrep__option_t
515
{
516
  typedef bool type;
517
  type operator()() const;
518
  bool wasSetByUser() const;
519
  void set(const type& v);
520
  const char* getName() const;
521
} thread_local extRewPrep;
522
extern struct extRewPrepAgg__option_t
523
{
524
  typedef bool type;
525
  type operator()() const;
526
  bool wasSetByUser() const;
527
  void set(const type& v);
528
  const char* getName() const;
529
} thread_local extRewPrepAgg;
530
extern struct forceNoLimitCpuWhileDump__option_t
531
{
532
  typedef bool type;
533
  type operator()() const;
534
  bool wasSetByUser() const;
535
  const char* getName() const;
536
} thread_local forceNoLimitCpuWhileDump;
537
extern struct foreignTheoryRewrite__option_t
538
{
539
  typedef bool type;
540
  type operator()() const;
541
  bool wasSetByUser() const;
542
  const char* getName() const;
543
} thread_local foreignTheoryRewrite;
544
extern struct iandMode__option_t
545
{
546
  typedef IandMode type;
547
  type operator()() const;
548
  bool wasSetByUser() const;
549
  const char* getName() const;
550
} thread_local iandMode;
551
extern struct incrementalSolving__option_t
552
{
553
  typedef bool type;
554
  type operator()() const;
555
  bool wasSetByUser() const;
556
  void set(const type& v);
557
  const char* getName() const;
558
} thread_local incrementalSolving;
559
extern struct interactiveMode__option_t
560
{
561
  typedef bool type;
562
  type operator()() const;
563
  bool wasSetByUser() const;
564
  void set(const type& v);
565
  const char* getName() const;
566
} thread_local interactiveMode;
567
extern struct doITESimp__option_t
568
{
569
  typedef bool type;
570
  type operator()() const;
571
  bool wasSetByUser() const;
572
  void set(const type& v);
573
  const char* getName() const;
574
} thread_local doITESimp;
575
extern struct lemmaStep__option_t
576
{
577
  typedef unsigned type;
578
  type operator()() const;
579
  bool wasSetByUser() const;
580
  const char* getName() const;
581
} thread_local lemmaStep;
582
extern struct modelCoresMode__option_t
583
{
584
  typedef ModelCoresMode type;
585
  type operator()() const;
586
  bool wasSetByUser() const;
587
  void set(const type& v);
588
  const char* getName() const;
589
} thread_local modelCoresMode;
590
extern struct modelUninterpPrint__option_t
591
{
592
  typedef ModelUninterpPrintMode type;
593
  type operator()() const;
594
  bool wasSetByUser() const;
595
  const char* getName() const;
596
} thread_local modelUninterpPrint;
597
extern struct modelWitnessValue__option_t
598
{
599
  typedef bool type;
600
  type operator()() const;
601
  bool wasSetByUser() const;
602
  const char* getName() const;
603
} thread_local modelWitnessValue;
604
extern struct newSkolemStep__option_t
605
{
606
  typedef unsigned type;
607
  type operator()() const;
608
  bool wasSetByUser() const;
609
  const char* getName() const;
610
} thread_local newSkolemStep;
611
extern struct doITESimpOnRepeat__option_t
612
{
613
  typedef bool type;
614
  type operator()() const;
615
  bool wasSetByUser() const;
616
  void set(const type& v);
617
  const char* getName() const;
618
} thread_local doITESimpOnRepeat;
619
extern struct parseStep__option_t
620
{
621
  typedef unsigned type;
622
  type operator()() const;
623
  bool wasSetByUser() const;
624
  const char* getName() const;
625
} thread_local parseStep;
626
extern struct preprocessStep__option_t
627
{
628
  typedef unsigned type;
629
  type operator()() const;
630
  bool wasSetByUser() const;
631
  const char* getName() const;
632
} thread_local preprocessStep;
633
extern struct produceAbducts__option_t
634
{
635
  typedef bool type;
636
  type operator()() const;
637
  bool wasSetByUser() const;
638
  const char* getName() const;
639
} thread_local produceAbducts;
640
extern struct produceAssertions__option_t
641
{
642
  typedef bool type;
643
  type operator()() const;
644
  bool wasSetByUser() const;
645
  void set(const type& v);
646
  const char* getName() const;
647
} thread_local produceAssertions;
648
extern struct produceAssignments__option_t
649
{
650
  typedef bool type;
651
  type operator()() const;
652
  bool wasSetByUser() const;
653
  void set(const type& v);
654
  const char* getName() const;
655
} thread_local produceAssignments;
656
extern struct produceInterpols__option_t
657
{
658
  typedef ProduceInterpols type;
659
  type operator()() const;
660
  bool wasSetByUser() const;
661
  const char* getName() const;
662
} thread_local produceInterpols;
663
extern struct produceModels__option_t
664
{
665
  typedef bool type;
666
  type operator()() const;
667
  bool wasSetByUser() const;
668
  void set(const type& v);
669
  const char* getName() const;
670
} thread_local produceModels;
671
extern struct produceProofs__option_t
672
{
673
  typedef bool type;
674
  type operator()() const;
675
  bool wasSetByUser() const;
676
  void set(const type& v);
677
  const char* getName() const;
678
} thread_local produceProofs;
679
extern struct unsatAssumptions__option_t
680
{
681
  typedef bool type;
682
  type operator()() const;
683
  bool wasSetByUser() const;
684
  const char* getName() const;
685
} thread_local unsatAssumptions;
686
extern struct unsatCores__option_t
687
{
688
  typedef bool type;
689
  type operator()() const;
690
  bool wasSetByUser() const;
691
  void set(const type& v);
692
  const char* getName() const;
693
} thread_local unsatCores;
694
extern struct quantifierStep__option_t
695
{
696
  typedef unsigned type;
697
  type operator()() const;
698
  bool wasSetByUser() const;
699
  const char* getName() const;
700
} thread_local quantifierStep;
701
extern struct regularChannelName__option_t
702
{
703
  typedef std::string type;
704
  type operator()() const;
705
  bool wasSetByUser() const;
706
  const char* getName() const;
707
} thread_local regularChannelName;
708
extern struct repeatSimp__option_t
709
{
710
  typedef bool type;
711
  type operator()() const;
712
  bool wasSetByUser() const;
713
  void set(const type& v);
714
  const char* getName() const;
715
} thread_local repeatSimp;
716
extern struct restartStep__option_t
717
{
718
  typedef unsigned type;
719
  type operator()() const;
720
  bool wasSetByUser() const;
721
  const char* getName() const;
722
} thread_local restartStep;
723
extern struct rewriteStep__option_t
724
{
725
  typedef unsigned type;
726
  type operator()() const;
727
  bool wasSetByUser() const;
728
  const char* getName() const;
729
} thread_local rewriteStep;
730
extern struct perCallResourceLimit__option_t
731
{
732
  typedef unsigned long type;
733
  type operator()() const;
734
  bool wasSetByUser() const;
735
  const char* getName() const;
736
} thread_local perCallResourceLimit;
737
extern struct cumulativeResourceLimit__option_t
738
{
739
  typedef unsigned long type;
740
  type operator()() const;
741
  bool wasSetByUser() const;
742
  const char* getName() const;
743
} thread_local cumulativeResourceLimit;
744
extern struct satConflictStep__option_t
745
{
746
  typedef unsigned type;
747
  type operator()() const;
748
  bool wasSetByUser() const;
749
  const char* getName() const;
750
} thread_local satConflictStep;
751
extern struct compressItes__option_t
752
{
753
  typedef bool type;
754
  type operator()() const;
755
  bool wasSetByUser() const;
756
  void set(const type& v);
757
  const char* getName() const;
758
} thread_local compressItes;
759
extern struct zombieHuntThreshold__option_t
760
{
761
  typedef uint32_t type;
762
  type operator()() const;
763
  bool wasSetByUser() const;
764
  const char* getName() const;
765
} thread_local zombieHuntThreshold;
766
extern struct simplifyWithCareEnabled__option_t
767
{
768
  typedef bool type;
769
  type operator()() const;
770
  bool wasSetByUser() const;
771
  void set(const type& v);
772
  const char* getName() const;
773
} thread_local simplifyWithCareEnabled;
774
extern struct simplificationMode__option_t
775
{
776
  typedef SimplificationMode type;
777
  type operator()() const;
778
  bool wasSetByUser() const;
779
  void set(const type& v);
780
  const char* getName() const;
781
} thread_local simplificationMode;
782
extern struct solveBVAsInt__option_t
783
{
784
  typedef SolveBVAsIntMode type;
785
  type operator()() const;
786
  bool wasSetByUser() const;
787
  void set(const type& v);
788
  const char* getName() const;
789
} thread_local solveBVAsInt;
790
extern struct solveIntAsBV__option_t
791
{
792
  typedef uint32_t type;
793
  type operator()() const;
794
  bool wasSetByUser() const;
795
  const char* getName() const;
796
} thread_local solveIntAsBV;
797
extern struct solveRealAsInt__option_t
798
{
799
  typedef bool type;
800
  type operator()() const;
801
  bool wasSetByUser() const;
802
  const char* getName() const;
803
} thread_local solveRealAsInt;
804
extern struct sortInference__option_t
805
{
806
  typedef bool type;
807
  type operator()() const;
808
  bool wasSetByUser() const;
809
  void set(const type& v);
810
  const char* getName() const;
811
} thread_local sortInference;
812
extern struct doStaticLearning__option_t
813
{
814
  typedef bool type;
815
  type operator()() const;
816
  bool wasSetByUser() const;
817
  const char* getName() const;
818
} thread_local doStaticLearning;
819
extern struct sygusOut__option_t
820
{
821
  typedef SygusSolutionOutMode type;
822
  type operator()() const;
823
  bool wasSetByUser() const;
824
  void set(const type& v);
825
  const char* getName() const;
826
} thread_local sygusOut;
827
extern struct sygusPrintCallbacks__option_t
828
{
829
  typedef bool type;
830
  type operator()() const;
831
  bool wasSetByUser() const;
832
  const char* getName() const;
833
} thread_local sygusPrintCallbacks;
834
extern struct theoryCheckStep__option_t
835
{
836
  typedef unsigned type;
837
  type operator()() const;
838
  bool wasSetByUser() const;
839
  const char* getName() const;
840
} thread_local theoryCheckStep;
841
extern struct perCallMillisecondLimit__option_t
842
{
843
  typedef unsigned long type;
844
  type operator()() const;
845
  bool wasSetByUser() const;
846
  const char* getName() const;
847
} thread_local perCallMillisecondLimit;
848
extern struct cumulativeMillisecondLimit__option_t
849
{
850
  typedef unsigned long type;
851
  type operator()() const;
852
  bool wasSetByUser() const;
853
  const char* getName() const;
854
} thread_local cumulativeMillisecondLimit;
855
extern struct unconstrainedSimp__option_t
856
{
857
  typedef bool type;
858
  type operator()() const;
859
  bool wasSetByUser() const;
860
  void set(const type& v);
861
  const char* getName() const;
862
} thread_local unconstrainedSimp;
863
864
}  // namespace options
865
866
template <> const options::abstractValues__option_t::type& Options::operator[](
867
    options::abstractValues__option_t) const;
868
template <> bool Options::wasSetByUser(options::abstractValues__option_t) const;
869
template <> void Options::assignBool(
870
    options::abstractValues__option_t,
871
    std::string option,
872
    bool value);
873
template <> void Options::set(
874
    options::ackermann__option_t,
875
    const options::ackermann__option_t::type& x);
876
template <> const options::ackermann__option_t::type& Options::operator[](
877
    options::ackermann__option_t) const;
878
template <> bool Options::wasSetByUser(options::ackermann__option_t) const;
879
template <> void Options::assignBool(
880
    options::ackermann__option_t,
881
    std::string option,
882
    bool value);
883
template <> const options::arithNlLemmaStep__option_t::type& Options::operator[](
884
    options::arithNlLemmaStep__option_t) const;
885
template <> bool Options::wasSetByUser(options::arithNlLemmaStep__option_t) const;
886
template <> void Options::assign(
887
    options::arithNlLemmaStep__option_t,
888
    std::string option,
889
    std::string value);
890
template <> const options::arithPivotStep__option_t::type& Options::operator[](
891
    options::arithPivotStep__option_t) const;
892
template <> bool Options::wasSetByUser(options::arithPivotStep__option_t) const;
893
template <> void Options::assign(
894
    options::arithPivotStep__option_t,
895
    std::string option,
896
    std::string value);
897
template <> const options::bitblastStep__option_t::type& Options::operator[](
898
    options::bitblastStep__option_t) const;
899
template <> bool Options::wasSetByUser(options::bitblastStep__option_t) const;
900
template <> void Options::assign(
901
    options::bitblastStep__option_t,
902
    std::string option,
903
    std::string value);
904
template <> void Options::set(
905
    options::blockModelsMode__option_t,
906
    const options::blockModelsMode__option_t::type& x);
907
template <> const options::blockModelsMode__option_t::type& Options::operator[](
908
    options::blockModelsMode__option_t) const;
909
template <> bool Options::wasSetByUser(options::blockModelsMode__option_t) const;
910
template <> void Options::assign(
911
    options::blockModelsMode__option_t,
912
    std::string option,
913
    std::string value);
914
template <> const options::bvEagerAssertStep__option_t::type& Options::operator[](
915
    options::bvEagerAssertStep__option_t) const;
916
template <> bool Options::wasSetByUser(options::bvEagerAssertStep__option_t) const;
917
template <> void Options::assign(
918
    options::bvEagerAssertStep__option_t,
919
    std::string option,
920
    std::string value);
921
template <> const options::bvPropagationStep__option_t::type& Options::operator[](
922
    options::bvPropagationStep__option_t) const;
923
template <> bool Options::wasSetByUser(options::bvPropagationStep__option_t) const;
924
template <> void Options::assign(
925
    options::bvPropagationStep__option_t,
926
    std::string option,
927
    std::string value);
928
template <> const options::bvSatConflictStep__option_t::type& Options::operator[](
929
    options::bvSatConflictStep__option_t) const;
930
template <> bool Options::wasSetByUser(options::bvSatConflictStep__option_t) const;
931
template <> void Options::assign(
932
    options::bvSatConflictStep__option_t,
933
    std::string option,
934
    std::string value);
935
template <> const options::bvSatPropagateStep__option_t::type& Options::operator[](
936
    options::bvSatPropagateStep__option_t) const;
937
template <> bool Options::wasSetByUser(options::bvSatPropagateStep__option_t) const;
938
template <> void Options::assign(
939
    options::bvSatPropagateStep__option_t,
940
    std::string option,
941
    std::string value);
942
template <> const options::bvSatSimplifyStep__option_t::type& Options::operator[](
943
    options::bvSatSimplifyStep__option_t) const;
944
template <> bool Options::wasSetByUser(options::bvSatSimplifyStep__option_t) const;
945
template <> void Options::assign(
946
    options::bvSatSimplifyStep__option_t,
947
    std::string option,
948
    std::string value);
949
template <> const options::BVAndIntegerGranularity__option_t::type& Options::operator[](
950
    options::BVAndIntegerGranularity__option_t) const;
951
template <> bool Options::wasSetByUser(options::BVAndIntegerGranularity__option_t) const;
952
template <> void Options::assign(
953
    options::BVAndIntegerGranularity__option_t,
954
    std::string option,
955
    std::string value);
956
template <> const options::checkAbducts__option_t::type& Options::operator[](
957
    options::checkAbducts__option_t) const;
958
template <> bool Options::wasSetByUser(options::checkAbducts__option_t) const;
959
template <> void Options::assignBool(
960
    options::checkAbducts__option_t,
961
    std::string option,
962
    bool value);
963
template <> const options::checkInterpols__option_t::type& Options::operator[](
964
    options::checkInterpols__option_t) const;
965
template <> bool Options::wasSetByUser(options::checkInterpols__option_t) const;
966
template <> void Options::assignBool(
967
    options::checkInterpols__option_t,
968
    std::string option,
969
    bool value);
970
template <> void Options::set(
971
    options::checkModels__option_t,
972
    const options::checkModels__option_t::type& x);
973
template <> const options::checkModels__option_t::type& Options::operator[](
974
    options::checkModels__option_t) const;
975
template <> bool Options::wasSetByUser(options::checkModels__option_t) const;
976
template <> void Options::assignBool(
977
    options::checkModels__option_t,
978
    std::string option,
979
    bool value);
980
template <> void Options::set(
981
    options::checkProofs__option_t,
982
    const options::checkProofs__option_t::type& x);
983
template <> const options::checkProofs__option_t::type& Options::operator[](
984
    options::checkProofs__option_t) const;
985
template <> bool Options::wasSetByUser(options::checkProofs__option_t) const;
986
template <> void Options::assignBool(
987
    options::checkProofs__option_t,
988
    std::string option,
989
    bool value);
990
template <> void Options::set(
991
    options::checkSynthSol__option_t,
992
    const options::checkSynthSol__option_t::type& x);
993
template <> const options::checkSynthSol__option_t::type& Options::operator[](
994
    options::checkSynthSol__option_t) const;
995
template <> bool Options::wasSetByUser(options::checkSynthSol__option_t) const;
996
template <> void Options::assignBool(
997
    options::checkSynthSol__option_t,
998
    std::string option,
999
    bool value);
1000
template <> void Options::set(
1001
    options::checkUnsatCores__option_t,
1002
    const options::checkUnsatCores__option_t::type& x);
1003
template <> const options::checkUnsatCores__option_t::type& Options::operator[](
1004
    options::checkUnsatCores__option_t) const;
1005
template <> bool Options::wasSetByUser(options::checkUnsatCores__option_t) const;
1006
template <> void Options::assignBool(
1007
    options::checkUnsatCores__option_t,
1008
    std::string option,
1009
    bool value);
1010
template <> void Options::set(
1011
    options::checkUnsatCoresNew__option_t,
1012
    const options::checkUnsatCoresNew__option_t::type& x);
1013
template <> const options::checkUnsatCoresNew__option_t::type& Options::operator[](
1014
    options::checkUnsatCoresNew__option_t) const;
1015
template <> bool Options::wasSetByUser(options::checkUnsatCoresNew__option_t) const;
1016
template <> void Options::assignBool(
1017
    options::checkUnsatCoresNew__option_t,
1018
    std::string option,
1019
    bool value);
1020
template <> const options::cnfStep__option_t::type& Options::operator[](
1021
    options::cnfStep__option_t) const;
1022
template <> bool Options::wasSetByUser(options::cnfStep__option_t) const;
1023
template <> void Options::assign(
1024
    options::cnfStep__option_t,
1025
    std::string option,
1026
    std::string value);
1027
template <> void Options::set(
1028
    options::debugCheckModels__option_t,
1029
    const options::debugCheckModels__option_t::type& x);
1030
template <> const options::debugCheckModels__option_t::type& Options::operator[](
1031
    options::debugCheckModels__option_t) const;
1032
template <> bool Options::wasSetByUser(options::debugCheckModels__option_t) const;
1033
template <> void Options::assignBool(
1034
    options::debugCheckModels__option_t,
1035
    std::string option,
1036
    bool value);
1037
template <> const options::decisionStep__option_t::type& Options::operator[](
1038
    options::decisionStep__option_t) const;
1039
template <> bool Options::wasSetByUser(options::decisionStep__option_t) const;
1040
template <> void Options::assign(
1041
    options::decisionStep__option_t,
1042
    std::string option,
1043
    std::string value);
1044
template <> const options::diagnosticChannelName__option_t::type& Options::operator[](
1045
    options::diagnosticChannelName__option_t) const;
1046
template <> bool Options::wasSetByUser(options::diagnosticChannelName__option_t) const;
1047
template <> void Options::assign(
1048
    options::diagnosticChannelName__option_t,
1049
    std::string option,
1050
    std::string value);
1051
template <> const options::dumpInstantiations__option_t::type& Options::operator[](
1052
    options::dumpInstantiations__option_t) const;
1053
template <> bool Options::wasSetByUser(options::dumpInstantiations__option_t) const;
1054
template <> void Options::assignBool(
1055
    options::dumpInstantiations__option_t,
1056
    std::string option,
1057
    bool value);
1058
template <> const options::dumpModels__option_t::type& Options::operator[](
1059
    options::dumpModels__option_t) const;
1060
template <> bool Options::wasSetByUser(options::dumpModels__option_t) const;
1061
template <> void Options::assignBool(
1062
    options::dumpModels__option_t,
1063
    std::string option,
1064
    bool value);
1065
template <> const options::dumpProofs__option_t::type& Options::operator[](
1066
    options::dumpProofs__option_t) const;
1067
template <> bool Options::wasSetByUser(options::dumpProofs__option_t) const;
1068
template <> void Options::assignBool(
1069
    options::dumpProofs__option_t,
1070
    std::string option,
1071
    bool value);
1072
template <> const options::dumpToFileName__option_t::type& Options::operator[](
1073
    options::dumpToFileName__option_t) const;
1074
template <> bool Options::wasSetByUser(options::dumpToFileName__option_t) const;
1075
template <> void Options::assign(
1076
    options::dumpToFileName__option_t,
1077
    std::string option,
1078
    std::string value);
1079
template <> void Options::set(
1080
    options::dumpUnsatCores__option_t,
1081
    const options::dumpUnsatCores__option_t::type& x);
1082
template <> const options::dumpUnsatCores__option_t::type& Options::operator[](
1083
    options::dumpUnsatCores__option_t) const;
1084
template <> bool Options::wasSetByUser(options::dumpUnsatCores__option_t) const;
1085
template <> void Options::assignBool(
1086
    options::dumpUnsatCores__option_t,
1087
    std::string option,
1088
    bool value);
1089
template <> const options::dumpUnsatCoresFull__option_t::type& Options::operator[](
1090
    options::dumpUnsatCoresFull__option_t) const;
1091
template <> bool Options::wasSetByUser(options::dumpUnsatCoresFull__option_t) const;
1092
template <> void Options::assignBool(
1093
    options::dumpUnsatCoresFull__option_t,
1094
    std::string option,
1095
    bool value);
1096
template <> const options::dumpModeString__option_t::type& Options::operator[](
1097
    options::dumpModeString__option_t) const;
1098
template <> bool Options::wasSetByUser(options::dumpModeString__option_t) const;
1099
template <> void Options::assign(
1100
    options::dumpModeString__option_t,
1101
    std::string option,
1102
    std::string value);
1103
template <> void Options::set(
1104
    options::earlyIteRemoval__option_t,
1105
    const options::earlyIteRemoval__option_t::type& x);
1106
template <> const options::earlyIteRemoval__option_t::type& Options::operator[](
1107
    options::earlyIteRemoval__option_t) const;
1108
template <> bool Options::wasSetByUser(options::earlyIteRemoval__option_t) const;
1109
template <> void Options::assignBool(
1110
    options::earlyIteRemoval__option_t,
1111
    std::string option,
1112
    bool value);
1113
template <> const options::expandDefinitions__option_t::type& Options::operator[](
1114
    options::expandDefinitions__option_t) const;
1115
template <> bool Options::wasSetByUser(options::expandDefinitions__option_t) const;
1116
template <> void Options::assignBool(
1117
    options::expandDefinitions__option_t,
1118
    std::string option,
1119
    bool value);
1120
template <> void Options::set(
1121
    options::extRewPrep__option_t,
1122
    const options::extRewPrep__option_t::type& x);
1123
template <> const options::extRewPrep__option_t::type& Options::operator[](
1124
    options::extRewPrep__option_t) const;
1125
template <> bool Options::wasSetByUser(options::extRewPrep__option_t) const;
1126
template <> void Options::assignBool(
1127
    options::extRewPrep__option_t,
1128
    std::string option,
1129
    bool value);
1130
template <> void Options::set(
1131
    options::extRewPrepAgg__option_t,
1132
    const options::extRewPrepAgg__option_t::type& x);
1133
template <> const options::extRewPrepAgg__option_t::type& Options::operator[](
1134
    options::extRewPrepAgg__option_t) const;
1135
template <> bool Options::wasSetByUser(options::extRewPrepAgg__option_t) const;
1136
template <> void Options::assignBool(
1137
    options::extRewPrepAgg__option_t,
1138
    std::string option,
1139
    bool value);
1140
template <> const options::forceNoLimitCpuWhileDump__option_t::type& Options::operator[](
1141
    options::forceNoLimitCpuWhileDump__option_t) const;
1142
template <> bool Options::wasSetByUser(options::forceNoLimitCpuWhileDump__option_t) const;
1143
template <> void Options::assignBool(
1144
    options::forceNoLimitCpuWhileDump__option_t,
1145
    std::string option,
1146
    bool value);
1147
template <> const options::foreignTheoryRewrite__option_t::type& Options::operator[](
1148
    options::foreignTheoryRewrite__option_t) const;
1149
template <> bool Options::wasSetByUser(options::foreignTheoryRewrite__option_t) const;
1150
template <> void Options::assignBool(
1151
    options::foreignTheoryRewrite__option_t,
1152
    std::string option,
1153
    bool value);
1154
template <> const options::iandMode__option_t::type& Options::operator[](
1155
    options::iandMode__option_t) const;
1156
template <> bool Options::wasSetByUser(options::iandMode__option_t) const;
1157
template <> void Options::assign(
1158
    options::iandMode__option_t,
1159
    std::string option,
1160
    std::string value);
1161
template <> void Options::set(
1162
    options::incrementalSolving__option_t,
1163
    const options::incrementalSolving__option_t::type& x);
1164
template <> const options::incrementalSolving__option_t::type& Options::operator[](
1165
    options::incrementalSolving__option_t) const;
1166
template <> bool Options::wasSetByUser(options::incrementalSolving__option_t) const;
1167
template <> void Options::assignBool(
1168
    options::incrementalSolving__option_t,
1169
    std::string option,
1170
    bool value);
1171
template <> void Options::set(
1172
    options::interactiveMode__option_t,
1173
    const options::interactiveMode__option_t::type& x);
1174
template <> const options::interactiveMode__option_t::type& Options::operator[](
1175
    options::interactiveMode__option_t) const;
1176
template <> bool Options::wasSetByUser(options::interactiveMode__option_t) const;
1177
template <> void Options::assignBool(
1178
    options::interactiveMode__option_t,
1179
    std::string option,
1180
    bool value);
1181
template <> void Options::set(
1182
    options::doITESimp__option_t,
1183
    const options::doITESimp__option_t::type& x);
1184
template <> const options::doITESimp__option_t::type& Options::operator[](
1185
    options::doITESimp__option_t) const;
1186
template <> bool Options::wasSetByUser(options::doITESimp__option_t) const;
1187
template <> void Options::assignBool(
1188
    options::doITESimp__option_t,
1189
    std::string option,
1190
    bool value);
1191
template <> const options::lemmaStep__option_t::type& Options::operator[](
1192
    options::lemmaStep__option_t) const;
1193
template <> bool Options::wasSetByUser(options::lemmaStep__option_t) const;
1194
template <> void Options::assign(
1195
    options::lemmaStep__option_t,
1196
    std::string option,
1197
    std::string value);
1198
template <> void Options::set(
1199
    options::modelCoresMode__option_t,
1200
    const options::modelCoresMode__option_t::type& x);
1201
template <> const options::modelCoresMode__option_t::type& Options::operator[](
1202
    options::modelCoresMode__option_t) const;
1203
template <> bool Options::wasSetByUser(options::modelCoresMode__option_t) const;
1204
template <> void Options::assign(
1205
    options::modelCoresMode__option_t,
1206
    std::string option,
1207
    std::string value);
1208
template <> const options::modelUninterpPrint__option_t::type& Options::operator[](
1209
    options::modelUninterpPrint__option_t) const;
1210
template <> bool Options::wasSetByUser(options::modelUninterpPrint__option_t) const;
1211
template <> void Options::assign(
1212
    options::modelUninterpPrint__option_t,
1213
    std::string option,
1214
    std::string value);
1215
template <> const options::modelWitnessValue__option_t::type& Options::operator[](
1216
    options::modelWitnessValue__option_t) const;
1217
template <> bool Options::wasSetByUser(options::modelWitnessValue__option_t) const;
1218
template <> void Options::assignBool(
1219
    options::modelWitnessValue__option_t,
1220
    std::string option,
1221
    bool value);
1222
template <> const options::newSkolemStep__option_t::type& Options::operator[](
1223
    options::newSkolemStep__option_t) const;
1224
template <> bool Options::wasSetByUser(options::newSkolemStep__option_t) const;
1225
template <> void Options::assign(
1226
    options::newSkolemStep__option_t,
1227
    std::string option,
1228
    std::string value);
1229
template <> void Options::set(
1230
    options::doITESimpOnRepeat__option_t,
1231
    const options::doITESimpOnRepeat__option_t::type& x);
1232
template <> const options::doITESimpOnRepeat__option_t::type& Options::operator[](
1233
    options::doITESimpOnRepeat__option_t) const;
1234
template <> bool Options::wasSetByUser(options::doITESimpOnRepeat__option_t) const;
1235
template <> void Options::assignBool(
1236
    options::doITESimpOnRepeat__option_t,
1237
    std::string option,
1238
    bool value);
1239
template <> const options::parseStep__option_t::type& Options::operator[](
1240
    options::parseStep__option_t) const;
1241
template <> bool Options::wasSetByUser(options::parseStep__option_t) const;
1242
template <> void Options::assign(
1243
    options::parseStep__option_t,
1244
    std::string option,
1245
    std::string value);
1246
template <> const options::preprocessStep__option_t::type& Options::operator[](
1247
    options::preprocessStep__option_t) const;
1248
template <> bool Options::wasSetByUser(options::preprocessStep__option_t) const;
1249
template <> void Options::assign(
1250
    options::preprocessStep__option_t,
1251
    std::string option,
1252
    std::string value);
1253
template <> const options::produceAbducts__option_t::type& Options::operator[](
1254
    options::produceAbducts__option_t) const;
1255
template <> bool Options::wasSetByUser(options::produceAbducts__option_t) const;
1256
template <> void Options::assignBool(
1257
    options::produceAbducts__option_t,
1258
    std::string option,
1259
    bool value);
1260
template <> void Options::set(
1261
    options::produceAssertions__option_t,
1262
    const options::produceAssertions__option_t::type& x);
1263
template <> const options::produceAssertions__option_t::type& Options::operator[](
1264
    options::produceAssertions__option_t) const;
1265
template <> bool Options::wasSetByUser(options::produceAssertions__option_t) const;
1266
template <> void Options::assignBool(
1267
    options::produceAssertions__option_t,
1268
    std::string option,
1269
    bool value);
1270
template <> void Options::set(
1271
    options::produceAssignments__option_t,
1272
    const options::produceAssignments__option_t::type& x);
1273
template <> const options::produceAssignments__option_t::type& Options::operator[](
1274
    options::produceAssignments__option_t) const;
1275
template <> bool Options::wasSetByUser(options::produceAssignments__option_t) const;
1276
template <> void Options::assignBool(
1277
    options::produceAssignments__option_t,
1278
    std::string option,
1279
    bool value);
1280
template <> const options::produceInterpols__option_t::type& Options::operator[](
1281
    options::produceInterpols__option_t) const;
1282
template <> bool Options::wasSetByUser(options::produceInterpols__option_t) const;
1283
template <> void Options::assign(
1284
    options::produceInterpols__option_t,
1285
    std::string option,
1286
    std::string value);
1287
template <> void Options::set(
1288
    options::produceModels__option_t,
1289
    const options::produceModels__option_t::type& x);
1290
template <> const options::produceModels__option_t::type& Options::operator[](
1291
    options::produceModels__option_t) const;
1292
template <> bool Options::wasSetByUser(options::produceModels__option_t) const;
1293
template <> void Options::assignBool(
1294
    options::produceModels__option_t,
1295
    std::string option,
1296
    bool value);
1297
template <> void Options::set(
1298
    options::produceProofs__option_t,
1299
    const options::produceProofs__option_t::type& x);
1300
template <> const options::produceProofs__option_t::type& Options::operator[](
1301
    options::produceProofs__option_t) const;
1302
template <> bool Options::wasSetByUser(options::produceProofs__option_t) const;
1303
template <> void Options::assignBool(
1304
    options::produceProofs__option_t,
1305
    std::string option,
1306
    bool value);
1307
template <> const options::unsatAssumptions__option_t::type& Options::operator[](
1308
    options::unsatAssumptions__option_t) const;
1309
template <> bool Options::wasSetByUser(options::unsatAssumptions__option_t) const;
1310
template <> void Options::assignBool(
1311
    options::unsatAssumptions__option_t,
1312
    std::string option,
1313
    bool value);
1314
template <> void Options::set(
1315
    options::unsatCores__option_t,
1316
    const options::unsatCores__option_t::type& x);
1317
template <> const options::unsatCores__option_t::type& Options::operator[](
1318
    options::unsatCores__option_t) const;
1319
template <> bool Options::wasSetByUser(options::unsatCores__option_t) const;
1320
template <> void Options::assignBool(
1321
    options::unsatCores__option_t,
1322
    std::string option,
1323
    bool value);
1324
template <> const options::quantifierStep__option_t::type& Options::operator[](
1325
    options::quantifierStep__option_t) const;
1326
template <> bool Options::wasSetByUser(options::quantifierStep__option_t) const;
1327
template <> void Options::assign(
1328
    options::quantifierStep__option_t,
1329
    std::string option,
1330
    std::string value);
1331
template <> const options::regularChannelName__option_t::type& Options::operator[](
1332
    options::regularChannelName__option_t) const;
1333
template <> bool Options::wasSetByUser(options::regularChannelName__option_t) const;
1334
template <> void Options::assign(
1335
    options::regularChannelName__option_t,
1336
    std::string option,
1337
    std::string value);
1338
template <> void Options::set(
1339
    options::repeatSimp__option_t,
1340
    const options::repeatSimp__option_t::type& x);
1341
template <> const options::repeatSimp__option_t::type& Options::operator[](
1342
    options::repeatSimp__option_t) const;
1343
template <> bool Options::wasSetByUser(options::repeatSimp__option_t) const;
1344
template <> void Options::assignBool(
1345
    options::repeatSimp__option_t,
1346
    std::string option,
1347
    bool value);
1348
template <> const options::restartStep__option_t::type& Options::operator[](
1349
    options::restartStep__option_t) const;
1350
template <> bool Options::wasSetByUser(options::restartStep__option_t) const;
1351
template <> void Options::assign(
1352
    options::restartStep__option_t,
1353
    std::string option,
1354
    std::string value);
1355
template <> const options::rewriteStep__option_t::type& Options::operator[](
1356
    options::rewriteStep__option_t) const;
1357
template <> bool Options::wasSetByUser(options::rewriteStep__option_t) const;
1358
template <> void Options::assign(
1359
    options::rewriteStep__option_t,
1360
    std::string option,
1361
    std::string value);
1362
template <> const options::perCallResourceLimit__option_t::type& Options::operator[](
1363
    options::perCallResourceLimit__option_t) const;
1364
template <> bool Options::wasSetByUser(options::perCallResourceLimit__option_t) const;
1365
template <> void Options::assign(
1366
    options::perCallResourceLimit__option_t,
1367
    std::string option,
1368
    std::string value);
1369
template <> const options::cumulativeResourceLimit__option_t::type& Options::operator[](
1370
    options::cumulativeResourceLimit__option_t) const;
1371
template <> bool Options::wasSetByUser(options::cumulativeResourceLimit__option_t) const;
1372
template <> void Options::assign(
1373
    options::cumulativeResourceLimit__option_t,
1374
    std::string option,
1375
    std::string value);
1376
template <> const options::satConflictStep__option_t::type& Options::operator[](
1377
    options::satConflictStep__option_t) const;
1378
template <> bool Options::wasSetByUser(options::satConflictStep__option_t) const;
1379
template <> void Options::assign(
1380
    options::satConflictStep__option_t,
1381
    std::string option,
1382
    std::string value);
1383
template <> void Options::set(
1384
    options::compressItes__option_t,
1385
    const options::compressItes__option_t::type& x);
1386
template <> const options::compressItes__option_t::type& Options::operator[](
1387
    options::compressItes__option_t) const;
1388
template <> bool Options::wasSetByUser(options::compressItes__option_t) const;
1389
template <> void Options::assignBool(
1390
    options::compressItes__option_t,
1391
    std::string option,
1392
    bool value);
1393
template <> const options::zombieHuntThreshold__option_t::type& Options::operator[](
1394
    options::zombieHuntThreshold__option_t) const;
1395
template <> bool Options::wasSetByUser(options::zombieHuntThreshold__option_t) const;
1396
template <> void Options::assign(
1397
    options::zombieHuntThreshold__option_t,
1398
    std::string option,
1399
    std::string value);
1400
template <> void Options::set(
1401
    options::simplifyWithCareEnabled__option_t,
1402
    const options::simplifyWithCareEnabled__option_t::type& x);
1403
template <> const options::simplifyWithCareEnabled__option_t::type& Options::operator[](
1404
    options::simplifyWithCareEnabled__option_t) const;
1405
template <> bool Options::wasSetByUser(options::simplifyWithCareEnabled__option_t) const;
1406
template <> void Options::assignBool(
1407
    options::simplifyWithCareEnabled__option_t,
1408
    std::string option,
1409
    bool value);
1410
template <> void Options::set(
1411
    options::simplificationMode__option_t,
1412
    const options::simplificationMode__option_t::type& x);
1413
template <> const options::simplificationMode__option_t::type& Options::operator[](
1414
    options::simplificationMode__option_t) const;
1415
template <> bool Options::wasSetByUser(options::simplificationMode__option_t) const;
1416
template <> void Options::assign(
1417
    options::simplificationMode__option_t,
1418
    std::string option,
1419
    std::string value);
1420
template <> void Options::set(
1421
    options::solveBVAsInt__option_t,
1422
    const options::solveBVAsInt__option_t::type& x);
1423
template <> const options::solveBVAsInt__option_t::type& Options::operator[](
1424
    options::solveBVAsInt__option_t) const;
1425
template <> bool Options::wasSetByUser(options::solveBVAsInt__option_t) const;
1426
template <> void Options::assign(
1427
    options::solveBVAsInt__option_t,
1428
    std::string option,
1429
    std::string value);
1430
template <> const options::solveIntAsBV__option_t::type& Options::operator[](
1431
    options::solveIntAsBV__option_t) const;
1432
template <> bool Options::wasSetByUser(options::solveIntAsBV__option_t) const;
1433
template <> void Options::assign(
1434
    options::solveIntAsBV__option_t,
1435
    std::string option,
1436
    std::string value);
1437
template <> const options::solveRealAsInt__option_t::type& Options::operator[](
1438
    options::solveRealAsInt__option_t) const;
1439
template <> bool Options::wasSetByUser(options::solveRealAsInt__option_t) const;
1440
template <> void Options::assignBool(
1441
    options::solveRealAsInt__option_t,
1442
    std::string option,
1443
    bool value);
1444
template <> void Options::set(
1445
    options::sortInference__option_t,
1446
    const options::sortInference__option_t::type& x);
1447
template <> const options::sortInference__option_t::type& Options::operator[](
1448
    options::sortInference__option_t) const;
1449
template <> bool Options::wasSetByUser(options::sortInference__option_t) const;
1450
template <> void Options::assignBool(
1451
    options::sortInference__option_t,
1452
    std::string option,
1453
    bool value);
1454
template <> const options::doStaticLearning__option_t::type& Options::operator[](
1455
    options::doStaticLearning__option_t) const;
1456
template <> bool Options::wasSetByUser(options::doStaticLearning__option_t) const;
1457
template <> void Options::assignBool(
1458
    options::doStaticLearning__option_t,
1459
    std::string option,
1460
    bool value);
1461
template <> void Options::set(
1462
    options::sygusOut__option_t,
1463
    const options::sygusOut__option_t::type& x);
1464
template <> const options::sygusOut__option_t::type& Options::operator[](
1465
    options::sygusOut__option_t) const;
1466
template <> bool Options::wasSetByUser(options::sygusOut__option_t) const;
1467
template <> void Options::assign(
1468
    options::sygusOut__option_t,
1469
    std::string option,
1470
    std::string value);
1471
template <> const options::sygusPrintCallbacks__option_t::type& Options::operator[](
1472
    options::sygusPrintCallbacks__option_t) const;
1473
template <> bool Options::wasSetByUser(options::sygusPrintCallbacks__option_t) const;
1474
template <> void Options::assignBool(
1475
    options::sygusPrintCallbacks__option_t,
1476
    std::string option,
1477
    bool value);
1478
template <> const options::theoryCheckStep__option_t::type& Options::operator[](
1479
    options::theoryCheckStep__option_t) const;
1480
template <> bool Options::wasSetByUser(options::theoryCheckStep__option_t) const;
1481
template <> void Options::assign(
1482
    options::theoryCheckStep__option_t,
1483
    std::string option,
1484
    std::string value);
1485
template <> const options::perCallMillisecondLimit__option_t::type& Options::operator[](
1486
    options::perCallMillisecondLimit__option_t) const;
1487
template <> bool Options::wasSetByUser(options::perCallMillisecondLimit__option_t) const;
1488
template <> void Options::assign(
1489
    options::perCallMillisecondLimit__option_t,
1490
    std::string option,
1491
    std::string value);
1492
template <> const options::cumulativeMillisecondLimit__option_t::type& Options::operator[](
1493
    options::cumulativeMillisecondLimit__option_t) const;
1494
template <> bool Options::wasSetByUser(options::cumulativeMillisecondLimit__option_t) const;
1495
template <> void Options::assign(
1496
    options::cumulativeMillisecondLimit__option_t,
1497
    std::string option,
1498
    std::string value);
1499
template <> void Options::set(
1500
    options::unconstrainedSimp__option_t,
1501
    const options::unconstrainedSimp__option_t::type& x);
1502
template <> const options::unconstrainedSimp__option_t::type& Options::operator[](
1503
    options::unconstrainedSimp__option_t) const;
1504
template <> bool Options::wasSetByUser(options::unconstrainedSimp__option_t) const;
1505
template <> void Options::assignBool(
1506
    options::unconstrainedSimp__option_t,
1507
    std::string option,
1508
    bool value);
1509
1510
1511
namespace options {
1512
1513
3742
inline abstractValues__option_t::type abstractValues__option_t::operator()() const
1514
{
1515
3742
  return (*Options::current())[*this];
1516
}
1517
inline bool abstractValues__option_t::wasSetByUser() const
1518
{
1519
  return Options::current()->wasSetByUser(*this);
1520
}
1521
inline const char* abstractValues__option_t::getName() const
1522
{
1523
  return "abstract-values";
1524
}
1525
29313
inline ackermann__option_t::type ackermann__option_t::operator()() const
1526
{
1527
29313
  return (*Options::current())[*this];
1528
}
1529
inline bool ackermann__option_t::wasSetByUser() const
1530
{
1531
  return Options::current()->wasSetByUser(*this);
1532
}
1533
25
inline void ackermann__option_t::set(const ackermann__option_t::type& v)
1534
{
1535
25
  Options::current()->set(*this, v);
1536
25
}
1537
inline const char* ackermann__option_t::getName() const
1538
{
1539
  return "ackermann";
1540
}
1541
inline arithNlLemmaStep__option_t::type arithNlLemmaStep__option_t::operator()() const
1542
{
1543
  return (*Options::current())[*this];
1544
}
1545
inline bool arithNlLemmaStep__option_t::wasSetByUser() const
1546
{
1547
  return Options::current()->wasSetByUser(*this);
1548
}
1549
inline const char* arithNlLemmaStep__option_t::getName() const
1550
{
1551
  return "arith-nl-lemma-step";
1552
}
1553
inline arithPivotStep__option_t::type arithPivotStep__option_t::operator()() const
1554
{
1555
  return (*Options::current())[*this];
1556
}
1557
inline bool arithPivotStep__option_t::wasSetByUser() const
1558
{
1559
  return Options::current()->wasSetByUser(*this);
1560
}
1561
inline const char* arithPivotStep__option_t::getName() const
1562
{
1563
  return "arith-pivot-step";
1564
}
1565
inline bitblastStep__option_t::type bitblastStep__option_t::operator()() const
1566
{
1567
  return (*Options::current())[*this];
1568
}
1569
inline bool bitblastStep__option_t::wasSetByUser() const
1570
{
1571
  return Options::current()->wasSetByUser(*this);
1572
}
1573
inline const char* bitblastStep__option_t::getName() const
1574
{
1575
  return "bitblast-step";
1576
}
1577
6719
inline blockModelsMode__option_t::type blockModelsMode__option_t::operator()() const
1578
{
1579
6719
  return (*Options::current())[*this];
1580
}
1581
inline bool blockModelsMode__option_t::wasSetByUser() const
1582
{
1583
  return Options::current()->wasSetByUser(*this);
1584
}
1585
inline void blockModelsMode__option_t::set(const blockModelsMode__option_t::type& v)
1586
{
1587
  Options::current()->set(*this, v);
1588
}
1589
inline const char* blockModelsMode__option_t::getName() const
1590
{
1591
  return "block-models";
1592
}
1593
inline bvEagerAssertStep__option_t::type bvEagerAssertStep__option_t::operator()() const
1594
{
1595
  return (*Options::current())[*this];
1596
}
1597
inline bool bvEagerAssertStep__option_t::wasSetByUser() const
1598
{
1599
  return Options::current()->wasSetByUser(*this);
1600
}
1601
inline const char* bvEagerAssertStep__option_t::getName() const
1602
{
1603
  return "bv-eager-assert-step";
1604
}
1605
inline bvPropagationStep__option_t::type bvPropagationStep__option_t::operator()() const
1606
{
1607
  return (*Options::current())[*this];
1608
}
1609
inline bool bvPropagationStep__option_t::wasSetByUser() const
1610
{
1611
  return Options::current()->wasSetByUser(*this);
1612
}
1613
inline const char* bvPropagationStep__option_t::getName() const
1614
{
1615
  return "bv-propagation-step";
1616
}
1617
inline bvSatConflictStep__option_t::type bvSatConflictStep__option_t::operator()() const
1618
{
1619
  return (*Options::current())[*this];
1620
}
1621
inline bool bvSatConflictStep__option_t::wasSetByUser() const
1622
{
1623
  return Options::current()->wasSetByUser(*this);
1624
}
1625
inline const char* bvSatConflictStep__option_t::getName() const
1626
{
1627
  return "bv-sat-conflict-step";
1628
}
1629
inline bvSatPropagateStep__option_t::type bvSatPropagateStep__option_t::operator()() const
1630
{
1631
  return (*Options::current())[*this];
1632
}
1633
inline bool bvSatPropagateStep__option_t::wasSetByUser() const
1634
{
1635
  return Options::current()->wasSetByUser(*this);
1636
}
1637
inline const char* bvSatPropagateStep__option_t::getName() const
1638
{
1639
  return "bv-sat-propagate-step";
1640
}
1641
inline bvSatSimplifyStep__option_t::type bvSatSimplifyStep__option_t::operator()() const
1642
{
1643
  return (*Options::current())[*this];
1644
}
1645
inline bool bvSatSimplifyStep__option_t::wasSetByUser() const
1646
{
1647
  return Options::current()->wasSetByUser(*this);
1648
}
1649
inline const char* bvSatSimplifyStep__option_t::getName() const
1650
{
1651
  return "bv-sat-simplify-step";
1652
}
1653
150
inline BVAndIntegerGranularity__option_t::type BVAndIntegerGranularity__option_t::operator()() const
1654
{
1655
150
  return (*Options::current())[*this];
1656
}
1657
inline bool BVAndIntegerGranularity__option_t::wasSetByUser() const
1658
{
1659
  return Options::current()->wasSetByUser(*this);
1660
}
1661
inline const char* BVAndIntegerGranularity__option_t::getName() const
1662
{
1663
  return "bvand-integer-granularity";
1664
}
1665
18
inline checkAbducts__option_t::type checkAbducts__option_t::operator()() const
1666
{
1667
18
  return (*Options::current())[*this];
1668
}
1669
inline bool checkAbducts__option_t::wasSetByUser() const
1670
{
1671
  return Options::current()->wasSetByUser(*this);
1672
}
1673
inline const char* checkAbducts__option_t::getName() const
1674
{
1675
  return "check-abducts";
1676
}
1677
10
inline checkInterpols__option_t::type checkInterpols__option_t::operator()() const
1678
{
1679
10
  return (*Options::current())[*this];
1680
}
1681
inline bool checkInterpols__option_t::wasSetByUser() const
1682
{
1683
  return Options::current()->wasSetByUser(*this);
1684
}
1685
inline const char* checkInterpols__option_t::getName() const
1686
{
1687
  return "check-interpols";
1688
}
1689
49272
inline checkModels__option_t::type checkModels__option_t::operator()() const
1690
{
1691
49272
  return (*Options::current())[*this];
1692
}
1693
1
inline bool checkModels__option_t::wasSetByUser() const
1694
{
1695
1
  return Options::current()->wasSetByUser(*this);
1696
}
1697
1088
inline void checkModels__option_t::set(const checkModels__option_t::type& v)
1698
{
1699
1088
  Options::current()->set(*this, v);
1700
1088
}
1701
inline const char* checkModels__option_t::getName() const
1702
{
1703
  return "check-models";
1704
}
1705
23286
inline checkProofs__option_t::type checkProofs__option_t::operator()() const
1706
{
1707
23286
  return (*Options::current())[*this];
1708
}
1709
inline bool checkProofs__option_t::wasSetByUser() const
1710
{
1711
  return Options::current()->wasSetByUser(*this);
1712
}
1713
19
inline void checkProofs__option_t::set(const checkProofs__option_t::type& v)
1714
{
1715
19
  Options::current()->set(*this, v);
1716
19
}
1717
inline const char* checkProofs__option_t::getName() const
1718
{
1719
  return "check-proofs";
1720
}
1721
8258
inline checkSynthSol__option_t::type checkSynthSol__option_t::operator()() const
1722
{
1723
8258
  return (*Options::current())[*this];
1724
}
1725
inline bool checkSynthSol__option_t::wasSetByUser() const
1726
{
1727
  return Options::current()->wasSetByUser(*this);
1728
}
1729
inline void checkSynthSol__option_t::set(const checkSynthSol__option_t::type& v)
1730
{
1731
  Options::current()->set(*this, v);
1732
}
1733
inline const char* checkSynthSol__option_t::getName() const
1734
{
1735
  return "check-synth-sol";
1736
}
1737
21002
inline checkUnsatCores__option_t::type checkUnsatCores__option_t::operator()() const
1738
{
1739
21002
  return (*Options::current())[*this];
1740
}
1741
inline bool checkUnsatCores__option_t::wasSetByUser() const
1742
{
1743
  return Options::current()->wasSetByUser(*this);
1744
}
1745
inline void checkUnsatCores__option_t::set(const checkUnsatCores__option_t::type& v)
1746
{
1747
  Options::current()->set(*this, v);
1748
}
1749
inline const char* checkUnsatCores__option_t::getName() const
1750
{
1751
  return "check-unsat-cores";
1752
}
1753
29051
inline checkUnsatCoresNew__option_t::type checkUnsatCoresNew__option_t::operator()() const
1754
{
1755
29051
  return (*Options::current())[*this];
1756
}
1757
inline bool checkUnsatCoresNew__option_t::wasSetByUser() const
1758
{
1759
  return Options::current()->wasSetByUser(*this);
1760
}
1761
inline void checkUnsatCoresNew__option_t::set(const checkUnsatCoresNew__option_t::type& v)
1762
{
1763
  Options::current()->set(*this, v);
1764
}
1765
inline const char* checkUnsatCoresNew__option_t::getName() const
1766
{
1767
  return "check-unsat-cores-new";
1768
}
1769
inline cnfStep__option_t::type cnfStep__option_t::operator()() const
1770
{
1771
  return (*Options::current())[*this];
1772
}
1773
inline bool cnfStep__option_t::wasSetByUser() const
1774
{
1775
  return Options::current()->wasSetByUser(*this);
1776
}
1777
inline const char* cnfStep__option_t::getName() const
1778
{
1779
  return "cnf-step";
1780
}
1781
11840
inline debugCheckModels__option_t::type debugCheckModels__option_t::operator()() const
1782
{
1783
11840
  return (*Options::current())[*this];
1784
}
1785
inline bool debugCheckModels__option_t::wasSetByUser() const
1786
{
1787
  return Options::current()->wasSetByUser(*this);
1788
}
1789
inline void debugCheckModels__option_t::set(const debugCheckModels__option_t::type& v)
1790
{
1791
  Options::current()->set(*this, v);
1792
}
1793
inline const char* debugCheckModels__option_t::getName() const
1794
{
1795
  return "debug-check-models";
1796
}
1797
inline decisionStep__option_t::type decisionStep__option_t::operator()() const
1798
{
1799
  return (*Options::current())[*this];
1800
}
1801
inline bool decisionStep__option_t::wasSetByUser() const
1802
{
1803
  return Options::current()->wasSetByUser(*this);
1804
}
1805
inline const char* decisionStep__option_t::getName() const
1806
{
1807
  return "decision-step";
1808
}
1809
inline diagnosticChannelName__option_t::type diagnosticChannelName__option_t::operator()() const
1810
{
1811
  return (*Options::current())[*this];
1812
}
1813
inline bool diagnosticChannelName__option_t::wasSetByUser() const
1814
{
1815
  return Options::current()->wasSetByUser(*this);
1816
}
1817
9168
inline const char* diagnosticChannelName__option_t::getName() const
1818
{
1819
9168
  return "";
1820
}
1821
inline dumpInstantiations__option_t::type dumpInstantiations__option_t::operator()() const
1822
{
1823
  return (*Options::current())[*this];
1824
}
1825
inline bool dumpInstantiations__option_t::wasSetByUser() const
1826
{
1827
  return Options::current()->wasSetByUser(*this);
1828
}
1829
inline const char* dumpInstantiations__option_t::getName() const
1830
{
1831
  return "dump-instantiations";
1832
}
1833
7898
inline dumpModels__option_t::type dumpModels__option_t::operator()() const
1834
{
1835
7898
  return (*Options::current())[*this];
1836
}
1837
inline bool dumpModels__option_t::wasSetByUser() const
1838
{
1839
  return Options::current()->wasSetByUser(*this);
1840
}
1841
inline const char* dumpModels__option_t::getName() const
1842
{
1843
  return "dump-models";
1844
}
1845
8016
inline dumpProofs__option_t::type dumpProofs__option_t::operator()() const
1846
{
1847
8016
  return (*Options::current())[*this];
1848
}
1849
inline bool dumpProofs__option_t::wasSetByUser() const
1850
{
1851
  return Options::current()->wasSetByUser(*this);
1852
}
1853
inline const char* dumpProofs__option_t::getName() const
1854
{
1855
  return "dump-proofs";
1856
}
1857
inline dumpToFileName__option_t::type dumpToFileName__option_t::operator()() const
1858
{
1859
  return (*Options::current())[*this];
1860
}
1861
inline bool dumpToFileName__option_t::wasSetByUser() const
1862
{
1863
  return Options::current()->wasSetByUser(*this);
1864
}
1865
9168
inline const char* dumpToFileName__option_t::getName() const
1866
{
1867
9168
  return "dump-to";
1868
}
1869
8165
inline dumpUnsatCores__option_t::type dumpUnsatCores__option_t::operator()() const
1870
{
1871
8165
  return (*Options::current())[*this];
1872
}
1873
inline bool dumpUnsatCores__option_t::wasSetByUser() const
1874
{
1875
  return Options::current()->wasSetByUser(*this);
1876
}
1877
4
inline void dumpUnsatCores__option_t::set(const dumpUnsatCores__option_t::type& v)
1878
{
1879
4
  Options::current()->set(*this, v);
1880
4
}
1881
inline const char* dumpUnsatCores__option_t::getName() const
1882
{
1883
  return "dump-unsat-cores";
1884
}
1885
9005
inline dumpUnsatCoresFull__option_t::type dumpUnsatCoresFull__option_t::operator()() const
1886
{
1887
9005
  return (*Options::current())[*this];
1888
}
1889
inline bool dumpUnsatCoresFull__option_t::wasSetByUser() const
1890
{
1891
  return Options::current()->wasSetByUser(*this);
1892
}
1893
inline const char* dumpUnsatCoresFull__option_t::getName() const
1894
{
1895
  return "dump-unsat-cores-full";
1896
}
1897
inline dumpModeString__option_t::type dumpModeString__option_t::operator()() const
1898
{
1899
  return (*Options::current())[*this];
1900
}
1901
inline bool dumpModeString__option_t::wasSetByUser() const
1902
{
1903
  return Options::current()->wasSetByUser(*this);
1904
}
1905
9206
inline const char* dumpModeString__option_t::getName() const
1906
{
1907
9206
  return "dump";
1908
}
1909
11321
inline earlyIteRemoval__option_t::type earlyIteRemoval__option_t::operator()() const
1910
{
1911
11321
  return (*Options::current())[*this];
1912
}
1913
1
inline bool earlyIteRemoval__option_t::wasSetByUser() const
1914
{
1915
1
  return Options::current()->wasSetByUser(*this);
1916
}
1917
1
inline void earlyIteRemoval__option_t::set(const earlyIteRemoval__option_t::type& v)
1918
{
1919
1
  Options::current()->set(*this, v);
1920
1
}
1921
inline const char* earlyIteRemoval__option_t::getName() const
1922
{
1923
  return "early-ite-removal";
1924
}
1925
inline expandDefinitions__option_t::type expandDefinitions__option_t::operator()() const
1926
{
1927
  return (*Options::current())[*this];
1928
}
1929
inline bool expandDefinitions__option_t::wasSetByUser() const
1930
{
1931
  return Options::current()->wasSetByUser(*this);
1932
}
1933
inline const char* expandDefinitions__option_t::getName() const
1934
{
1935
  return "";
1936
}
1937
11323
inline extRewPrep__option_t::type extRewPrep__option_t::operator()() const
1938
{
1939
11323
  return (*Options::current())[*this];
1940
}
1941
inline bool extRewPrep__option_t::wasSetByUser() const
1942
{
1943
  return Options::current()->wasSetByUser(*this);
1944
}
1945
inline void extRewPrep__option_t::set(const extRewPrep__option_t::type& v)
1946
{
1947
  Options::current()->set(*this, v);
1948
}
1949
inline const char* extRewPrep__option_t::getName() const
1950
{
1951
  return "ext-rew-prep";
1952
}
1953
22
inline extRewPrepAgg__option_t::type extRewPrepAgg__option_t::operator()() const
1954
{
1955
22
  return (*Options::current())[*this];
1956
}
1957
inline bool extRewPrepAgg__option_t::wasSetByUser() const
1958
{
1959
  return Options::current()->wasSetByUser(*this);
1960
}
1961
inline void extRewPrepAgg__option_t::set(const extRewPrepAgg__option_t::type& v)
1962
{
1963
  Options::current()->set(*this, v);
1964
}
1965
inline const char* extRewPrepAgg__option_t::getName() const
1966
{
1967
  return "ext-rew-prep-agg";
1968
}
1969
inline forceNoLimitCpuWhileDump__option_t::type forceNoLimitCpuWhileDump__option_t::operator()() const
1970
{
1971
  return (*Options::current())[*this];
1972
}
1973
inline bool forceNoLimitCpuWhileDump__option_t::wasSetByUser() const
1974
{
1975
  return Options::current()->wasSetByUser(*this);
1976
}
1977
inline const char* forceNoLimitCpuWhileDump__option_t::getName() const
1978
{
1979
  return "force-no-limit-cpu-while-dump";
1980
}
1981
11323
inline foreignTheoryRewrite__option_t::type foreignTheoryRewrite__option_t::operator()() const
1982
{
1983
11323
  return (*Options::current())[*this];
1984
}
1985
inline bool foreignTheoryRewrite__option_t::wasSetByUser() const
1986
{
1987
  return Options::current()->wasSetByUser(*this);
1988
}
1989
inline const char* foreignTheoryRewrite__option_t::getName() const
1990
{
1991
  return "foreign-theory-rewrite";
1992
}
1993
43
inline iandMode__option_t::type iandMode__option_t::operator()() const
1994
{
1995
43
  return (*Options::current())[*this];
1996
}
1997
inline bool iandMode__option_t::wasSetByUser() const
1998
{
1999
  return Options::current()->wasSetByUser(*this);
2000
}
2001
inline const char* iandMode__option_t::getName() const
2002
{
2003
  return "iand-mode";
2004
}
2005
3955683
inline incrementalSolving__option_t::type incrementalSolving__option_t::operator()() const
2006
{
2007
3955683
  return (*Options::current())[*this];
2008
}
2009
inline bool incrementalSolving__option_t::wasSetByUser() const
2010
{
2011
  return Options::current()->wasSetByUser(*this);
2012
}
2013
inline void incrementalSolving__option_t::set(const incrementalSolving__option_t::type& v)
2014
{
2015
  Options::current()->set(*this, v);
2016
}
2017
inline const char* incrementalSolving__option_t::getName() const
2018
{
2019
  return "incremental";
2020
}
2021
inline interactiveMode__option_t::type interactiveMode__option_t::operator()() const
2022
{
2023
  return (*Options::current())[*this];
2024
}
2025
inline bool interactiveMode__option_t::wasSetByUser() const
2026
{
2027
  return Options::current()->wasSetByUser(*this);
2028
}
2029
8
inline void interactiveMode__option_t::set(const interactiveMode__option_t::type& v)
2030
{
2031
8
  Options::current()->set(*this, v);
2032
8
}
2033
inline const char* interactiveMode__option_t::getName() const
2034
{
2035
  return "";
2036
}
2037
21519
inline doITESimp__option_t::type doITESimp__option_t::operator()() const
2038
{
2039
21519
  return (*Options::current())[*this];
2040
}
2041
inline bool doITESimp__option_t::wasSetByUser() const
2042
{
2043
  return Options::current()->wasSetByUser(*this);
2044
}
2045
inline void doITESimp__option_t::set(const doITESimp__option_t::type& v)
2046
{
2047
  Options::current()->set(*this, v);
2048
}
2049
inline const char* doITESimp__option_t::getName() const
2050
{
2051
  return "ite-simp";
2052
}
2053
inline lemmaStep__option_t::type lemmaStep__option_t::operator()() const
2054
{
2055
  return (*Options::current())[*this];
2056
}
2057
inline bool lemmaStep__option_t::wasSetByUser() const
2058
{
2059
  return Options::current()->wasSetByUser(*this);
2060
}
2061
inline const char* lemmaStep__option_t::getName() const
2062
{
2063
  return "lemma-step";
2064
}
2065
6721
inline modelCoresMode__option_t::type modelCoresMode__option_t::operator()() const
2066
{
2067
6721
  return (*Options::current())[*this];
2068
}
2069
inline bool modelCoresMode__option_t::wasSetByUser() const
2070
{
2071
  return Options::current()->wasSetByUser(*this);
2072
}
2073
inline void modelCoresMode__option_t::set(const modelCoresMode__option_t::type& v)
2074
{
2075
  Options::current()->set(*this, v);
2076
}
2077
inline const char* modelCoresMode__option_t::getName() const
2078
{
2079
  return "model-cores";
2080
}
2081
45
inline modelUninterpPrint__option_t::type modelUninterpPrint__option_t::operator()() const
2082
{
2083
45
  return (*Options::current())[*this];
2084
}
2085
inline bool modelUninterpPrint__option_t::wasSetByUser() const
2086
{
2087
  return Options::current()->wasSetByUser(*this);
2088
}
2089
inline const char* modelUninterpPrint__option_t::getName() const
2090
{
2091
  return "model-u-print";
2092
}
2093
35
inline modelWitnessValue__option_t::type modelWitnessValue__option_t::operator()() const
2094
{
2095
35
  return (*Options::current())[*this];
2096
}
2097
inline bool modelWitnessValue__option_t::wasSetByUser() const
2098
{
2099
  return Options::current()->wasSetByUser(*this);
2100
}
2101
inline const char* modelWitnessValue__option_t::getName() const
2102
{
2103
  return "model-witness-value";
2104
}
2105
inline newSkolemStep__option_t::type newSkolemStep__option_t::operator()() const
2106
{
2107
  return (*Options::current())[*this];
2108
}
2109
inline bool newSkolemStep__option_t::wasSetByUser() const
2110
{
2111
  return Options::current()->wasSetByUser(*this);
2112
}
2113
inline const char* newSkolemStep__option_t::getName() const
2114
{
2115
  return "new-skolem-step";
2116
}
2117
inline doITESimpOnRepeat__option_t::type doITESimpOnRepeat__option_t::operator()() const
2118
{
2119
  return (*Options::current())[*this];
2120
}
2121
inline bool doITESimpOnRepeat__option_t::wasSetByUser() const
2122
{
2123
  return Options::current()->wasSetByUser(*this);
2124
}
2125
inline void doITESimpOnRepeat__option_t::set(const doITESimpOnRepeat__option_t::type& v)
2126
{
2127
  Options::current()->set(*this, v);
2128
}
2129
inline const char* doITESimpOnRepeat__option_t::getName() const
2130
{
2131
  return "on-repeat-ite-simp";
2132
}
2133
inline parseStep__option_t::type parseStep__option_t::operator()() const
2134
{
2135
  return (*Options::current())[*this];
2136
}
2137
inline bool parseStep__option_t::wasSetByUser() const
2138
{
2139
  return Options::current()->wasSetByUser(*this);
2140
}
2141
inline const char* parseStep__option_t::getName() const
2142
{
2143
  return "parse-step";
2144
}
2145
inline preprocessStep__option_t::type preprocessStep__option_t::operator()() const
2146
{
2147
  return (*Options::current())[*this];
2148
}
2149
inline bool preprocessStep__option_t::wasSetByUser() const
2150
{
2151
  return Options::current()->wasSetByUser(*this);
2152
}
2153
inline const char* preprocessStep__option_t::getName() const
2154
{
2155
  return "preprocess-step";
2156
}
2157
24129
inline produceAbducts__option_t::type produceAbducts__option_t::operator()() const
2158
{
2159
24129
  return (*Options::current())[*this];
2160
}
2161
inline bool produceAbducts__option_t::wasSetByUser() const
2162
{
2163
  return Options::current()->wasSetByUser(*this);
2164
}
2165
inline const char* produceAbducts__option_t::getName() const
2166
{
2167
  return "produce-abducts";
2168
}
2169
12343
inline produceAssertions__option_t::type produceAssertions__option_t::operator()() const
2170
{
2171
12343
  return (*Options::current())[*this];
2172
}
2173
inline bool produceAssertions__option_t::wasSetByUser() const
2174
{
2175
  return Options::current()->wasSetByUser(*this);
2176
}
2177
2238
inline void produceAssertions__option_t::set(const produceAssertions__option_t::type& v)
2178
{
2179
2238
  Options::current()->set(*this, v);
2180
2238
}
2181
inline const char* produceAssertions__option_t::getName() const
2182
{
2183
  return "produce-assertions";
2184
}
2185
15808
inline produceAssignments__option_t::type produceAssignments__option_t::operator()() const
2186
{
2187
15808
  return (*Options::current())[*this];
2188
}
2189
1
inline bool produceAssignments__option_t::wasSetByUser() const
2190
{
2191
1
  return Options::current()->wasSetByUser(*this);
2192
}
2193
1098
inline void produceAssignments__option_t::set(const produceAssignments__option_t::type& v)
2194
{
2195
1098
  Options::current()->set(*this, v);
2196
1098
}
2197
inline const char* produceAssignments__option_t::getName() const
2198
{
2199
  return "produce-assignments";
2200
}
2201
22222
inline produceInterpols__option_t::type produceInterpols__option_t::operator()() const
2202
{
2203
22222
  return (*Options::current())[*this];
2204
}
2205
inline bool produceInterpols__option_t::wasSetByUser() const
2206
{
2207
  return Options::current()->wasSetByUser(*this);
2208
}
2209
inline const char* produceInterpols__option_t::getName() const
2210
{
2211
  return "produce-interpols";
2212
}
2213
59400
inline produceModels__option_t::type produceModels__option_t::operator()() const
2214
{
2215
59400
  return (*Options::current())[*this];
2216
}
2217
2
inline bool produceModels__option_t::wasSetByUser() const
2218
{
2219
2
  return Options::current()->wasSetByUser(*this);
2220
}
2221
1555
inline void produceModels__option_t::set(const produceModels__option_t::type& v)
2222
{
2223
1555
  Options::current()->set(*this, v);
2224
1555
}
2225
inline const char* produceModels__option_t::getName() const
2226
{
2227
  return "produce-models";
2228
}
2229
32656429
inline produceProofs__option_t::type produceProofs__option_t::operator()() const
2230
{
2231
32656429
  return (*Options::current())[*this];
2232
}
2233
inline bool produceProofs__option_t::wasSetByUser() const
2234
{
2235
  return Options::current()->wasSetByUser(*this);
2236
}
2237
998
inline void produceProofs__option_t::set(const produceProofs__option_t::type& v)
2238
{
2239
998
  Options::current()->set(*this, v);
2240
998
}
2241
inline const char* produceProofs__option_t::getName() const
2242
{
2243
  return "produce-proofs";
2244
}
2245
8170
inline unsatAssumptions__option_t::type unsatAssumptions__option_t::operator()() const
2246
{
2247
8170
  return (*Options::current())[*this];
2248
}
2249
inline bool unsatAssumptions__option_t::wasSetByUser() const
2250
{
2251
  return Options::current()->wasSetByUser(*this);
2252
}
2253
inline const char* unsatAssumptions__option_t::getName() const
2254
{
2255
  return "produce-unsat-assumptions";
2256
}
2257
31136070
inline unsatCores__option_t::type unsatCores__option_t::operator()() const
2258
{
2259
31136070
  return (*Options::current())[*this];
2260
}
2261
inline bool unsatCores__option_t::wasSetByUser() const
2262
{
2263
  return Options::current()->wasSetByUser(*this);
2264
}
2265
968
inline void unsatCores__option_t::set(const unsatCores__option_t::type& v)
2266
{
2267
968
  Options::current()->set(*this, v);
2268
968
}
2269
inline const char* unsatCores__option_t::getName() const
2270
{
2271
  return "produce-unsat-cores";
2272
}
2273
inline quantifierStep__option_t::type quantifierStep__option_t::operator()() const
2274
{
2275
  return (*Options::current())[*this];
2276
}
2277
inline bool quantifierStep__option_t::wasSetByUser() const
2278
{
2279
  return Options::current()->wasSetByUser(*this);
2280
}
2281
inline const char* quantifierStep__option_t::getName() const
2282
{
2283
  return "quantifier-step";
2284
}
2285
inline regularChannelName__option_t::type regularChannelName__option_t::operator()() const
2286
{
2287
  return (*Options::current())[*this];
2288
}
2289
inline bool regularChannelName__option_t::wasSetByUser() const
2290
{
2291
  return Options::current()->wasSetByUser(*this);
2292
}
2293
9168
inline const char* regularChannelName__option_t::getName() const
2294
{
2295
9168
  return "";
2296
}
2297
23845
inline repeatSimp__option_t::type repeatSimp__option_t::operator()() const
2298
{
2299
23845
  return (*Options::current())[*this];
2300
}
2301
8995
inline bool repeatSimp__option_t::wasSetByUser() const
2302
{
2303
8995
  return Options::current()->wasSetByUser(*this);
2304
}
2305
8993
inline void repeatSimp__option_t::set(const repeatSimp__option_t::type& v)
2306
{
2307
8993
  Options::current()->set(*this, v);
2308
8993
}
2309
inline const char* repeatSimp__option_t::getName() const
2310
{
2311
  return "repeat-simp";
2312
}
2313
inline restartStep__option_t::type restartStep__option_t::operator()() const
2314
{
2315
  return (*Options::current())[*this];
2316
}
2317
inline bool restartStep__option_t::wasSetByUser() const
2318
{
2319
  return Options::current()->wasSetByUser(*this);
2320
}
2321
inline const char* restartStep__option_t::getName() const
2322
{
2323
  return "restart-step";
2324
}
2325
inline rewriteStep__option_t::type rewriteStep__option_t::operator()() const
2326
{
2327
  return (*Options::current())[*this];
2328
}
2329
inline bool rewriteStep__option_t::wasSetByUser() const
2330
{
2331
  return Options::current()->wasSetByUser(*this);
2332
}
2333
inline const char* rewriteStep__option_t::getName() const
2334
{
2335
  return "rewrite-step";
2336
}
2337
inline perCallResourceLimit__option_t::type perCallResourceLimit__option_t::operator()() const
2338
{
2339
  return (*Options::current())[*this];
2340
}
2341
inline bool perCallResourceLimit__option_t::wasSetByUser() const
2342
{
2343
  return Options::current()->wasSetByUser(*this);
2344
}
2345
inline const char* perCallResourceLimit__option_t::getName() const
2346
{
2347
  return "rlimit-per";
2348
}
2349
inline cumulativeResourceLimit__option_t::type cumulativeResourceLimit__option_t::operator()() const
2350
{
2351
  return (*Options::current())[*this];
2352
}
2353
inline bool cumulativeResourceLimit__option_t::wasSetByUser() const
2354
{
2355
  return Options::current()->wasSetByUser(*this);
2356
}
2357
inline const char* cumulativeResourceLimit__option_t::getName() const
2358
{
2359
  return "rlimit";
2360
}
2361
inline satConflictStep__option_t::type satConflictStep__option_t::operator()() const
2362
{
2363
  return (*Options::current())[*this];
2364
}
2365
inline bool satConflictStep__option_t::wasSetByUser() const
2366
{
2367
  return Options::current()->wasSetByUser(*this);
2368
}
2369
inline const char* satConflictStep__option_t::getName() const
2370
{
2371
  return "sat-conflict-step";
2372
}
2373
1
inline compressItes__option_t::type compressItes__option_t::operator()() const
2374
{
2375
1
  return (*Options::current())[*this];
2376
}
2377
inline bool compressItes__option_t::wasSetByUser() const
2378
{
2379
  return Options::current()->wasSetByUser(*this);
2380
}
2381
inline void compressItes__option_t::set(const compressItes__option_t::type& v)
2382
{
2383
  Options::current()->set(*this, v);
2384
}
2385
inline const char* compressItes__option_t::getName() const
2386
{
2387
  return "simp-ite-compress";
2388
}
2389
1
inline zombieHuntThreshold__option_t::type zombieHuntThreshold__option_t::operator()() const
2390
{
2391
1
  return (*Options::current())[*this];
2392
}
2393
inline bool zombieHuntThreshold__option_t::wasSetByUser() const
2394
{
2395
  return Options::current()->wasSetByUser(*this);
2396
}
2397
inline const char* zombieHuntThreshold__option_t::getName() const
2398
{
2399
  return "simp-ite-hunt-zombies";
2400
}
2401
1
inline simplifyWithCareEnabled__option_t::type simplifyWithCareEnabled__option_t::operator()() const
2402
{
2403
1
  return (*Options::current())[*this];
2404
}
2405
8995
inline bool simplifyWithCareEnabled__option_t::wasSetByUser() const
2406
{
2407
8995
  return Options::current()->wasSetByUser(*this);
2408
}
2409
8995
inline void simplifyWithCareEnabled__option_t::set(const simplifyWithCareEnabled__option_t::type& v)
2410
{
2411
8995
  Options::current()->set(*this, v);
2412
8995
}
2413
inline const char* simplifyWithCareEnabled__option_t::getName() const
2414
{
2415
  return "simp-with-care";
2416
}
2417
14178
inline simplificationMode__option_t::type simplificationMode__option_t::operator()() const
2418
{
2419
14178
  return (*Options::current())[*this];
2420
}
2421
8023
inline bool simplificationMode__option_t::wasSetByUser() const
2422
{
2423
8023
  return Options::current()->wasSetByUser(*this);
2424
}
2425
7997
inline void simplificationMode__option_t::set(const simplificationMode__option_t::type& v)
2426
{
2427
7997
  Options::current()->set(*this, v);
2428
7997
}
2429
inline const char* simplificationMode__option_t::getName() const
2430
{
2431
  return "simplification";
2432
}
2433
29377
inline solveBVAsInt__option_t::type solveBVAsInt__option_t::operator()() const
2434
{
2435
29377
  return (*Options::current())[*this];
2436
}
2437
inline bool solveBVAsInt__option_t::wasSetByUser() const
2438
{
2439
  return Options::current()->wasSetByUser(*this);
2440
}
2441
inline void solveBVAsInt__option_t::set(const solveBVAsInt__option_t::type& v)
2442
{
2443
  Options::current()->set(*this, v);
2444
}
2445
inline const char* solveBVAsInt__option_t::getName() const
2446
{
2447
  return "solve-bv-as-int";
2448
}
2449
33265
inline solveIntAsBV__option_t::type solveIntAsBV__option_t::operator()() const
2450
{
2451
33265
  return (*Options::current())[*this];
2452
}
2453
inline bool solveIntAsBV__option_t::wasSetByUser() const
2454
{
2455
  return Options::current()->wasSetByUser(*this);
2456
}
2457
inline const char* solveIntAsBV__option_t::getName() const
2458
{
2459
  return "solve-int-as-bv";
2460
}
2461
23722
inline solveRealAsInt__option_t::type solveRealAsInt__option_t::operator()() const
2462
{
2463
23722
  return (*Options::current())[*this];
2464
}
2465
inline bool solveRealAsInt__option_t::wasSetByUser() const
2466
{
2467
  return Options::current()->wasSetByUser(*this);
2468
}
2469
inline const char* solveRealAsInt__option_t::getName() const
2470
{
2471
  return "solve-real-as-int";
2472
}
2473
31077
inline sortInference__option_t::type sortInference__option_t::operator()() const
2474
{
2475
31077
  return (*Options::current())[*this];
2476
}
2477
inline bool sortInference__option_t::wasSetByUser() const
2478
{
2479
  return Options::current()->wasSetByUser(*this);
2480
}
2481
1529
inline void sortInference__option_t::set(const sortInference__option_t::type& v)
2482
{
2483
1529
  Options::current()->set(*this, v);
2484
1529
}
2485
inline const char* sortInference__option_t::getName() const
2486
{
2487
  return "sort-inference";
2488
}
2489
11321
inline doStaticLearning__option_t::type doStaticLearning__option_t::operator()() const
2490
{
2491
11321
  return (*Options::current())[*this];
2492
}
2493
inline bool doStaticLearning__option_t::wasSetByUser() const
2494
{
2495
  return Options::current()->wasSetByUser(*this);
2496
}
2497
inline const char* doStaticLearning__option_t::getName() const
2498
{
2499
  return "static-learning";
2500
}
2501
1347
inline sygusOut__option_t::type sygusOut__option_t::operator()() const
2502
{
2503
1347
  return (*Options::current())[*this];
2504
}
2505
inline bool sygusOut__option_t::wasSetByUser() const
2506
{
2507
  return Options::current()->wasSetByUser(*this);
2508
}
2509
inline void sygusOut__option_t::set(const sygusOut__option_t::type& v)
2510
{
2511
  Options::current()->set(*this, v);
2512
}
2513
inline const char* sygusOut__option_t::getName() const
2514
{
2515
  return "sygus-out";
2516
}
2517
inline sygusPrintCallbacks__option_t::type sygusPrintCallbacks__option_t::operator()() const
2518
{
2519
  return (*Options::current())[*this];
2520
}
2521
inline bool sygusPrintCallbacks__option_t::wasSetByUser() const
2522
{
2523
  return Options::current()->wasSetByUser(*this);
2524
}
2525
inline const char* sygusPrintCallbacks__option_t::getName() const
2526
{
2527
  return "sygus-print-callbacks";
2528
}
2529
inline theoryCheckStep__option_t::type theoryCheckStep__option_t::operator()() const
2530
{
2531
  return (*Options::current())[*this];
2532
}
2533
inline bool theoryCheckStep__option_t::wasSetByUser() const
2534
{
2535
  return Options::current()->wasSetByUser(*this);
2536
}
2537
inline const char* theoryCheckStep__option_t::getName() const
2538
{
2539
  return "theory-check-step";
2540
}
2541
7
inline perCallMillisecondLimit__option_t::type perCallMillisecondLimit__option_t::operator()() const
2542
{
2543
7
  return (*Options::current())[*this];
2544
}
2545
inline bool perCallMillisecondLimit__option_t::wasSetByUser() const
2546
{
2547
  return Options::current()->wasSetByUser(*this);
2548
}
2549
inline const char* perCallMillisecondLimit__option_t::getName() const
2550
{
2551
  return "tlimit-per";
2552
}
2553
inline cumulativeMillisecondLimit__option_t::type cumulativeMillisecondLimit__option_t::operator()() const
2554
{
2555
  return (*Options::current())[*this];
2556
}
2557
inline bool cumulativeMillisecondLimit__option_t::wasSetByUser() const
2558
{
2559
  return Options::current()->wasSetByUser(*this);
2560
}
2561
inline const char* cumulativeMillisecondLimit__option_t::getName() const
2562
{
2563
  return "tlimit";
2564
}
2565
25353
inline unconstrainedSimp__option_t::type unconstrainedSimp__option_t::operator()() const
2566
{
2567
25353
  return (*Options::current())[*this];
2568
}
2569
14738
inline bool unconstrainedSimp__option_t::wasSetByUser() const
2570
{
2571
14738
  return Options::current()->wasSetByUser(*this);
2572
}
2573
5672
inline void unconstrainedSimp__option_t::set(const unconstrainedSimp__option_t::type& v)
2574
{
2575
5672
  Options::current()->set(*this, v);
2576
5672
}
2577
inline const char* unconstrainedSimp__option_t::getName() const
2578
{
2579
  return "unconstrained-simp";
2580
}
2581
2582
}  // namespace options
2583
}  // namespace CVC4
2584
2585
#endif /* CVC4__OPTIONS__SMT_H */