cvc4-1.3
options.h
Go to the documentation of this file.
1 /********************* */
14 /* THIS FILE IS AUTOMATICALLY GENERATED, DO NOT EDIT ! */
15 /* THIS FILE IS AUTOMATICALLY GENERATED, DO NOT EDIT ! */
16 /* THIS FILE IS AUTOMATICALLY GENERATED, DO NOT EDIT ! */
17 /* THIS FILE IS AUTOMATICALLY GENERATED, DO NOT EDIT ! */
18 /* THIS FILE IS AUTOMATICALLY GENERATED, DO NOT EDIT ! */
19 /* THIS FILE IS AUTOMATICALLY GENERATED, DO NOT EDIT ! */
20 
21 /* THIS FILE IS AUTOMATICALLY GENERATED, DO NOT EDIT ! */
22 /* THIS FILE IS AUTOMATICALLY GENERATED, DO NOT EDIT ! */
23 /* THIS FILE IS AUTOMATICALLY GENERATED, DO NOT EDIT ! */
24 /* THIS FILE IS AUTOMATICALLY GENERATED, DO NOT EDIT ! */
25 /* THIS FILE IS AUTOMATICALLY GENERATED, DO NOT EDIT ! */
26 /* THIS FILE IS AUTOMATICALLY GENERATED, DO NOT EDIT ! */
27 
28 /* Edit the template file instead. */
29 
30 /********************* */
46 #include "cvc4_public.h"
47 
48 #ifndef __CVC4__OPTIONS__QUANTIFIERS_H
49 #define __CVC4__OPTIONS__QUANTIFIERS_H
50 
51 #include "options/options.h"
52 
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"
59 
60 #line 26 "../../../src/options/base_options_template.h"
61 
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__;
143 
144 #line 30 "../../../src/options/base_options_template.h"
145 
146 namespace CVC4 {
147 
148 namespace options {
149 
150 
151 #line 11 "../../../src/options/../theory/quantifiers/options"
152 extern struct CVC4_PUBLIC miniscopeQuant__option_t { typedef bool type; type operator()() const; bool wasSetByUser() const; } miniscopeQuant CVC4_PUBLIC;
153 #line 17 "../../../src/options/../theory/quantifiers/options"
154 extern struct CVC4_PUBLIC miniscopeQuantFreeVar__option_t { typedef bool type; type operator()() const; bool wasSetByUser() const; } miniscopeQuantFreeVar CVC4_PUBLIC;
155 #line 21 "../../../src/options/../theory/quantifiers/options"
156 extern struct CVC4_PUBLIC prenexQuant__option_t { typedef bool type; type operator()() const; bool wasSetByUser() const; } prenexQuant CVC4_PUBLIC;
157 #line 27 "../../../src/options/../theory/quantifiers/options"
158 extern struct CVC4_PUBLIC varElimQuant__option_t { typedef bool type; type operator()() const; bool wasSetByUser() const; } varElimQuant CVC4_PUBLIC;
159 #line 30 "../../../src/options/../theory/quantifiers/options"
160 extern struct CVC4_PUBLIC simpleIteLiftQuant__option_t { typedef bool type; type operator()() const; bool wasSetByUser() const; } simpleIteLiftQuant CVC4_PUBLIC;
161 #line 34 "../../../src/options/../theory/quantifiers/options"
162 extern struct CVC4_PUBLIC cnfQuant__option_t { typedef bool type; type operator()() const; bool wasSetByUser() const; } cnfQuant CVC4_PUBLIC;
163 #line 37 "../../../src/options/../theory/quantifiers/options"
164 extern struct CVC4_PUBLIC clauseSplit__option_t { typedef bool type; type operator()() const; bool wasSetByUser() const; } clauseSplit CVC4_PUBLIC;
165 #line 43 "../../../src/options/../theory/quantifiers/options"
166 extern struct CVC4_PUBLIC preSkolemQuant__option_t { typedef bool type; type operator()() const; bool wasSetByUser() const; } preSkolemQuant CVC4_PUBLIC;
167 #line 45 "../../../src/options/../theory/quantifiers/options"
168 extern struct CVC4_PUBLIC iteRemoveQuant__option_t { typedef bool type; type operator()() const; bool wasSetByUser() const; } iteRemoveQuant CVC4_PUBLIC;
169 #line 48 "../../../src/options/../theory/quantifiers/options"
170 extern struct CVC4_PUBLIC aggressiveMiniscopeQuant__option_t { typedef bool type; type operator()() const; bool wasSetByUser() const; } aggressiveMiniscopeQuant CVC4_PUBLIC;
171 #line 51 "../../../src/options/../theory/quantifiers/options"
172 extern struct CVC4_PUBLIC macrosQuant__option_t { typedef bool type; type operator()() const; bool wasSetByUser() const; } macrosQuant CVC4_PUBLIC;
173 #line 54 "../../../src/options/../theory/quantifiers/options"
174 extern struct CVC4_PUBLIC foPropQuant__option_t { typedef bool type; type operator()() const; bool wasSetByUser() const; } foPropQuant CVC4_PUBLIC;
175 #line 58 "../../../src/options/../theory/quantifiers/options"
176 extern struct CVC4_PUBLIC smartTriggers__option_t { typedef bool type; type operator()() const; bool wasSetByUser() const; } smartTriggers CVC4_PUBLIC;
177 #line 61 "../../../src/options/../theory/quantifiers/options"
178 extern struct CVC4_PUBLIC relevantTriggers__option_t { typedef bool type; type operator()() const; bool wasSetByUser() const; } relevantTriggers CVC4_PUBLIC;
179 #line 63 "../../../src/options/../theory/quantifiers/options"
180 extern struct CVC4_PUBLIC relationalTriggers__option_t { typedef bool type; type operator()() const; bool wasSetByUser() const; } relationalTriggers CVC4_PUBLIC;
181 #line 67 "../../../src/options/../theory/quantifiers/options"
182 extern struct CVC4_PUBLIC registerQuantBodyTerms__option_t { typedef bool type; type operator()() const; bool wasSetByUser() const; } registerQuantBodyTerms CVC4_PUBLIC;
183 #line 70 "../../../src/options/../theory/quantifiers/options"
184 extern struct CVC4_PUBLIC instWhenMode__option_t { typedef CVC4::theory::quantifiers::InstWhenMode type; type operator()() const; bool wasSetByUser() const; void set(const type& v); } instWhenMode CVC4_PUBLIC;
185 #line 73 "../../../src/options/../theory/quantifiers/options"
186 extern struct CVC4_PUBLIC eagerInstQuant__option_t { typedef bool type; type operator()() const; bool wasSetByUser() const; } eagerInstQuant CVC4_PUBLIC;
187 #line 76 "../../../src/options/../theory/quantifiers/options"
188 extern struct CVC4_PUBLIC literalMatchMode__option_t { typedef CVC4::theory::quantifiers::LiteralMatchMode type; type operator()() const; bool wasSetByUser() const; } literalMatchMode CVC4_PUBLIC;
189 #line 79 "../../../src/options/../theory/quantifiers/options"
190 extern struct CVC4_PUBLIC cbqi__option_t { typedef bool type; type operator()() const; bool wasSetByUser() const; } cbqi CVC4_PUBLIC;
191 #line 83 "../../../src/options/../theory/quantifiers/options"
192 extern struct CVC4_PUBLIC recurseCbqi__option_t { typedef bool type; type operator()() const; bool wasSetByUser() const; } recurseCbqi CVC4_PUBLIC;
193 #line 86 "../../../src/options/../theory/quantifiers/options"
194 extern struct CVC4_PUBLIC userPatternsQuant__option_t { typedef bool type; type operator()() const; bool wasSetByUser() const; } userPatternsQuant CVC4_PUBLIC;
195 #line 89 "../../../src/options/../theory/quantifiers/options"
196 extern struct CVC4_PUBLIC flipDecision__option_t { typedef bool type; type operator()() const; bool wasSetByUser() const; } flipDecision CVC4_PUBLIC;
197 #line 92 "../../../src/options/../theory/quantifiers/options"
198 extern struct CVC4_PUBLIC internalReps__option_t { typedef bool type; type operator()() const; bool wasSetByUser() const; } internalReps CVC4_PUBLIC;
199 #line 95 "../../../src/options/../theory/quantifiers/options"
200 extern struct CVC4_PUBLIC finiteModelFind__option_t { typedef bool type; type operator()() const; bool wasSetByUser() const; } finiteModelFind CVC4_PUBLIC;
201 #line 98 "../../../src/options/../theory/quantifiers/options"
202 extern struct CVC4_PUBLIC fmfModelBasedInst__option_t { typedef bool type; type operator()() const; bool wasSetByUser() const; } fmfModelBasedInst CVC4_PUBLIC;
203 #line 101 "../../../src/options/../theory/quantifiers/options"
204 extern struct CVC4_PUBLIC fmfFullModelCheck__option_t { typedef bool type; type operator()() const; bool wasSetByUser() const; void set(const type& v); } fmfFullModelCheck CVC4_PUBLIC;
205 #line 103 "../../../src/options/../theory/quantifiers/options"
206 extern struct CVC4_PUBLIC fmfFmcSimple__option_t { typedef bool type; type operator()() const; bool wasSetByUser() const; } fmfFmcSimple CVC4_PUBLIC;
207 #line 105 "../../../src/options/../theory/quantifiers/options"
208 extern struct CVC4_PUBLIC fmfFmcCoverSimplify__option_t { typedef bool type; type operator()() const; bool wasSetByUser() const; } fmfFmcCoverSimplify CVC4_PUBLIC;
209 #line 107 "../../../src/options/../theory/quantifiers/options"
210 extern struct CVC4_PUBLIC fmfFmcInterval__option_t { typedef bool type; type operator()() const; bool wasSetByUser() const; } fmfFmcInterval CVC4_PUBLIC;
211 #line 110 "../../../src/options/../theory/quantifiers/options"
212 extern struct CVC4_PUBLIC fmfOneInstPerRound__option_t { typedef bool type; type operator()() const; bool wasSetByUser() const; } fmfOneInstPerRound CVC4_PUBLIC;
213 #line 112 "../../../src/options/../theory/quantifiers/options"
214 extern struct CVC4_PUBLIC fmfOneQuantPerRound__option_t { typedef bool type; type operator()() const; bool wasSetByUser() const; } fmfOneQuantPerRound CVC4_PUBLIC;
215 #line 114 "../../../src/options/../theory/quantifiers/options"
216 extern struct CVC4_PUBLIC fmfInstEngine__option_t { typedef bool type; type operator()() const; bool wasSetByUser() const; } fmfInstEngine CVC4_PUBLIC;
217 #line 116 "../../../src/options/../theory/quantifiers/options"
218 extern struct CVC4_PUBLIC fmfRelevantDomain__option_t { typedef bool type; type operator()() const; bool wasSetByUser() const; } fmfRelevantDomain CVC4_PUBLIC;
219 #line 118 "../../../src/options/../theory/quantifiers/options"
220 extern struct CVC4_PUBLIC fmfNewInstGen__option_t { typedef bool type; type operator()() const; bool wasSetByUser() const; } fmfNewInstGen CVC4_PUBLIC;
221 #line 120 "../../../src/options/../theory/quantifiers/options"
222 extern struct CVC4_PUBLIC fmfInstGen__option_t { typedef bool type; type operator()() const; bool wasSetByUser() const; void set(const type& v); } fmfInstGen CVC4_PUBLIC;
223 #line 123 "../../../src/options/../theory/quantifiers/options"
224 extern struct CVC4_PUBLIC fmfInstGenOneQuantPerRound__option_t { typedef bool type; type operator()() const; bool wasSetByUser() const; } fmfInstGenOneQuantPerRound CVC4_PUBLIC;
225 #line 125 "../../../src/options/../theory/quantifiers/options"
226 extern struct CVC4_PUBLIC fmfFreshDistConst__option_t { typedef bool type; type operator()() const; bool wasSetByUser() const; } fmfFreshDistConst CVC4_PUBLIC;
227 #line 128 "../../../src/options/../theory/quantifiers/options"
228 extern struct CVC4_PUBLIC fmfBoundInt__option_t { typedef bool type; type operator()() const; bool wasSetByUser() const; } fmfBoundInt CVC4_PUBLIC;
229 #line 131 "../../../src/options/../theory/quantifiers/options"
230 extern struct CVC4_PUBLIC axiomInstMode__option_t { typedef CVC4::theory::quantifiers::AxiomInstMode type; type operator()() const; bool wasSetByUser() const; } axiomInstMode CVC4_PUBLIC;
231 
232 #line 38 "../../../src/options/base_options_template.h"
233 
234 }/* CVC4::options namespace */
235 
236 
237 #line 11 "../../../src/options/../theory/quantifiers/options"
239 #line 11 "../../../src/options/../theory/quantifiers/options"
241 #line 11 "../../../src/options/../theory/quantifiers/options"
242 template <> void Options::assignBool(options::miniscopeQuant__option_t, std::string option, bool value, SmtEngine* smt);
243 #line 17 "../../../src/options/../theory/quantifiers/options"
245 #line 17 "../../../src/options/../theory/quantifiers/options"
247 #line 17 "../../../src/options/../theory/quantifiers/options"
248 template <> void Options::assignBool(options::miniscopeQuantFreeVar__option_t, std::string option, bool value, SmtEngine* smt);
249 #line 21 "../../../src/options/../theory/quantifiers/options"
251 #line 21 "../../../src/options/../theory/quantifiers/options"
253 #line 21 "../../../src/options/../theory/quantifiers/options"
254 template <> void Options::assignBool(options::prenexQuant__option_t, std::string option, bool value, SmtEngine* smt);
255 #line 27 "../../../src/options/../theory/quantifiers/options"
257 #line 27 "../../../src/options/../theory/quantifiers/options"
259 #line 27 "../../../src/options/../theory/quantifiers/options"
260 template <> void Options::assignBool(options::varElimQuant__option_t, std::string option, bool value, SmtEngine* smt);
261 #line 30 "../../../src/options/../theory/quantifiers/options"
263 #line 30 "../../../src/options/../theory/quantifiers/options"
265 #line 30 "../../../src/options/../theory/quantifiers/options"
266 template <> void Options::assignBool(options::simpleIteLiftQuant__option_t, std::string option, bool value, SmtEngine* smt);
267 #line 34 "../../../src/options/../theory/quantifiers/options"
269 #line 34 "../../../src/options/../theory/quantifiers/options"
270 template <> bool Options::wasSetByUser(options::cnfQuant__option_t) const;
271 #line 34 "../../../src/options/../theory/quantifiers/options"
272 template <> void Options::assignBool(options::cnfQuant__option_t, std::string option, bool value, SmtEngine* smt);
273 #line 37 "../../../src/options/../theory/quantifiers/options"
275 #line 37 "../../../src/options/../theory/quantifiers/options"
277 #line 37 "../../../src/options/../theory/quantifiers/options"
278 template <> void Options::assignBool(options::clauseSplit__option_t, std::string option, bool value, SmtEngine* smt);
279 #line 43 "../../../src/options/../theory/quantifiers/options"
281 #line 43 "../../../src/options/../theory/quantifiers/options"
283 #line 43 "../../../src/options/../theory/quantifiers/options"
284 template <> void Options::assignBool(options::preSkolemQuant__option_t, std::string option, bool value, SmtEngine* smt);
285 #line 45 "../../../src/options/../theory/quantifiers/options"
287 #line 45 "../../../src/options/../theory/quantifiers/options"
289 #line 45 "../../../src/options/../theory/quantifiers/options"
290 template <> void Options::assignBool(options::iteRemoveQuant__option_t, std::string option, bool value, SmtEngine* smt);
291 #line 48 "../../../src/options/../theory/quantifiers/options"
293 #line 48 "../../../src/options/../theory/quantifiers/options"
295 #line 48 "../../../src/options/../theory/quantifiers/options"
296 template <> void Options::assignBool(options::aggressiveMiniscopeQuant__option_t, std::string option, bool value, SmtEngine* smt);
297 #line 51 "../../../src/options/../theory/quantifiers/options"
299 #line 51 "../../../src/options/../theory/quantifiers/options"
301 #line 51 "../../../src/options/../theory/quantifiers/options"
302 template <> void Options::assignBool(options::macrosQuant__option_t, std::string option, bool value, SmtEngine* smt);
303 #line 54 "../../../src/options/../theory/quantifiers/options"
305 #line 54 "../../../src/options/../theory/quantifiers/options"
307 #line 54 "../../../src/options/../theory/quantifiers/options"
308 template <> void Options::assignBool(options::foPropQuant__option_t, std::string option, bool value, SmtEngine* smt);
309 #line 58 "../../../src/options/../theory/quantifiers/options"
311 #line 58 "../../../src/options/../theory/quantifiers/options"
313 #line 58 "../../../src/options/../theory/quantifiers/options"
314 template <> void Options::assignBool(options::smartTriggers__option_t, std::string option, bool value, SmtEngine* smt);
315 #line 61 "../../../src/options/../theory/quantifiers/options"
317 #line 61 "../../../src/options/../theory/quantifiers/options"
319 #line 61 "../../../src/options/../theory/quantifiers/options"
320 template <> void Options::assignBool(options::relevantTriggers__option_t, std::string option, bool value, SmtEngine* smt);
321 #line 63 "../../../src/options/../theory/quantifiers/options"
323 #line 63 "../../../src/options/../theory/quantifiers/options"
325 #line 63 "../../../src/options/../theory/quantifiers/options"
326 template <> void Options::assignBool(options::relationalTriggers__option_t, std::string option, bool value, SmtEngine* smt);
327 #line 67 "../../../src/options/../theory/quantifiers/options"
329 #line 67 "../../../src/options/../theory/quantifiers/options"
331 #line 67 "../../../src/options/../theory/quantifiers/options"
332 template <> void Options::assignBool(options::registerQuantBodyTerms__option_t, std::string option, bool value, SmtEngine* smt);
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"
340 template <> void Options::assign(options::instWhenMode__option_t, std::string option, std::string value, SmtEngine* smt);
341 #line 73 "../../../src/options/../theory/quantifiers/options"
343 #line 73 "../../../src/options/../theory/quantifiers/options"
345 #line 73 "../../../src/options/../theory/quantifiers/options"
346 template <> void Options::assignBool(options::eagerInstQuant__option_t, std::string option, bool value, SmtEngine* smt);
347 #line 76 "../../../src/options/../theory/quantifiers/options"
349 #line 76 "../../../src/options/../theory/quantifiers/options"
351 #line 76 "../../../src/options/../theory/quantifiers/options"
352 template <> void Options::assign(options::literalMatchMode__option_t, std::string option, std::string value, SmtEngine* smt);
353 #line 79 "../../../src/options/../theory/quantifiers/options"
355 #line 79 "../../../src/options/../theory/quantifiers/options"
356 template <> bool Options::wasSetByUser(options::cbqi__option_t) const;
357 #line 79 "../../../src/options/../theory/quantifiers/options"
358 template <> void Options::assignBool(options::cbqi__option_t, std::string option, bool value, SmtEngine* smt);
359 #line 83 "../../../src/options/../theory/quantifiers/options"
361 #line 83 "../../../src/options/../theory/quantifiers/options"
363 #line 83 "../../../src/options/../theory/quantifiers/options"
364 template <> void Options::assignBool(options::recurseCbqi__option_t, std::string option, bool value, SmtEngine* smt);
365 #line 86 "../../../src/options/../theory/quantifiers/options"
367 #line 86 "../../../src/options/../theory/quantifiers/options"
369 #line 86 "../../../src/options/../theory/quantifiers/options"
370 template <> void Options::assignBool(options::userPatternsQuant__option_t, std::string option, bool value, SmtEngine* smt);
371 #line 89 "../../../src/options/../theory/quantifiers/options"
373 #line 89 "../../../src/options/../theory/quantifiers/options"
375 #line 89 "../../../src/options/../theory/quantifiers/options"
376 template <> void Options::assignBool(options::flipDecision__option_t, std::string option, bool value, SmtEngine* smt);
377 #line 92 "../../../src/options/../theory/quantifiers/options"
379 #line 92 "../../../src/options/../theory/quantifiers/options"
381 #line 92 "../../../src/options/../theory/quantifiers/options"
382 template <> void Options::assignBool(options::internalReps__option_t, std::string option, bool value, SmtEngine* smt);
383 #line 95 "../../../src/options/../theory/quantifiers/options"
385 #line 95 "../../../src/options/../theory/quantifiers/options"
387 #line 95 "../../../src/options/../theory/quantifiers/options"
388 template <> void Options::assignBool(options::finiteModelFind__option_t, std::string option, bool value, SmtEngine* smt);
389 #line 98 "../../../src/options/../theory/quantifiers/options"
391 #line 98 "../../../src/options/../theory/quantifiers/options"
393 #line 98 "../../../src/options/../theory/quantifiers/options"
394 template <> void Options::assignBool(options::fmfModelBasedInst__option_t, std::string option, bool value, SmtEngine* smt);
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"
402 template <> void Options::assignBool(options::fmfFullModelCheck__option_t, std::string option, bool value, SmtEngine* smt);
403 #line 103 "../../../src/options/../theory/quantifiers/options"
405 #line 103 "../../../src/options/../theory/quantifiers/options"
407 #line 103 "../../../src/options/../theory/quantifiers/options"
408 template <> void Options::assignBool(options::fmfFmcSimple__option_t, std::string option, bool value, SmtEngine* smt);
409 #line 105 "../../../src/options/../theory/quantifiers/options"
411 #line 105 "../../../src/options/../theory/quantifiers/options"
413 #line 105 "../../../src/options/../theory/quantifiers/options"
414 template <> void Options::assignBool(options::fmfFmcCoverSimplify__option_t, std::string option, bool value, SmtEngine* smt);
415 #line 107 "../../../src/options/../theory/quantifiers/options"
417 #line 107 "../../../src/options/../theory/quantifiers/options"
419 #line 107 "../../../src/options/../theory/quantifiers/options"
420 template <> void Options::assignBool(options::fmfFmcInterval__option_t, std::string option, bool value, SmtEngine* smt);
421 #line 110 "../../../src/options/../theory/quantifiers/options"
423 #line 110 "../../../src/options/../theory/quantifiers/options"
425 #line 110 "../../../src/options/../theory/quantifiers/options"
426 template <> void Options::assignBool(options::fmfOneInstPerRound__option_t, std::string option, bool value, SmtEngine* smt);
427 #line 112 "../../../src/options/../theory/quantifiers/options"
429 #line 112 "../../../src/options/../theory/quantifiers/options"
431 #line 112 "../../../src/options/../theory/quantifiers/options"
432 template <> void Options::assignBool(options::fmfOneQuantPerRound__option_t, std::string option, bool value, SmtEngine* smt);
433 #line 114 "../../../src/options/../theory/quantifiers/options"
435 #line 114 "../../../src/options/../theory/quantifiers/options"
437 #line 114 "../../../src/options/../theory/quantifiers/options"
438 template <> void Options::assignBool(options::fmfInstEngine__option_t, std::string option, bool value, SmtEngine* smt);
439 #line 116 "../../../src/options/../theory/quantifiers/options"
441 #line 116 "../../../src/options/../theory/quantifiers/options"
443 #line 116 "../../../src/options/../theory/quantifiers/options"
444 template <> void Options::assignBool(options::fmfRelevantDomain__option_t, std::string option, bool value, SmtEngine* smt);
445 #line 118 "../../../src/options/../theory/quantifiers/options"
447 #line 118 "../../../src/options/../theory/quantifiers/options"
449 #line 118 "../../../src/options/../theory/quantifiers/options"
450 template <> void Options::assignBool(options::fmfNewInstGen__option_t, std::string option, bool value, SmtEngine* smt);
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"
458 template <> void Options::assignBool(options::fmfInstGen__option_t, std::string option, bool value, SmtEngine* smt);
459 #line 123 "../../../src/options/../theory/quantifiers/options"
461 #line 123 "../../../src/options/../theory/quantifiers/options"
463 #line 123 "../../../src/options/../theory/quantifiers/options"
464 template <> void Options::assignBool(options::fmfInstGenOneQuantPerRound__option_t, std::string option, bool value, SmtEngine* smt);
465 #line 125 "../../../src/options/../theory/quantifiers/options"
467 #line 125 "../../../src/options/../theory/quantifiers/options"
469 #line 125 "../../../src/options/../theory/quantifiers/options"
470 template <> void Options::assignBool(options::fmfFreshDistConst__option_t, std::string option, bool value, SmtEngine* smt);
471 #line 128 "../../../src/options/../theory/quantifiers/options"
473 #line 128 "../../../src/options/../theory/quantifiers/options"
475 #line 128 "../../../src/options/../theory/quantifiers/options"
476 template <> void Options::assignBool(options::fmfBoundInt__option_t, std::string option, bool value, SmtEngine* smt);
477 #line 131 "../../../src/options/../theory/quantifiers/options"
479 #line 131 "../../../src/options/../theory/quantifiers/options"
481 #line 131 "../../../src/options/../theory/quantifiers/options"
482 template <> void Options::assign(options::axiomInstMode__option_t, std::string option, std::string value, SmtEngine* smt);
483 
484 #line 44 "../../../src/options/base_options_template.h"
485 
486 namespace options {
487 
488 
489 #line 11 "../../../src/options/../theory/quantifiers/options"
491 #line 11 "../../../src/options/../theory/quantifiers/options"
493 
494 #line 17 "../../../src/options/../theory/quantifiers/options"
496 #line 17 "../../../src/options/../theory/quantifiers/options"
498 
499 #line 21 "../../../src/options/../theory/quantifiers/options"
501 #line 21 "../../../src/options/../theory/quantifiers/options"
502 inline bool prenexQuant__option_t::wasSetByUser() const { return Options::current().wasSetByUser(*this); }
503 
504 #line 27 "../../../src/options/../theory/quantifiers/options"
506 #line 27 "../../../src/options/../theory/quantifiers/options"
508 
509 #line 30 "../../../src/options/../theory/quantifiers/options"
511 #line 30 "../../../src/options/../theory/quantifiers/options"
513 
514 #line 34 "../../../src/options/../theory/quantifiers/options"
516 #line 34 "../../../src/options/../theory/quantifiers/options"
517 inline bool cnfQuant__option_t::wasSetByUser() const { return Options::current().wasSetByUser(*this); }
518 
519 #line 37 "../../../src/options/../theory/quantifiers/options"
521 #line 37 "../../../src/options/../theory/quantifiers/options"
522 inline bool clauseSplit__option_t::wasSetByUser() const { return Options::current().wasSetByUser(*this); }
523 
524 #line 43 "../../../src/options/../theory/quantifiers/options"
526 #line 43 "../../../src/options/../theory/quantifiers/options"
528 
529 #line 45 "../../../src/options/../theory/quantifiers/options"
531 #line 45 "../../../src/options/../theory/quantifiers/options"
533 
534 #line 48 "../../../src/options/../theory/quantifiers/options"
536 #line 48 "../../../src/options/../theory/quantifiers/options"
538 
539 #line 51 "../../../src/options/../theory/quantifiers/options"
541 #line 51 "../../../src/options/../theory/quantifiers/options"
542 inline bool macrosQuant__option_t::wasSetByUser() const { return Options::current().wasSetByUser(*this); }
543 
544 #line 54 "../../../src/options/../theory/quantifiers/options"
546 #line 54 "../../../src/options/../theory/quantifiers/options"
547 inline bool foPropQuant__option_t::wasSetByUser() const { return Options::current().wasSetByUser(*this); }
548 
549 #line 58 "../../../src/options/../theory/quantifiers/options"
551 #line 58 "../../../src/options/../theory/quantifiers/options"
553 
554 #line 61 "../../../src/options/../theory/quantifiers/options"
556 #line 61 "../../../src/options/../theory/quantifiers/options"
558 
559 #line 63 "../../../src/options/../theory/quantifiers/options"
561 #line 63 "../../../src/options/../theory/quantifiers/options"
563 
564 #line 67 "../../../src/options/../theory/quantifiers/options"
566 #line 67 "../../../src/options/../theory/quantifiers/options"
568 
569 #line 70 "../../../src/options/../theory/quantifiers/options"
571 #line 70 "../../../src/options/../theory/quantifiers/options"
573 #line 70 "../../../src/options/../theory/quantifiers/options"
575 
576 #line 73 "../../../src/options/../theory/quantifiers/options"
578 #line 73 "../../../src/options/../theory/quantifiers/options"
580 
581 #line 76 "../../../src/options/../theory/quantifiers/options"
583 #line 76 "../../../src/options/../theory/quantifiers/options"
585 
586 #line 79 "../../../src/options/../theory/quantifiers/options"
588 #line 79 "../../../src/options/../theory/quantifiers/options"
589 inline bool cbqi__option_t::wasSetByUser() const { return Options::current().wasSetByUser(*this); }
590 
591 #line 83 "../../../src/options/../theory/quantifiers/options"
593 #line 83 "../../../src/options/../theory/quantifiers/options"
594 inline bool recurseCbqi__option_t::wasSetByUser() const { return Options::current().wasSetByUser(*this); }
595 
596 #line 86 "../../../src/options/../theory/quantifiers/options"
598 #line 86 "../../../src/options/../theory/quantifiers/options"
600 
601 #line 89 "../../../src/options/../theory/quantifiers/options"
603 #line 89 "../../../src/options/../theory/quantifiers/options"
605 
606 #line 92 "../../../src/options/../theory/quantifiers/options"
608 #line 92 "../../../src/options/../theory/quantifiers/options"
610 
611 #line 95 "../../../src/options/../theory/quantifiers/options"
613 #line 95 "../../../src/options/../theory/quantifiers/options"
615 
616 #line 98 "../../../src/options/../theory/quantifiers/options"
618 #line 98 "../../../src/options/../theory/quantifiers/options"
620 
621 #line 101 "../../../src/options/../theory/quantifiers/options"
623 #line 101 "../../../src/options/../theory/quantifiers/options"
625 #line 101 "../../../src/options/../theory/quantifiers/options"
627 
628 #line 103 "../../../src/options/../theory/quantifiers/options"
630 #line 103 "../../../src/options/../theory/quantifiers/options"
632 
633 #line 105 "../../../src/options/../theory/quantifiers/options"
635 #line 105 "../../../src/options/../theory/quantifiers/options"
637 
638 #line 107 "../../../src/options/../theory/quantifiers/options"
640 #line 107 "../../../src/options/../theory/quantifiers/options"
642 
643 #line 110 "../../../src/options/../theory/quantifiers/options"
645 #line 110 "../../../src/options/../theory/quantifiers/options"
647 
648 #line 112 "../../../src/options/../theory/quantifiers/options"
650 #line 112 "../../../src/options/../theory/quantifiers/options"
652 
653 #line 114 "../../../src/options/../theory/quantifiers/options"
655 #line 114 "../../../src/options/../theory/quantifiers/options"
657 
658 #line 116 "../../../src/options/../theory/quantifiers/options"
660 #line 116 "../../../src/options/../theory/quantifiers/options"
662 
663 #line 118 "../../../src/options/../theory/quantifiers/options"
665 #line 118 "../../../src/options/../theory/quantifiers/options"
667 
668 #line 120 "../../../src/options/../theory/quantifiers/options"
670 #line 120 "../../../src/options/../theory/quantifiers/options"
671 inline bool fmfInstGen__option_t::wasSetByUser() const { return Options::current().wasSetByUser(*this); }
672 #line 120 "../../../src/options/../theory/quantifiers/options"
674 
675 #line 123 "../../../src/options/../theory/quantifiers/options"
677 #line 123 "../../../src/options/../theory/quantifiers/options"
679 
680 #line 125 "../../../src/options/../theory/quantifiers/options"
682 #line 125 "../../../src/options/../theory/quantifiers/options"
684 
685 #line 128 "../../../src/options/../theory/quantifiers/options"
687 #line 128 "../../../src/options/../theory/quantifiers/options"
688 inline bool fmfBoundInt__option_t::wasSetByUser() const { return Options::current().wasSetByUser(*this); }
689 
690 #line 131 "../../../src/options/../theory/quantifiers/options"
692 #line 131 "../../../src/options/../theory/quantifiers/options"
694 
695 #line 50 "../../../src/options/base_options_template.h"
696 
697 }/* CVC4::options namespace */
698 
699 }/* CVC4 namespace */
700 
701 #endif /* __CVC4__OPTIONS__QUANTIFIERS_H */
struct CVC4::options::foPropQuant__option_t foPropQuant
struct CVC4::options::fmfOneInstPerRound__option_t fmfOneInstPerRound
struct CVC4::options::fmfFmcCoverSimplify__option_t fmfFmcCoverSimplify
struct CVC4::options::finiteModelFind__option_t finiteModelFind
struct CVC4::options::fmfBoundInt__option_t fmfBoundInt
struct CVC4::options::userPatternsQuant__option_t userPatternsQuant
CVC4::theory::quantifiers::AxiomInstMode type
Definition: options.h:230
struct CVC4::options::fmfInstGen__option_t fmfInstGen
struct CVC4::options::cnfQuant__option_t cnfQuant
struct CVC4::options::cbqi__option_t cbqi
struct CVC4::options::clauseSplit__option_t clauseSplit
struct CVC4::options::internalReps__option_t internalReps
struct CVC4::options::macrosQuant__option_t macrosQuant
const T::type & operator[](T) const
Get the value of the given option.
struct CVC4::options::miniscopeQuantFreeVar__option_t miniscopeQuantFreeVar
struct CVC4::options::iteRemoveQuant__option_t iteRemoveQuant
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
Definition: options.h:184
struct CVC4::options::prenexQuant__option_t prenexQuant
struct CVC4::options::aggressiveMiniscopeQuant__option_t aggressiveMiniscopeQuant
struct CVC4::options::instWhenMode__option_t instWhenMode
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
Definition: README:39
struct CVC4::options::axiomInstMode__option_t axiomInstMode
type operator()() const
Definition: options.h:587
#define CVC4_PUBLIC
Definition: cvc4_public.h:30
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
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.
struct CVC4::options::fmfRelevantDomain__option_t fmfRelevantDomain
static Options & current()
Get the current Options in effect.
Definition: options.h:64
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
Definition: options.h:589
struct CVC4::options::miniscopeQuant__option_t miniscopeQuant
struct CVC4::options::fmfFreshDistConst__option_t fmfFreshDistConst
CVC4::theory::quantifiers::LiteralMatchMode type
Definition: options.h:188
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.
Definition: options.h:78
struct CVC4::options::fmfNewInstGen__option_t fmfNewInstGen
struct CVC4::options::relationalTriggers__option_t relationalTriggers
struct CVC4::options::flipDecision__option_t flipDecision
struct CVC4::options::fmfInstGenOneQuantPerRound__option_t fmfInstGenOneQuantPerRound