GCC Code Coverage Report
Directory: . Exec Total Coverage
File: build-coverage/src/options/datatypes_options.h Lines: 43 43 100.0 %
Date: 2021-03-23 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__DATATYPES_H
21
#define CVC4__OPTIONS__DATATYPES_H
22
23
#include "options/options.h"
24
25
26
27
28
#define CVC4_OPTIONS__DATATYPES__FOR_OPTION_HOLDER \
29
  cdtBisimilar__option_t::type cdtBisimilar;\
30
  bool cdtBisimilar__setByUser__; \
31
  dtBinarySplit__option_t::type dtBinarySplit;\
32
  bool dtBinarySplit__setByUser__; \
33
  dtBlastSplits__option_t::type dtBlastSplits;\
34
  bool dtBlastSplits__setByUser__; \
35
  dtCyclic__option_t::type dtCyclic;\
36
  bool dtCyclic__setByUser__; \
37
  dtForceAssignment__option_t::type dtForceAssignment;\
38
  bool dtForceAssignment__setByUser__; \
39
  dtInferAsLemmas__option_t::type dtInferAsLemmas;\
40
  bool dtInferAsLemmas__setByUser__; \
41
  dtNestedRec__option_t::type dtNestedRec;\
42
  bool dtNestedRec__setByUser__; \
43
  dtPoliteOptimize__option_t::type dtPoliteOptimize;\
44
  bool dtPoliteOptimize__setByUser__; \
45
  dtRewriteErrorSel__option_t::type dtRewriteErrorSel;\
46
  bool dtRewriteErrorSel__setByUser__; \
47
  dtSharedSelectors__option_t::type dtSharedSelectors;\
48
  bool dtSharedSelectors__setByUser__; \
49
  sygusAbortSize__option_t::type sygusAbortSize;\
50
  bool sygusAbortSize__setByUser__; \
51
  sygusFairMax__option_t::type sygusFairMax;\
52
  bool sygusFairMax__setByUser__; \
53
  sygusFair__option_t::type sygusFair;\
54
  bool sygusFair__setByUser__; \
55
  sygusSymBreak__option_t::type sygusSymBreak;\
56
  bool sygusSymBreak__setByUser__; \
57
  sygusSymBreakAgg__option_t::type sygusSymBreakAgg;\
58
  bool sygusSymBreakAgg__setByUser__; \
59
  sygusSymBreakDynamic__option_t::type sygusSymBreakDynamic;\
60
  bool sygusSymBreakDynamic__setByUser__; \
61
  sygusSymBreakLazy__option_t::type sygusSymBreakLazy;\
62
  bool sygusSymBreakLazy__setByUser__; \
63
  sygusSymBreakPbe__option_t::type sygusSymBreakPbe;\
64
  bool sygusSymBreakPbe__setByUser__; \
65
  sygusSymBreakRlv__option_t::type sygusSymBreakRlv;\
66
  bool sygusSymBreakRlv__setByUser__;
67
68
69
namespace CVC4 {
70
71
namespace options {
72
73
74
enum class SygusFairMode
75
{
76
  DT_SIZE_PRED,
77
  DT_SIZE,
78
  DT_HEIGHT_PRED,
79
  NONE,
80
  DIRECT
81
};
82
std::ostream&
83
operator<<(std::ostream& os, SygusFairMode mode);
84
SygusFairMode
85
stringToSygusFairMode(const std::string& option, const std::string& optarg);
86
87
extern struct cdtBisimilar__option_t
88
{
89
  typedef bool type;
90
  type operator()() const;
91
  bool wasSetByUser() const;
92
  const char* getName() const;
93
} thread_local cdtBisimilar;
94
extern struct dtBinarySplit__option_t
95
{
96
  typedef bool type;
97
  type operator()() const;
98
  bool wasSetByUser() const;
99
  const char* getName() const;
100
} thread_local dtBinarySplit;
101
extern struct dtBlastSplits__option_t
102
{
103
  typedef bool type;
104
  type operator()() const;
105
  bool wasSetByUser() const;
106
  const char* getName() const;
107
} thread_local dtBlastSplits;
108
extern struct dtCyclic__option_t
109
{
110
  typedef bool type;
111
  type operator()() const;
112
  bool wasSetByUser() const;
113
  const char* getName() const;
114
} thread_local dtCyclic;
115
extern struct dtForceAssignment__option_t
116
{
117
  typedef bool type;
118
  type operator()() const;
119
  bool wasSetByUser() const;
120
  void set(const type& v);
121
  const char* getName() const;
122
} thread_local dtForceAssignment;
123
extern struct dtInferAsLemmas__option_t
124
{
125
  typedef bool type;
126
  type operator()() const;
127
  bool wasSetByUser() const;
128
  const char* getName() const;
129
} thread_local dtInferAsLemmas;
130
extern struct dtNestedRec__option_t
131
{
132
  typedef bool type;
133
  type operator()() const;
134
  bool wasSetByUser() const;
135
  const char* getName() const;
136
} thread_local dtNestedRec;
137
extern struct dtPoliteOptimize__option_t
138
{
139
  typedef bool type;
140
  type operator()() const;
141
  bool wasSetByUser() const;
142
  const char* getName() const;
143
} thread_local dtPoliteOptimize;
144
extern struct dtRewriteErrorSel__option_t
145
{
146
  typedef bool type;
147
  type operator()() const;
148
  bool wasSetByUser() const;
149
  void set(const type& v);
150
  const char* getName() const;
151
} thread_local dtRewriteErrorSel;
152
extern struct dtSharedSelectors__option_t
153
{
154
  typedef bool type;
155
  type operator()() const;
156
  bool wasSetByUser() const;
157
  const char* getName() const;
158
} thread_local dtSharedSelectors;
159
extern struct sygusAbortSize__option_t
160
{
161
  typedef int type;
162
  type operator()() const;
163
  bool wasSetByUser() const;
164
  const char* getName() const;
165
} thread_local sygusAbortSize;
166
extern struct sygusFairMax__option_t
167
{
168
  typedef bool type;
169
  type operator()() const;
170
  bool wasSetByUser() const;
171
  const char* getName() const;
172
} thread_local sygusFairMax;
173
extern struct sygusFair__option_t
174
{
175
  typedef SygusFairMode type;
176
  type operator()() const;
177
  bool wasSetByUser() const;
178
  const char* getName() const;
179
} thread_local sygusFair;
180
extern struct sygusSymBreak__option_t
181
{
182
  typedef bool type;
183
  type operator()() const;
184
  bool wasSetByUser() const;
185
  const char* getName() const;
186
} thread_local sygusSymBreak;
187
extern struct sygusSymBreakAgg__option_t
188
{
189
  typedef bool type;
190
  type operator()() const;
191
  bool wasSetByUser() const;
192
  const char* getName() const;
193
} thread_local sygusSymBreakAgg;
194
extern struct sygusSymBreakDynamic__option_t
195
{
196
  typedef bool type;
197
  type operator()() const;
198
  bool wasSetByUser() const;
199
  const char* getName() const;
200
} thread_local sygusSymBreakDynamic;
201
extern struct sygusSymBreakLazy__option_t
202
{
203
  typedef bool type;
204
  type operator()() const;
205
  bool wasSetByUser() const;
206
  const char* getName() const;
207
} thread_local sygusSymBreakLazy;
208
extern struct sygusSymBreakPbe__option_t
209
{
210
  typedef bool type;
211
  type operator()() const;
212
  bool wasSetByUser() const;
213
  void set(const type& v);
214
  const char* getName() const;
215
} thread_local sygusSymBreakPbe;
216
extern struct sygusSymBreakRlv__option_t
217
{
218
  typedef bool type;
219
  type operator()() const;
220
  bool wasSetByUser() const;
221
  const char* getName() const;
222
} thread_local sygusSymBreakRlv;
223
224
}  // namespace options
225
226
template <> const options::cdtBisimilar__option_t::type& Options::operator[](
227
    options::cdtBisimilar__option_t) const;
228
template <> bool Options::wasSetByUser(options::cdtBisimilar__option_t) const;
229
template <> void Options::assignBool(
230
    options::cdtBisimilar__option_t,
231
    std::string option,
232
    bool value);
233
template <> const options::dtBinarySplit__option_t::type& Options::operator[](
234
    options::dtBinarySplit__option_t) const;
235
template <> bool Options::wasSetByUser(options::dtBinarySplit__option_t) const;
236
template <> void Options::assignBool(
237
    options::dtBinarySplit__option_t,
238
    std::string option,
239
    bool value);
240
template <> const options::dtBlastSplits__option_t::type& Options::operator[](
241
    options::dtBlastSplits__option_t) const;
242
template <> bool Options::wasSetByUser(options::dtBlastSplits__option_t) const;
243
template <> void Options::assignBool(
244
    options::dtBlastSplits__option_t,
245
    std::string option,
246
    bool value);
247
template <> const options::dtCyclic__option_t::type& Options::operator[](
248
    options::dtCyclic__option_t) const;
249
template <> bool Options::wasSetByUser(options::dtCyclic__option_t) const;
250
template <> void Options::assignBool(
251
    options::dtCyclic__option_t,
252
    std::string option,
253
    bool value);
254
template <> void Options::set(
255
    options::dtForceAssignment__option_t,
256
    const options::dtForceAssignment__option_t::type& x);
257
template <> const options::dtForceAssignment__option_t::type& Options::operator[](
258
    options::dtForceAssignment__option_t) const;
259
template <> bool Options::wasSetByUser(options::dtForceAssignment__option_t) const;
260
template <> void Options::assignBool(
261
    options::dtForceAssignment__option_t,
262
    std::string option,
263
    bool value);
264
template <> const options::dtInferAsLemmas__option_t::type& Options::operator[](
265
    options::dtInferAsLemmas__option_t) const;
266
template <> bool Options::wasSetByUser(options::dtInferAsLemmas__option_t) const;
267
template <> void Options::assignBool(
268
    options::dtInferAsLemmas__option_t,
269
    std::string option,
270
    bool value);
271
template <> const options::dtNestedRec__option_t::type& Options::operator[](
272
    options::dtNestedRec__option_t) const;
273
template <> bool Options::wasSetByUser(options::dtNestedRec__option_t) const;
274
template <> void Options::assignBool(
275
    options::dtNestedRec__option_t,
276
    std::string option,
277
    bool value);
278
template <> const options::dtPoliteOptimize__option_t::type& Options::operator[](
279
    options::dtPoliteOptimize__option_t) const;
280
template <> bool Options::wasSetByUser(options::dtPoliteOptimize__option_t) const;
281
template <> void Options::assignBool(
282
    options::dtPoliteOptimize__option_t,
283
    std::string option,
284
    bool value);
285
template <> void Options::set(
286
    options::dtRewriteErrorSel__option_t,
287
    const options::dtRewriteErrorSel__option_t::type& x);
288
template <> const options::dtRewriteErrorSel__option_t::type& Options::operator[](
289
    options::dtRewriteErrorSel__option_t) const;
290
template <> bool Options::wasSetByUser(options::dtRewriteErrorSel__option_t) const;
291
template <> void Options::assignBool(
292
    options::dtRewriteErrorSel__option_t,
293
    std::string option,
294
    bool value);
295
template <> const options::dtSharedSelectors__option_t::type& Options::operator[](
296
    options::dtSharedSelectors__option_t) const;
297
template <> bool Options::wasSetByUser(options::dtSharedSelectors__option_t) const;
298
template <> void Options::assignBool(
299
    options::dtSharedSelectors__option_t,
300
    std::string option,
301
    bool value);
302
template <> const options::sygusAbortSize__option_t::type& Options::operator[](
303
    options::sygusAbortSize__option_t) const;
304
template <> bool Options::wasSetByUser(options::sygusAbortSize__option_t) const;
305
template <> void Options::assign(
306
    options::sygusAbortSize__option_t,
307
    std::string option,
308
    std::string value);
309
template <> const options::sygusFairMax__option_t::type& Options::operator[](
310
    options::sygusFairMax__option_t) const;
311
template <> bool Options::wasSetByUser(options::sygusFairMax__option_t) const;
312
template <> void Options::assignBool(
313
    options::sygusFairMax__option_t,
314
    std::string option,
315
    bool value);
316
template <> const options::sygusFair__option_t::type& Options::operator[](
317
    options::sygusFair__option_t) const;
318
template <> bool Options::wasSetByUser(options::sygusFair__option_t) const;
319
template <> void Options::assign(
320
    options::sygusFair__option_t,
321
    std::string option,
322
    std::string value);
323
template <> const options::sygusSymBreak__option_t::type& Options::operator[](
324
    options::sygusSymBreak__option_t) const;
325
template <> bool Options::wasSetByUser(options::sygusSymBreak__option_t) const;
326
template <> void Options::assignBool(
327
    options::sygusSymBreak__option_t,
328
    std::string option,
329
    bool value);
330
template <> const options::sygusSymBreakAgg__option_t::type& Options::operator[](
331
    options::sygusSymBreakAgg__option_t) const;
332
template <> bool Options::wasSetByUser(options::sygusSymBreakAgg__option_t) const;
333
template <> void Options::assignBool(
334
    options::sygusSymBreakAgg__option_t,
335
    std::string option,
336
    bool value);
337
template <> const options::sygusSymBreakDynamic__option_t::type& Options::operator[](
338
    options::sygusSymBreakDynamic__option_t) const;
339
template <> bool Options::wasSetByUser(options::sygusSymBreakDynamic__option_t) const;
340
template <> void Options::assignBool(
341
    options::sygusSymBreakDynamic__option_t,
342
    std::string option,
343
    bool value);
344
template <> const options::sygusSymBreakLazy__option_t::type& Options::operator[](
345
    options::sygusSymBreakLazy__option_t) const;
346
template <> bool Options::wasSetByUser(options::sygusSymBreakLazy__option_t) const;
347
template <> void Options::assignBool(
348
    options::sygusSymBreakLazy__option_t,
349
    std::string option,
350
    bool value);
351
template <> void Options::set(
352
    options::sygusSymBreakPbe__option_t,
353
    const options::sygusSymBreakPbe__option_t::type& x);
354
template <> const options::sygusSymBreakPbe__option_t::type& Options::operator[](
355
    options::sygusSymBreakPbe__option_t) const;
356
template <> bool Options::wasSetByUser(options::sygusSymBreakPbe__option_t) const;
357
template <> void Options::assignBool(
358
    options::sygusSymBreakPbe__option_t,
359
    std::string option,
360
    bool value);
361
template <> const options::sygusSymBreakRlv__option_t::type& Options::operator[](
362
    options::sygusSymBreakRlv__option_t) const;
363
template <> bool Options::wasSetByUser(options::sygusSymBreakRlv__option_t) const;
364
template <> void Options::assignBool(
365
    options::sygusSymBreakRlv__option_t,
366
    std::string option,
367
    bool value);
368
369
370
namespace options {
371
372
85
inline cdtBisimilar__option_t::type cdtBisimilar__option_t::operator()() const
373
{
374
85
  return (*Options::current())[*this];
375
}
376
inline bool cdtBisimilar__option_t::wasSetByUser() const
377
{
378
  return Options::current()->wasSetByUser(*this);
379
}
380
inline const char* cdtBisimilar__option_t::getName() const
381
{
382
  return "cdt-bisimilar";
383
}
384
1549
inline dtBinarySplit__option_t::type dtBinarySplit__option_t::operator()() const
385
{
386
1549
  return (*Options::current())[*this];
387
}
388
inline bool dtBinarySplit__option_t::wasSetByUser() const
389
{
390
  return Options::current()->wasSetByUser(*this);
391
}
392
inline const char* dtBinarySplit__option_t::getName() const
393
{
394
  return "dt-binary-split";
395
}
396
1549
inline dtBlastSplits__option_t::type dtBlastSplits__option_t::operator()() const
397
{
398
1549
  return (*Options::current())[*this];
399
}
400
inline bool dtBlastSplits__option_t::wasSetByUser() const
401
{
402
  return Options::current()->wasSetByUser(*this);
403
}
404
inline const char* dtBlastSplits__option_t::getName() const
405
{
406
  return "dt-blast-splits";
407
}
408
225561
inline dtCyclic__option_t::type dtCyclic__option_t::operator()() const
409
{
410
225561
  return (*Options::current())[*this];
411
}
412
inline bool dtCyclic__option_t::wasSetByUser() const
413
{
414
  return Options::current()->wasSetByUser(*this);
415
}
416
inline const char* dtCyclic__option_t::getName() const
417
{
418
  return "dt-cyclic";
419
}
420
26978
inline dtForceAssignment__option_t::type dtForceAssignment__option_t::operator()() const
421
{
422
26978
  return (*Options::current())[*this];
423
}
424
inline bool dtForceAssignment__option_t::wasSetByUser() const
425
{
426
  return Options::current()->wasSetByUser(*this);
427
}
428
inline void dtForceAssignment__option_t::set(const dtForceAssignment__option_t::type& v)
429
{
430
  Options::current()->set(*this, v);
431
}
432
inline const char* dtForceAssignment__option_t::getName() const
433
{
434
  return "dt-force-assignment";
435
}
436
411653
inline dtInferAsLemmas__option_t::type dtInferAsLemmas__option_t::operator()() const
437
{
438
411653
  return (*Options::current())[*this];
439
}
440
inline bool dtInferAsLemmas__option_t::wasSetByUser() const
441
{
442
  return Options::current()->wasSetByUser(*this);
443
}
444
inline const char* dtInferAsLemmas__option_t::getName() const
445
{
446
  return "dt-infer-as-lemmas";
447
}
448
47442
inline dtNestedRec__option_t::type dtNestedRec__option_t::operator()() const
449
{
450
47442
  return (*Options::current())[*this];
451
}
452
inline bool dtNestedRec__option_t::wasSetByUser() const
453
{
454
  return Options::current()->wasSetByUser(*this);
455
}
456
inline const char* dtNestedRec__option_t::getName() const
457
{
458
  return "dt-nested-rec";
459
}
460
148165
inline dtPoliteOptimize__option_t::type dtPoliteOptimize__option_t::operator()() const
461
{
462
148165
  return (*Options::current())[*this];
463
}
464
inline bool dtPoliteOptimize__option_t::wasSetByUser() const
465
{
466
  return Options::current()->wasSetByUser(*this);
467
}
468
inline const char* dtPoliteOptimize__option_t::getName() const
469
{
470
  return "dt-polite-optimize";
471
}
472
3140
inline dtRewriteErrorSel__option_t::type dtRewriteErrorSel__option_t::operator()() const
473
{
474
3140
  return (*Options::current())[*this];
475
}
476
1319
inline bool dtRewriteErrorSel__option_t::wasSetByUser() const
477
{
478
1319
  return Options::current()->wasSetByUser(*this);
479
}
480
1319
inline void dtRewriteErrorSel__option_t::set(const dtRewriteErrorSel__option_t::type& v)
481
{
482
1319
  Options::current()->set(*this, v);
483
1319
}
484
inline const char* dtRewriteErrorSel__option_t::getName() const
485
{
486
  return "dt-rewrite-error-sel";
487
}
488
943868
inline dtSharedSelectors__option_t::type dtSharedSelectors__option_t::operator()() const
489
{
490
943868
  return (*Options::current())[*this];
491
}
492
inline bool dtSharedSelectors__option_t::wasSetByUser() const
493
{
494
  return Options::current()->wasSetByUser(*this);
495
}
496
inline const char* dtSharedSelectors__option_t::getName() const
497
{
498
  return "dt-share-sel";
499
}
500
1001
inline sygusAbortSize__option_t::type sygusAbortSize__option_t::operator()() const
501
{
502
1001
  return (*Options::current())[*this];
503
}
504
inline bool sygusAbortSize__option_t::wasSetByUser() const
505
{
506
  return Options::current()->wasSetByUser(*this);
507
}
508
inline const char* sygusAbortSize__option_t::getName() const
509
{
510
  return "sygus-abort-size";
511
}
512
626
inline sygusFairMax__option_t::type sygusFairMax__option_t::operator()() const
513
{
514
626
  return (*Options::current())[*this];
515
}
516
inline bool sygusFairMax__option_t::wasSetByUser() const
517
{
518
  return Options::current()->wasSetByUser(*this);
519
}
520
inline const char* sygusFairMax__option_t::getName() const
521
{
522
  return "sygus-fair-max";
523
}
524
146134
inline sygusFair__option_t::type sygusFair__option_t::operator()() const
525
{
526
146134
  return (*Options::current())[*this];
527
}
528
inline bool sygusFair__option_t::wasSetByUser() const
529
{
530
  return Options::current()->wasSetByUser(*this);
531
}
532
inline const char* sygusFair__option_t::getName() const
533
{
534
  return "sygus-fair";
535
}
536
4794
inline sygusSymBreak__option_t::type sygusSymBreak__option_t::operator()() const
537
{
538
4794
  return (*Options::current())[*this];
539
}
540
inline bool sygusSymBreak__option_t::wasSetByUser() const
541
{
542
  return Options::current()->wasSetByUser(*this);
543
}
544
inline const char* sygusSymBreak__option_t::getName() const
545
{
546
  return "sygus-sym-break";
547
}
548
301
inline sygusSymBreakAgg__option_t::type sygusSymBreakAgg__option_t::operator()() const
549
{
550
301
  return (*Options::current())[*this];
551
}
552
inline bool sygusSymBreakAgg__option_t::wasSetByUser() const
553
{
554
  return Options::current()->wasSetByUser(*this);
555
}
556
inline const char* sygusSymBreakAgg__option_t::getName() const
557
{
558
  return "sygus-sym-break-agg";
559
}
560
81536
inline sygusSymBreakDynamic__option_t::type sygusSymBreakDynamic__option_t::operator()() const
561
{
562
81536
  return (*Options::current())[*this];
563
}
564
inline bool sygusSymBreakDynamic__option_t::wasSetByUser() const
565
{
566
  return Options::current()->wasSetByUser(*this);
567
}
568
inline const char* sygusSymBreakDynamic__option_t::getName() const
569
{
570
  return "sygus-sym-break-dynamic";
571
}
572
475840
inline sygusSymBreakLazy__option_t::type sygusSymBreakLazy__option_t::operator()() const
573
{
574
475840
  return (*Options::current())[*this];
575
}
576
inline bool sygusSymBreakLazy__option_t::wasSetByUser() const
577
{
578
  return Options::current()->wasSetByUser(*this);
579
}
580
inline const char* sygusSymBreakLazy__option_t::getName() const
581
{
582
  return "sygus-sym-break-lazy";
583
}
584
8027
inline sygusSymBreakPbe__option_t::type sygusSymBreakPbe__option_t::operator()() const
585
{
586
8027
  return (*Options::current())[*this];
587
}
588
inline bool sygusSymBreakPbe__option_t::wasSetByUser() const
589
{
590
  return Options::current()->wasSetByUser(*this);
591
}
592
inline void sygusSymBreakPbe__option_t::set(const sygusSymBreakPbe__option_t::type& v)
593
{
594
  Options::current()->set(*this, v);
595
}
596
inline const char* sygusSymBreakPbe__option_t::getName() const
597
{
598
  return "sygus-sym-break-pbe";
599
}
600
123130
inline sygusSymBreakRlv__option_t::type sygusSymBreakRlv__option_t::operator()() const
601
{
602
123130
  return (*Options::current())[*this];
603
}
604
inline bool sygusSymBreakRlv__option_t::wasSetByUser() const
605
{
606
  return Options::current()->wasSetByUser(*this);
607
}
608
inline const char* sygusSymBreakRlv__option_t::getName() const
609
{
610
  return "sygus-sym-break-rlv";
611
}
612
613
}  // namespace options
614
}  // namespace CVC4
615
616
#endif /* CVC4__OPTIONS__DATATYPES_H */