48 #ifndef __CVC4__OPTIONS__QUANTIFIERS_H
49 #define __CVC4__OPTIONS__QUANTIFIERS_H
53 #line 70 "../../../src/options/../theory/quantifiers/options"
54 #include "theory/quantifiers/modes.h"
55 #line 76 "../../../src/options/../theory/quantifiers/options"
56 #include "theory/quantifiers/modes.h"
57 #line 131 "../../../src/options/../theory/quantifiers/options"
58 #include "theory/quantifiers/modes.h"
60 #line 26 "../../../src/options/base_options_template.h"
62 #define CVC4_OPTIONS__QUANTIFIERS__FOR_OPTION_HOLDER \
63 miniscopeQuant__option_t::type miniscopeQuant; \
64 bool miniscopeQuant__setByUser__; \
65 miniscopeQuantFreeVar__option_t::type miniscopeQuantFreeVar; \
66 bool miniscopeQuantFreeVar__setByUser__; \
67 prenexQuant__option_t::type prenexQuant; \
68 bool prenexQuant__setByUser__; \
69 varElimQuant__option_t::type varElimQuant; \
70 bool varElimQuant__setByUser__; \
71 simpleIteLiftQuant__option_t::type simpleIteLiftQuant; \
72 bool simpleIteLiftQuant__setByUser__; \
73 cnfQuant__option_t::type cnfQuant; \
74 bool cnfQuant__setByUser__; \
75 clauseSplit__option_t::type clauseSplit; \
76 bool clauseSplit__setByUser__; \
77 preSkolemQuant__option_t::type preSkolemQuant; \
78 bool preSkolemQuant__setByUser__; \
79 iteRemoveQuant__option_t::type iteRemoveQuant; \
80 bool iteRemoveQuant__setByUser__; \
81 aggressiveMiniscopeQuant__option_t::type aggressiveMiniscopeQuant; \
82 bool aggressiveMiniscopeQuant__setByUser__; \
83 macrosQuant__option_t::type macrosQuant; \
84 bool macrosQuant__setByUser__; \
85 foPropQuant__option_t::type foPropQuant; \
86 bool foPropQuant__setByUser__; \
87 smartTriggers__option_t::type smartTriggers; \
88 bool smartTriggers__setByUser__; \
89 relevantTriggers__option_t::type relevantTriggers; \
90 bool relevantTriggers__setByUser__; \
91 relationalTriggers__option_t::type relationalTriggers; \
92 bool relationalTriggers__setByUser__; \
93 registerQuantBodyTerms__option_t::type registerQuantBodyTerms; \
94 bool registerQuantBodyTerms__setByUser__; \
95 instWhenMode__option_t::type instWhenMode; \
96 bool instWhenMode__setByUser__; \
97 eagerInstQuant__option_t::type eagerInstQuant; \
98 bool eagerInstQuant__setByUser__; \
99 literalMatchMode__option_t::type literalMatchMode; \
100 bool literalMatchMode__setByUser__; \
101 cbqi__option_t::type cbqi; \
102 bool cbqi__setByUser__; \
103 recurseCbqi__option_t::type recurseCbqi; \
104 bool recurseCbqi__setByUser__; \
105 userPatternsQuant__option_t::type userPatternsQuant; \
106 bool userPatternsQuant__setByUser__; \
107 flipDecision__option_t::type flipDecision; \
108 bool flipDecision__setByUser__; \
109 internalReps__option_t::type internalReps; \
110 bool internalReps__setByUser__; \
111 finiteModelFind__option_t::type finiteModelFind; \
112 bool finiteModelFind__setByUser__; \
113 fmfModelBasedInst__option_t::type fmfModelBasedInst; \
114 bool fmfModelBasedInst__setByUser__; \
115 fmfFullModelCheck__option_t::type fmfFullModelCheck; \
116 bool fmfFullModelCheck__setByUser__; \
117 fmfFmcSimple__option_t::type fmfFmcSimple; \
118 bool fmfFmcSimple__setByUser__; \
119 fmfFmcCoverSimplify__option_t::type fmfFmcCoverSimplify; \
120 bool fmfFmcCoverSimplify__setByUser__; \
121 fmfFmcInterval__option_t::type fmfFmcInterval; \
122 bool fmfFmcInterval__setByUser__; \
123 fmfOneInstPerRound__option_t::type fmfOneInstPerRound; \
124 bool fmfOneInstPerRound__setByUser__; \
125 fmfOneQuantPerRound__option_t::type fmfOneQuantPerRound; \
126 bool fmfOneQuantPerRound__setByUser__; \
127 fmfInstEngine__option_t::type fmfInstEngine; \
128 bool fmfInstEngine__setByUser__; \
129 fmfRelevantDomain__option_t::type fmfRelevantDomain; \
130 bool fmfRelevantDomain__setByUser__; \
131 fmfNewInstGen__option_t::type fmfNewInstGen; \
132 bool fmfNewInstGen__setByUser__; \
133 fmfInstGen__option_t::type fmfInstGen; \
134 bool fmfInstGen__setByUser__; \
135 fmfInstGenOneQuantPerRound__option_t::type fmfInstGenOneQuantPerRound; \
136 bool fmfInstGenOneQuantPerRound__setByUser__; \
137 fmfFreshDistConst__option_t::type fmfFreshDistConst; \
138 bool fmfFreshDistConst__setByUser__; \
139 fmfBoundInt__option_t::type fmfBoundInt; \
140 bool fmfBoundInt__setByUser__; \
141 axiomInstMode__option_t::type axiomInstMode; \
142 bool axiomInstMode__setByUser__;
144 #line 30 "../../../src/options/base_options_template.h"
151 #line 11 "../../../src/options/../theory/quantifiers/options"
153 #line 17 "../../../src/options/../theory/quantifiers/options"
155 #line 21 "../../../src/options/../theory/quantifiers/options"
157 #line 27 "../../../src/options/../theory/quantifiers/options"
159 #line 30 "../../../src/options/../theory/quantifiers/options"
161 #line 34 "../../../src/options/../theory/quantifiers/options"
163 #line 37 "../../../src/options/../theory/quantifiers/options"
165 #line 43 "../../../src/options/../theory/quantifiers/options"
167 #line 45 "../../../src/options/../theory/quantifiers/options"
169 #line 48 "../../../src/options/../theory/quantifiers/options"
171 #line 51 "../../../src/options/../theory/quantifiers/options"
173 #line 54 "../../../src/options/../theory/quantifiers/options"
175 #line 58 "../../../src/options/../theory/quantifiers/options"
177 #line 61 "../../../src/options/../theory/quantifiers/options"
179 #line 63 "../../../src/options/../theory/quantifiers/options"
181 #line 67 "../../../src/options/../theory/quantifiers/options"
183 #line 70 "../../../src/options/../theory/quantifiers/options"
185 #line 73 "../../../src/options/../theory/quantifiers/options"
187 #line 76 "../../../src/options/../theory/quantifiers/options"
189 #line 79 "../../../src/options/../theory/quantifiers/options"
191 #line 83 "../../../src/options/../theory/quantifiers/options"
193 #line 86 "../../../src/options/../theory/quantifiers/options"
195 #line 89 "../../../src/options/../theory/quantifiers/options"
197 #line 92 "../../../src/options/../theory/quantifiers/options"
199 #line 95 "../../../src/options/../theory/quantifiers/options"
201 #line 98 "../../../src/options/../theory/quantifiers/options"
203 #line 101 "../../../src/options/../theory/quantifiers/options"
205 #line 103 "../../../src/options/../theory/quantifiers/options"
207 #line 105 "../../../src/options/../theory/quantifiers/options"
209 #line 107 "../../../src/options/../theory/quantifiers/options"
211 #line 110 "../../../src/options/../theory/quantifiers/options"
213 #line 112 "../../../src/options/../theory/quantifiers/options"
215 #line 114 "../../../src/options/../theory/quantifiers/options"
217 #line 116 "../../../src/options/../theory/quantifiers/options"
219 #line 118 "../../../src/options/../theory/quantifiers/options"
221 #line 120 "../../../src/options/../theory/quantifiers/options"
223 #line 123 "../../../src/options/../theory/quantifiers/options"
225 #line 125 "../../../src/options/../theory/quantifiers/options"
227 #line 128 "../../../src/options/../theory/quantifiers/options"
229 #line 131 "../../../src/options/../theory/quantifiers/options"
232 #line 38 "../../../src/options/base_options_template.h"
237 #line 11 "../../../src/options/../theory/quantifiers/options"
239 #line 11 "../../../src/options/../theory/quantifiers/options"
241 #line 11 "../../../src/options/../theory/quantifiers/options"
243 #line 17 "../../../src/options/../theory/quantifiers/options"
245 #line 17 "../../../src/options/../theory/quantifiers/options"
247 #line 17 "../../../src/options/../theory/quantifiers/options"
249 #line 21 "../../../src/options/../theory/quantifiers/options"
251 #line 21 "../../../src/options/../theory/quantifiers/options"
253 #line 21 "../../../src/options/../theory/quantifiers/options"
255 #line 27 "../../../src/options/../theory/quantifiers/options"
257 #line 27 "../../../src/options/../theory/quantifiers/options"
259 #line 27 "../../../src/options/../theory/quantifiers/options"
261 #line 30 "../../../src/options/../theory/quantifiers/options"
263 #line 30 "../../../src/options/../theory/quantifiers/options"
265 #line 30 "../../../src/options/../theory/quantifiers/options"
267 #line 34 "../../../src/options/../theory/quantifiers/options"
269 #line 34 "../../../src/options/../theory/quantifiers/options"
271 #line 34 "../../../src/options/../theory/quantifiers/options"
273 #line 37 "../../../src/options/../theory/quantifiers/options"
275 #line 37 "../../../src/options/../theory/quantifiers/options"
277 #line 37 "../../../src/options/../theory/quantifiers/options"
279 #line 43 "../../../src/options/../theory/quantifiers/options"
281 #line 43 "../../../src/options/../theory/quantifiers/options"
283 #line 43 "../../../src/options/../theory/quantifiers/options"
285 #line 45 "../../../src/options/../theory/quantifiers/options"
287 #line 45 "../../../src/options/../theory/quantifiers/options"
289 #line 45 "../../../src/options/../theory/quantifiers/options"
291 #line 48 "../../../src/options/../theory/quantifiers/options"
293 #line 48 "../../../src/options/../theory/quantifiers/options"
295 #line 48 "../../../src/options/../theory/quantifiers/options"
297 #line 51 "../../../src/options/../theory/quantifiers/options"
299 #line 51 "../../../src/options/../theory/quantifiers/options"
301 #line 51 "../../../src/options/../theory/quantifiers/options"
303 #line 54 "../../../src/options/../theory/quantifiers/options"
305 #line 54 "../../../src/options/../theory/quantifiers/options"
307 #line 54 "../../../src/options/../theory/quantifiers/options"
309 #line 58 "../../../src/options/../theory/quantifiers/options"
311 #line 58 "../../../src/options/../theory/quantifiers/options"
313 #line 58 "../../../src/options/../theory/quantifiers/options"
315 #line 61 "../../../src/options/../theory/quantifiers/options"
317 #line 61 "../../../src/options/../theory/quantifiers/options"
319 #line 61 "../../../src/options/../theory/quantifiers/options"
321 #line 63 "../../../src/options/../theory/quantifiers/options"
323 #line 63 "../../../src/options/../theory/quantifiers/options"
325 #line 63 "../../../src/options/../theory/quantifiers/options"
327 #line 67 "../../../src/options/../theory/quantifiers/options"
329 #line 67 "../../../src/options/../theory/quantifiers/options"
331 #line 67 "../../../src/options/../theory/quantifiers/options"
333 #line 70 "../../../src/options/../theory/quantifiers/options"
335 #line 70 "../../../src/options/../theory/quantifiers/options"
337 #line 70 "../../../src/options/../theory/quantifiers/options"
339 #line 70 "../../../src/options/../theory/quantifiers/options"
341 #line 73 "../../../src/options/../theory/quantifiers/options"
343 #line 73 "../../../src/options/../theory/quantifiers/options"
345 #line 73 "../../../src/options/../theory/quantifiers/options"
347 #line 76 "../../../src/options/../theory/quantifiers/options"
349 #line 76 "../../../src/options/../theory/quantifiers/options"
351 #line 76 "../../../src/options/../theory/quantifiers/options"
353 #line 79 "../../../src/options/../theory/quantifiers/options"
355 #line 79 "../../../src/options/../theory/quantifiers/options"
357 #line 79 "../../../src/options/../theory/quantifiers/options"
359 #line 83 "../../../src/options/../theory/quantifiers/options"
361 #line 83 "../../../src/options/../theory/quantifiers/options"
363 #line 83 "../../../src/options/../theory/quantifiers/options"
365 #line 86 "../../../src/options/../theory/quantifiers/options"
367 #line 86 "../../../src/options/../theory/quantifiers/options"
369 #line 86 "../../../src/options/../theory/quantifiers/options"
371 #line 89 "../../../src/options/../theory/quantifiers/options"
373 #line 89 "../../../src/options/../theory/quantifiers/options"
375 #line 89 "../../../src/options/../theory/quantifiers/options"
377 #line 92 "../../../src/options/../theory/quantifiers/options"
379 #line 92 "../../../src/options/../theory/quantifiers/options"
381 #line 92 "../../../src/options/../theory/quantifiers/options"
383 #line 95 "../../../src/options/../theory/quantifiers/options"
385 #line 95 "../../../src/options/../theory/quantifiers/options"
387 #line 95 "../../../src/options/../theory/quantifiers/options"
389 #line 98 "../../../src/options/../theory/quantifiers/options"
391 #line 98 "../../../src/options/../theory/quantifiers/options"
393 #line 98 "../../../src/options/../theory/quantifiers/options"
395 #line 101 "../../../src/options/../theory/quantifiers/options"
397 #line 101 "../../../src/options/../theory/quantifiers/options"
399 #line 101 "../../../src/options/../theory/quantifiers/options"
401 #line 101 "../../../src/options/../theory/quantifiers/options"
403 #line 103 "../../../src/options/../theory/quantifiers/options"
405 #line 103 "../../../src/options/../theory/quantifiers/options"
407 #line 103 "../../../src/options/../theory/quantifiers/options"
409 #line 105 "../../../src/options/../theory/quantifiers/options"
411 #line 105 "../../../src/options/../theory/quantifiers/options"
413 #line 105 "../../../src/options/../theory/quantifiers/options"
415 #line 107 "../../../src/options/../theory/quantifiers/options"
417 #line 107 "../../../src/options/../theory/quantifiers/options"
419 #line 107 "../../../src/options/../theory/quantifiers/options"
421 #line 110 "../../../src/options/../theory/quantifiers/options"
423 #line 110 "../../../src/options/../theory/quantifiers/options"
425 #line 110 "../../../src/options/../theory/quantifiers/options"
427 #line 112 "../../../src/options/../theory/quantifiers/options"
429 #line 112 "../../../src/options/../theory/quantifiers/options"
431 #line 112 "../../../src/options/../theory/quantifiers/options"
433 #line 114 "../../../src/options/../theory/quantifiers/options"
435 #line 114 "../../../src/options/../theory/quantifiers/options"
437 #line 114 "../../../src/options/../theory/quantifiers/options"
439 #line 116 "../../../src/options/../theory/quantifiers/options"
441 #line 116 "../../../src/options/../theory/quantifiers/options"
443 #line 116 "../../../src/options/../theory/quantifiers/options"
445 #line 118 "../../../src/options/../theory/quantifiers/options"
447 #line 118 "../../../src/options/../theory/quantifiers/options"
449 #line 118 "../../../src/options/../theory/quantifiers/options"
451 #line 120 "../../../src/options/../theory/quantifiers/options"
453 #line 120 "../../../src/options/../theory/quantifiers/options"
455 #line 120 "../../../src/options/../theory/quantifiers/options"
457 #line 120 "../../../src/options/../theory/quantifiers/options"
459 #line 123 "../../../src/options/../theory/quantifiers/options"
461 #line 123 "../../../src/options/../theory/quantifiers/options"
463 #line 123 "../../../src/options/../theory/quantifiers/options"
465 #line 125 "../../../src/options/../theory/quantifiers/options"
467 #line 125 "../../../src/options/../theory/quantifiers/options"
469 #line 125 "../../../src/options/../theory/quantifiers/options"
471 #line 128 "../../../src/options/../theory/quantifiers/options"
473 #line 128 "../../../src/options/../theory/quantifiers/options"
475 #line 128 "../../../src/options/../theory/quantifiers/options"
477 #line 131 "../../../src/options/../theory/quantifiers/options"
479 #line 131 "../../../src/options/../theory/quantifiers/options"
481 #line 131 "../../../src/options/../theory/quantifiers/options"
484 #line 44 "../../../src/options/base_options_template.h"
489 #line 11 "../../../src/options/../theory/quantifiers/options"
491 #line 11 "../../../src/options/../theory/quantifiers/options"
494 #line 17 "../../../src/options/../theory/quantifiers/options"
496 #line 17 "../../../src/options/../theory/quantifiers/options"
499 #line 21 "../../../src/options/../theory/quantifiers/options"
501 #line 21 "../../../src/options/../theory/quantifiers/options"
504 #line 27 "../../../src/options/../theory/quantifiers/options"
506 #line 27 "../../../src/options/../theory/quantifiers/options"
509 #line 30 "../../../src/options/../theory/quantifiers/options"
511 #line 30 "../../../src/options/../theory/quantifiers/options"
514 #line 34 "../../../src/options/../theory/quantifiers/options"
516 #line 34 "../../../src/options/../theory/quantifiers/options"
519 #line 37 "../../../src/options/../theory/quantifiers/options"
521 #line 37 "../../../src/options/../theory/quantifiers/options"
524 #line 43 "../../../src/options/../theory/quantifiers/options"
526 #line 43 "../../../src/options/../theory/quantifiers/options"
529 #line 45 "../../../src/options/../theory/quantifiers/options"
531 #line 45 "../../../src/options/../theory/quantifiers/options"
534 #line 48 "../../../src/options/../theory/quantifiers/options"
536 #line 48 "../../../src/options/../theory/quantifiers/options"
539 #line 51 "../../../src/options/../theory/quantifiers/options"
541 #line 51 "../../../src/options/../theory/quantifiers/options"
544 #line 54 "../../../src/options/../theory/quantifiers/options"
546 #line 54 "../../../src/options/../theory/quantifiers/options"
549 #line 58 "../../../src/options/../theory/quantifiers/options"
551 #line 58 "../../../src/options/../theory/quantifiers/options"
554 #line 61 "../../../src/options/../theory/quantifiers/options"
556 #line 61 "../../../src/options/../theory/quantifiers/options"
559 #line 63 "../../../src/options/../theory/quantifiers/options"
561 #line 63 "../../../src/options/../theory/quantifiers/options"
564 #line 67 "../../../src/options/../theory/quantifiers/options"
566 #line 67 "../../../src/options/../theory/quantifiers/options"
569 #line 70 "../../../src/options/../theory/quantifiers/options"
571 #line 70 "../../../src/options/../theory/quantifiers/options"
573 #line 70 "../../../src/options/../theory/quantifiers/options"
576 #line 73 "../../../src/options/../theory/quantifiers/options"
578 #line 73 "../../../src/options/../theory/quantifiers/options"
581 #line 76 "../../../src/options/../theory/quantifiers/options"
583 #line 76 "../../../src/options/../theory/quantifiers/options"
586 #line 79 "../../../src/options/../theory/quantifiers/options"
588 #line 79 "../../../src/options/../theory/quantifiers/options"
591 #line 83 "../../../src/options/../theory/quantifiers/options"
593 #line 83 "../../../src/options/../theory/quantifiers/options"
596 #line 86 "../../../src/options/../theory/quantifiers/options"
598 #line 86 "../../../src/options/../theory/quantifiers/options"
601 #line 89 "../../../src/options/../theory/quantifiers/options"
603 #line 89 "../../../src/options/../theory/quantifiers/options"
606 #line 92 "../../../src/options/../theory/quantifiers/options"
608 #line 92 "../../../src/options/../theory/quantifiers/options"
611 #line 95 "../../../src/options/../theory/quantifiers/options"
613 #line 95 "../../../src/options/../theory/quantifiers/options"
616 #line 98 "../../../src/options/../theory/quantifiers/options"
618 #line 98 "../../../src/options/../theory/quantifiers/options"
621 #line 101 "../../../src/options/../theory/quantifiers/options"
623 #line 101 "../../../src/options/../theory/quantifiers/options"
625 #line 101 "../../../src/options/../theory/quantifiers/options"
628 #line 103 "../../../src/options/../theory/quantifiers/options"
630 #line 103 "../../../src/options/../theory/quantifiers/options"
633 #line 105 "../../../src/options/../theory/quantifiers/options"
635 #line 105 "../../../src/options/../theory/quantifiers/options"
638 #line 107 "../../../src/options/../theory/quantifiers/options"
640 #line 107 "../../../src/options/../theory/quantifiers/options"
643 #line 110 "../../../src/options/../theory/quantifiers/options"
645 #line 110 "../../../src/options/../theory/quantifiers/options"
648 #line 112 "../../../src/options/../theory/quantifiers/options"
650 #line 112 "../../../src/options/../theory/quantifiers/options"
653 #line 114 "../../../src/options/../theory/quantifiers/options"
655 #line 114 "../../../src/options/../theory/quantifiers/options"
658 #line 116 "../../../src/options/../theory/quantifiers/options"
660 #line 116 "../../../src/options/../theory/quantifiers/options"
663 #line 118 "../../../src/options/../theory/quantifiers/options"
665 #line 118 "../../../src/options/../theory/quantifiers/options"
668 #line 120 "../../../src/options/../theory/quantifiers/options"
670 #line 120 "../../../src/options/../theory/quantifiers/options"
672 #line 120 "../../../src/options/../theory/quantifiers/options"
675 #line 123 "../../../src/options/../theory/quantifiers/options"
677 #line 123 "../../../src/options/../theory/quantifiers/options"
680 #line 125 "../../../src/options/../theory/quantifiers/options"
682 #line 125 "../../../src/options/../theory/quantifiers/options"
685 #line 128 "../../../src/options/../theory/quantifiers/options"
687 #line 128 "../../../src/options/../theory/quantifiers/options"
690 #line 131 "../../../src/options/../theory/quantifiers/options"
692 #line 131 "../../../src/options/../theory/quantifiers/options"
695 #line 50 "../../../src/options/base_options_template.h"
bool wasSetByUser() const
bool wasSetByUser() const
struct CVC4::options::foPropQuant__option_t foPropQuant
struct CVC4::options::fmfOneInstPerRound__option_t fmfOneInstPerRound
bool wasSetByUser() const
struct CVC4::options::fmfFmcCoverSimplify__option_t fmfFmcCoverSimplify
struct CVC4::options::finiteModelFind__option_t finiteModelFind
bool wasSetByUser() const
bool wasSetByUser() const
struct CVC4::options::fmfBoundInt__option_t fmfBoundInt
struct CVC4::options::userPatternsQuant__option_t userPatternsQuant
CVC4::theory::quantifiers::AxiomInstMode type
struct CVC4::options::fmfInstGen__option_t fmfInstGen
struct CVC4::options::cnfQuant__option_t cnfQuant
bool wasSetByUser() const
struct CVC4::options::cbqi__option_t cbqi
struct CVC4::options::clauseSplit__option_t clauseSplit
struct CVC4::options::internalReps__option_t internalReps
bool wasSetByUser() const
struct CVC4::options::macrosQuant__option_t macrosQuant
bool wasSetByUser() const
bool wasSetByUser() const
const T::type & operator[](T) const
Get the value of the given option.
struct CVC4::options::miniscopeQuantFreeVar__option_t miniscopeQuantFreeVar
bool wasSetByUser() const
bool wasSetByUser() const
struct CVC4::options::iteRemoveQuant__option_t iteRemoveQuant
bool wasSetByUser() const
bool wasSetByUser(T) const
Returns true iff the value of the given option was set by the user via a command-line option or SmtEn...
struct CVC4::options::simpleIteLiftQuant__option_t simpleIteLiftQuant
CVC4::theory::quantifiers::InstWhenMode type
bool wasSetByUser() const
bool wasSetByUser() const
struct CVC4::options::prenexQuant__option_t prenexQuant
bool wasSetByUser() const
struct CVC4::options::aggressiveMiniscopeQuant__option_t aggressiveMiniscopeQuant
struct CVC4::options::instWhenMode__option_t instWhenMode
bool wasSetByUser() const
bool wasSetByUser() const
bool wasSetByUser() const
bool wasSetByUser() const
struct CVC4::options::smartTriggers__option_t smartTriggers
This is CVC4 release version For build and installation please see the INSTALL file included with this distribution This first official release of CVC4 is the result of more than three years of efforts by researchers at New York University and The University of Iowa The project leaders are Clark please refer to the AUTHORS file in the source distribution CVC4 is a tool for determining the satisfiability of a first order formula modulo a first order CVC CVC3 but does not directly incorporate code from any previous version CVC4 is intended to be an open and extensible SMT engine It can be used as a stand alone tool or as a library It has been designed to increase the performance and reduce the memory overhead of its predecessors It is written entirely in C and is released under a free software see the INSTALL file that comes with this distribution We recommend that you visit our CVC4 tutorials online please write to the cvc users cs nyu edu mailing list *if you need to report a bug with CVC4
struct CVC4::options::axiomInstMode__option_t axiomInstMode
bool wasSetByUser() const
bool wasSetByUser() const
bool wasSetByUser() const
struct CVC4::options::fmfFullModelCheck__option_t fmfFullModelCheck
struct CVC4::options::fmfInstEngine__option_t fmfInstEngine
struct CVC4::options::fmfFmcSimple__option_t fmfFmcSimple
struct CVC4::options::preSkolemQuant__option_t preSkolemQuant
struct CVC4::options::registerQuantBodyTerms__option_t registerQuantBodyTerms
bool wasSetByUser() const
bool wasSetByUser() const
struct CVC4::options::relevantTriggers__option_t relevantTriggers
struct CVC4::options::fmfFmcInterval__option_t fmfFmcInterval
struct CVC4::options::fmfModelBasedInst__option_t fmfModelBasedInst
struct CVC4::options::varElimQuant__option_t varElimQuant
Global (command-line, set-option, ...) parameters for SMT.
bool wasSetByUser() const
struct CVC4::options::fmfRelevantDomain__option_t fmfRelevantDomain
static Options & current()
Get the current Options in effect.
Macros that should be defined everywhere during the building of the libraries and driver binary...
struct CVC4::options::fmfOneQuantPerRound__option_t fmfOneQuantPerRound
bool wasSetByUser() const
bool wasSetByUser() const
struct CVC4::options::miniscopeQuant__option_t miniscopeQuant
struct CVC4::options::fmfFreshDistConst__option_t fmfFreshDistConst
CVC4::theory::quantifiers::LiteralMatchMode type
bool wasSetByUser() const
bool wasSetByUser() const
bool wasSetByUser() const
struct CVC4::options::recurseCbqi__option_t recurseCbqi
struct CVC4::options::eagerInstQuant__option_t eagerInstQuant
struct CVC4::options::literalMatchMode__option_t literalMatchMode
void set(T, const typename T::type &)
Set the value of the given option.
bool wasSetByUser() const
struct CVC4::options::fmfNewInstGen__option_t fmfNewInstGen
bool wasSetByUser() const
struct CVC4::options::relationalTriggers__option_t relationalTriggers
bool wasSetByUser() const
bool wasSetByUser() const
bool wasSetByUser() const
bool wasSetByUser() const
bool wasSetByUser() const
bool wasSetByUser() const
struct CVC4::options::flipDecision__option_t flipDecision
bool wasSetByUser() const
struct CVC4::options::fmfInstGenOneQuantPerRound__option_t fmfInstGenOneQuantPerRound
bool wasSetByUser() const