cvc4-1.4
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 71 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/quantifiers/options"
54 #include "theory/quantifiers/modes.h"
55 #line 82 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/quantifiers/options"
56 #include "theory/quantifiers/modes.h"
57 #line 91 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/quantifiers/options"
58 #include "theory/quantifiers/modes.h"
59 #line 103 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/quantifiers/options"
60 #include "theory/quantifiers/modes.h"
61 #line 125 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/quantifiers/options"
62 #include "theory/quantifiers/modes.h"
63 #line 130 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/quantifiers/options"
64 #include "theory/quantifiers/modes.h"
65 #line 132 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/quantifiers/options"
66 #include "theory/quantifiers/modes.h"
67 
68 #line 26 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/base_options_template.h"
69 
70 #define CVC4_OPTIONS__QUANTIFIERS__FOR_OPTION_HOLDER \
71  miniscopeQuant__option_t::type miniscopeQuant; \
72  bool miniscopeQuant__setByUser__; \
73  miniscopeQuantFreeVar__option_t::type miniscopeQuantFreeVar; \
74  bool miniscopeQuantFreeVar__setByUser__; \
75  prenexQuant__option_t::type prenexQuant; \
76  bool prenexQuant__setByUser__; \
77  varElimQuant__option_t::type varElimQuant; \
78  bool varElimQuant__setByUser__; \
79  simpleIteLiftQuant__option_t::type simpleIteLiftQuant; \
80  bool simpleIteLiftQuant__setByUser__; \
81  cnfQuant__option_t::type cnfQuant; \
82  bool cnfQuant__setByUser__; \
83  nnfQuant__option_t::type nnfQuant; \
84  bool nnfQuant__setByUser__; \
85  clauseSplit__option_t::type clauseSplit; \
86  bool clauseSplit__setByUser__; \
87  preSkolemQuant__option_t::type preSkolemQuant; \
88  bool preSkolemQuant__setByUser__; \
89  aggressiveMiniscopeQuant__option_t::type aggressiveMiniscopeQuant; \
90  bool aggressiveMiniscopeQuant__setByUser__; \
91  macrosQuant__option_t::type macrosQuant; \
92  bool macrosQuant__setByUser__; \
93  foPropQuant__option_t::type foPropQuant; \
94  bool foPropQuant__setByUser__; \
95  smartTriggers__option_t::type smartTriggers; \
96  bool smartTriggers__setByUser__; \
97  relevantTriggers__option_t::type relevantTriggers; \
98  bool relevantTriggers__setByUser__; \
99  relationalTriggers__option_t::type relationalTriggers; \
100  bool relationalTriggers__setByUser__; \
101  registerQuantBodyTerms__option_t::type registerQuantBodyTerms; \
102  bool registerQuantBodyTerms__setByUser__; \
103  instWhenMode__option_t::type instWhenMode; \
104  bool instWhenMode__setByUser__; \
105  instMaxLevel__option_t::type instMaxLevel; \
106  bool instMaxLevel__setByUser__; \
107  eagerInstQuant__option_t::type eagerInstQuant; \
108  bool eagerInstQuant__setByUser__; \
109  fullSaturateQuant__option_t::type fullSaturateQuant; \
110  bool fullSaturateQuant__setByUser__; \
111  literalMatchMode__option_t::type literalMatchMode; \
112  bool literalMatchMode__setByUser__; \
113  cbqi__option_t::type cbqi; \
114  bool cbqi__setByUser__; \
115  recurseCbqi__option_t::type recurseCbqi; \
116  bool recurseCbqi__setByUser__; \
117  userPatternsQuant__option_t::type userPatternsQuant; \
118  bool userPatternsQuant__setByUser__; \
119  flipDecision__option_t::type flipDecision; \
120  bool flipDecision__setByUser__; \
121  internalReps__option_t::type internalReps; \
122  bool internalReps__setByUser__; \
123  finiteModelFind__option_t::type finiteModelFind; \
124  bool finiteModelFind__setByUser__; \
125  mbqiMode__option_t::type mbqiMode; \
126  bool mbqiMode__setByUser__; \
127  fmfOneInstPerRound__option_t::type fmfOneInstPerRound; \
128  bool fmfOneInstPerRound__setByUser__; \
129  fmfOneQuantPerRound__option_t::type fmfOneQuantPerRound; \
130  bool fmfOneQuantPerRound__setByUser__; \
131  fmfInstEngine__option_t::type fmfInstEngine; \
132  bool fmfInstEngine__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  fmfFmcSimple__option_t::type fmfFmcSimple; \
140  bool fmfFmcSimple__setByUser__; \
141  fmfBoundInt__option_t::type fmfBoundInt; \
142  bool fmfBoundInt__setByUser__; \
143  fmfBoundIntLazy__option_t::type fmfBoundIntLazy; \
144  bool fmfBoundIntLazy__setByUser__; \
145  axiomInstMode__option_t::type axiomInstMode; \
146  bool axiomInstMode__setByUser__; \
147  quantConflictFind__option_t::type quantConflictFind; \
148  bool quantConflictFind__setByUser__; \
149  qcfMode__option_t::type qcfMode; \
150  bool qcfMode__setByUser__; \
151  qcfWhenMode__option_t::type qcfWhenMode; \
152  bool qcfWhenMode__setByUser__; \
153  qcfTConstraint__option_t::type qcfTConstraint; \
154  bool qcfTConstraint__setByUser__; \
155  quantRewriteRules__option_t::type quantRewriteRules; \
156  bool quantRewriteRules__setByUser__; \
157  rrOneInstPerRound__option_t::type rrOneInstPerRound; \
158  bool rrOneInstPerRound__setByUser__; \
159  dtStcInduction__option_t::type dtStcInduction; \
160  bool dtStcInduction__setByUser__;
161 
162 #line 30 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/base_options_template.h"
163 
164 namespace CVC4 {
165 
166 namespace options {
167 
168 
169 #line 11 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/quantifiers/options"
170 extern struct CVC4_PUBLIC miniscopeQuant__option_t { typedef bool type; type operator()() const; bool wasSetByUser() const; } miniscopeQuant CVC4_PUBLIC;
171 #line 17 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/quantifiers/options"
172 extern struct CVC4_PUBLIC miniscopeQuantFreeVar__option_t { typedef bool type; type operator()() const; bool wasSetByUser() const; } miniscopeQuantFreeVar CVC4_PUBLIC;
173 #line 21 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/quantifiers/options"
174 extern struct CVC4_PUBLIC prenexQuant__option_t { typedef bool type; type operator()() const; bool wasSetByUser() const; } prenexQuant CVC4_PUBLIC;
175 #line 27 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/quantifiers/options"
176 extern struct CVC4_PUBLIC varElimQuant__option_t { typedef bool type; type operator()() const; bool wasSetByUser() const; } varElimQuant CVC4_PUBLIC;
177 #line 30 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/quantifiers/options"
178 extern struct CVC4_PUBLIC simpleIteLiftQuant__option_t { typedef bool type; type operator()() const; bool wasSetByUser() const; } simpleIteLiftQuant CVC4_PUBLIC;
179 #line 34 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/quantifiers/options"
180 extern struct CVC4_PUBLIC cnfQuant__option_t { typedef bool type; type operator()() const; bool wasSetByUser() const; } cnfQuant CVC4_PUBLIC;
181 #line 37 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/quantifiers/options"
182 extern struct CVC4_PUBLIC nnfQuant__option_t { typedef bool type; type operator()() const; bool wasSetByUser() const; } nnfQuant CVC4_PUBLIC;
183 #line 40 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/quantifiers/options"
184 extern struct CVC4_PUBLIC clauseSplit__option_t { typedef bool type; type operator()() const; bool wasSetByUser() const; } clauseSplit CVC4_PUBLIC;
185 #line 46 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/quantifiers/options"
186 extern struct CVC4_PUBLIC preSkolemQuant__option_t { typedef bool type; type operator()() const; bool wasSetByUser() const; void set(const type& v); } preSkolemQuant CVC4_PUBLIC;
187 #line 49 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/quantifiers/options"
188 extern struct CVC4_PUBLIC aggressiveMiniscopeQuant__option_t { typedef bool type; type operator()() const; bool wasSetByUser() const; } aggressiveMiniscopeQuant CVC4_PUBLIC;
189 #line 52 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/quantifiers/options"
190 extern struct CVC4_PUBLIC macrosQuant__option_t { typedef bool type; type operator()() const; bool wasSetByUser() const; } macrosQuant CVC4_PUBLIC;
191 #line 55 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/quantifiers/options"
192 extern struct CVC4_PUBLIC foPropQuant__option_t { typedef bool type; type operator()() const; bool wasSetByUser() const; } foPropQuant CVC4_PUBLIC;
193 #line 59 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/quantifiers/options"
194 extern struct CVC4_PUBLIC smartTriggers__option_t { typedef bool type; type operator()() const; bool wasSetByUser() const; } smartTriggers CVC4_PUBLIC;
195 #line 62 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/quantifiers/options"
196 extern struct CVC4_PUBLIC relevantTriggers__option_t { typedef bool type; type operator()() const; bool wasSetByUser() const; } relevantTriggers CVC4_PUBLIC;
197 #line 64 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/quantifiers/options"
198 extern struct CVC4_PUBLIC relationalTriggers__option_t { typedef bool type; type operator()() const; bool wasSetByUser() const; } relationalTriggers CVC4_PUBLIC;
199 #line 68 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/quantifiers/options"
200 extern struct CVC4_PUBLIC registerQuantBodyTerms__option_t { typedef bool type; type operator()() const; bool wasSetByUser() const; } registerQuantBodyTerms CVC4_PUBLIC;
201 #line 71 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/quantifiers/options"
202 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;
203 #line 73 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/quantifiers/options"
204 extern struct CVC4_PUBLIC instMaxLevel__option_t { typedef int type; type operator()() const; bool wasSetByUser() const; } instMaxLevel CVC4_PUBLIC;
205 #line 76 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/quantifiers/options"
206 extern struct CVC4_PUBLIC eagerInstQuant__option_t { typedef bool type; type operator()() const; bool wasSetByUser() const; } eagerInstQuant CVC4_PUBLIC;
207 #line 79 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/quantifiers/options"
208 extern struct CVC4_PUBLIC fullSaturateQuant__option_t { typedef bool type; type operator()() const; bool wasSetByUser() const; } fullSaturateQuant CVC4_PUBLIC;
209 #line 82 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/quantifiers/options"
210 extern struct CVC4_PUBLIC literalMatchMode__option_t { typedef CVC4::theory::quantifiers::LiteralMatchMode type; type operator()() const; bool wasSetByUser() const; } literalMatchMode CVC4_PUBLIC;
211 #line 85 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/quantifiers/options"
212 extern struct CVC4_PUBLIC cbqi__option_t { typedef bool type; type operator()() const; bool wasSetByUser() const; void set(const type& v); } cbqi CVC4_PUBLIC;
213 #line 88 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/quantifiers/options"
214 extern struct CVC4_PUBLIC recurseCbqi__option_t { typedef bool type; type operator()() const; bool wasSetByUser() const; } recurseCbqi CVC4_PUBLIC;
215 #line 91 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/quantifiers/options"
216 extern struct CVC4_PUBLIC userPatternsQuant__option_t { typedef CVC4::theory::quantifiers::UserPatMode type; type operator()() const; bool wasSetByUser() const; } userPatternsQuant CVC4_PUBLIC;
217 #line 94 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/quantifiers/options"
218 extern struct CVC4_PUBLIC flipDecision__option_t { typedef bool type; type operator()() const; bool wasSetByUser() const; } flipDecision CVC4_PUBLIC;
219 #line 97 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/quantifiers/options"
220 extern struct CVC4_PUBLIC internalReps__option_t { typedef bool type; type operator()() const; bool wasSetByUser() const; } internalReps CVC4_PUBLIC;
221 #line 100 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/quantifiers/options"
222 extern struct CVC4_PUBLIC finiteModelFind__option_t { typedef bool type; type operator()() const; bool wasSetByUser() const; void set(const type& v); } finiteModelFind CVC4_PUBLIC;
223 #line 103 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/quantifiers/options"
224 extern struct CVC4_PUBLIC mbqiMode__option_t { typedef CVC4::theory::quantifiers::MbqiMode type; type operator()() const; bool wasSetByUser() const; void set(const type& v); } mbqiMode CVC4_PUBLIC;
225 #line 105 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/quantifiers/options"
226 extern struct CVC4_PUBLIC fmfOneInstPerRound__option_t { typedef bool type; type operator()() const; bool wasSetByUser() const; } fmfOneInstPerRound CVC4_PUBLIC;
227 #line 107 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/quantifiers/options"
228 extern struct CVC4_PUBLIC fmfOneQuantPerRound__option_t { typedef bool type; type operator()() const; bool wasSetByUser() const; } fmfOneQuantPerRound CVC4_PUBLIC;
229 #line 110 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/quantifiers/options"
230 extern struct CVC4_PUBLIC fmfInstEngine__option_t { typedef bool type; type operator()() const; bool wasSetByUser() const; } fmfInstEngine CVC4_PUBLIC;
231 #line 112 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/quantifiers/options"
232 extern struct CVC4_PUBLIC fmfInstGen__option_t { typedef bool type; type operator()() const; bool wasSetByUser() const; } fmfInstGen CVC4_PUBLIC;
233 #line 114 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/quantifiers/options"
234 extern struct CVC4_PUBLIC fmfInstGenOneQuantPerRound__option_t { typedef bool type; type operator()() const; bool wasSetByUser() const; } fmfInstGenOneQuantPerRound CVC4_PUBLIC;
235 #line 116 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/quantifiers/options"
236 extern struct CVC4_PUBLIC fmfFreshDistConst__option_t { typedef bool type; type operator()() const; bool wasSetByUser() const; } fmfFreshDistConst CVC4_PUBLIC;
237 #line 118 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/quantifiers/options"
238 extern struct CVC4_PUBLIC fmfFmcSimple__option_t { typedef bool type; type operator()() const; bool wasSetByUser() const; } fmfFmcSimple CVC4_PUBLIC;
239 #line 120 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/quantifiers/options"
240 extern struct CVC4_PUBLIC fmfBoundInt__option_t { typedef bool type; type operator()() const; bool wasSetByUser() const; void set(const type& v); } fmfBoundInt CVC4_PUBLIC;
241 #line 122 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/quantifiers/options"
242 extern struct CVC4_PUBLIC fmfBoundIntLazy__option_t { typedef bool type; type operator()() const; bool wasSetByUser() const; void set(const type& v); } fmfBoundIntLazy CVC4_PUBLIC;
243 #line 125 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/quantifiers/options"
244 extern struct CVC4_PUBLIC axiomInstMode__option_t { typedef CVC4::theory::quantifiers::AxiomInstMode type; type operator()() const; bool wasSetByUser() const; } axiomInstMode CVC4_PUBLIC;
245 #line 128 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/quantifiers/options"
246 extern struct CVC4_PUBLIC quantConflictFind__option_t { typedef bool type; type operator()() const; bool wasSetByUser() const; void set(const type& v); } quantConflictFind CVC4_PUBLIC;
247 #line 130 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/quantifiers/options"
248 extern struct CVC4_PUBLIC qcfMode__option_t { typedef CVC4::theory::quantifiers::QcfMode type; type operator()() const; bool wasSetByUser() const; } qcfMode CVC4_PUBLIC;
249 #line 132 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/quantifiers/options"
250 extern struct CVC4_PUBLIC qcfWhenMode__option_t { typedef CVC4::theory::quantifiers::QcfWhenMode type; type operator()() const; bool wasSetByUser() const; } qcfWhenMode CVC4_PUBLIC;
251 #line 134 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/quantifiers/options"
252 extern struct CVC4_PUBLIC qcfTConstraint__option_t { typedef bool type; type operator()() const; bool wasSetByUser() const; void set(const type& v); } qcfTConstraint CVC4_PUBLIC;
253 #line 137 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/quantifiers/options"
254 extern struct CVC4_PUBLIC quantRewriteRules__option_t { typedef bool type; type operator()() const; bool wasSetByUser() const; } quantRewriteRules CVC4_PUBLIC;
255 #line 139 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/quantifiers/options"
256 extern struct CVC4_PUBLIC rrOneInstPerRound__option_t { typedef bool type; type operator()() const; bool wasSetByUser() const; } rrOneInstPerRound CVC4_PUBLIC;
257 #line 142 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/quantifiers/options"
258 extern struct CVC4_PUBLIC dtStcInduction__option_t { typedef bool type; type operator()() const; bool wasSetByUser() const; } dtStcInduction CVC4_PUBLIC;
259 
260 #line 38 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/base_options_template.h"
261 
262 }/* CVC4::options namespace */
263 
264 
265 #line 11 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/quantifiers/options"
267 #line 11 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/quantifiers/options"
269 #line 11 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/quantifiers/options"
270 template <> void Options::assignBool(options::miniscopeQuant__option_t, std::string option, bool value, SmtEngine* smt);
271 #line 17 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/quantifiers/options"
273 #line 17 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/quantifiers/options"
275 #line 17 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/quantifiers/options"
276 template <> void Options::assignBool(options::miniscopeQuantFreeVar__option_t, std::string option, bool value, SmtEngine* smt);
277 #line 21 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/quantifiers/options"
279 #line 21 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/quantifiers/options"
281 #line 21 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/quantifiers/options"
282 template <> void Options::assignBool(options::prenexQuant__option_t, std::string option, bool value, SmtEngine* smt);
283 #line 27 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/quantifiers/options"
285 #line 27 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/quantifiers/options"
287 #line 27 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/quantifiers/options"
288 template <> void Options::assignBool(options::varElimQuant__option_t, std::string option, bool value, SmtEngine* smt);
289 #line 30 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/quantifiers/options"
291 #line 30 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/quantifiers/options"
293 #line 30 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/quantifiers/options"
294 template <> void Options::assignBool(options::simpleIteLiftQuant__option_t, std::string option, bool value, SmtEngine* smt);
295 #line 34 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/quantifiers/options"
297 #line 34 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/quantifiers/options"
298 template <> bool Options::wasSetByUser(options::cnfQuant__option_t) const;
299 #line 34 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/quantifiers/options"
300 template <> void Options::assignBool(options::cnfQuant__option_t, std::string option, bool value, SmtEngine* smt);
301 #line 37 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/quantifiers/options"
303 #line 37 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/quantifiers/options"
304 template <> bool Options::wasSetByUser(options::nnfQuant__option_t) const;
305 #line 37 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/quantifiers/options"
306 template <> void Options::assignBool(options::nnfQuant__option_t, std::string option, bool value, SmtEngine* smt);
307 #line 40 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/quantifiers/options"
309 #line 40 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/quantifiers/options"
311 #line 40 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/quantifiers/options"
312 template <> void Options::assignBool(options::clauseSplit__option_t, std::string option, bool value, SmtEngine* smt);
313 #line 46 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/quantifiers/options"
315 #line 46 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/quantifiers/options"
317 #line 46 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/quantifiers/options"
319 #line 46 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/quantifiers/options"
320 template <> void Options::assignBool(options::preSkolemQuant__option_t, std::string option, bool value, SmtEngine* smt);
321 #line 49 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/quantifiers/options"
323 #line 49 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/quantifiers/options"
325 #line 49 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/quantifiers/options"
326 template <> void Options::assignBool(options::aggressiveMiniscopeQuant__option_t, std::string option, bool value, SmtEngine* smt);
327 #line 52 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/quantifiers/options"
329 #line 52 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/quantifiers/options"
331 #line 52 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/quantifiers/options"
332 template <> void Options::assignBool(options::macrosQuant__option_t, std::string option, bool value, SmtEngine* smt);
333 #line 55 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/quantifiers/options"
335 #line 55 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/quantifiers/options"
337 #line 55 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/quantifiers/options"
338 template <> void Options::assignBool(options::foPropQuant__option_t, std::string option, bool value, SmtEngine* smt);
339 #line 59 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/quantifiers/options"
341 #line 59 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/quantifiers/options"
343 #line 59 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/quantifiers/options"
344 template <> void Options::assignBool(options::smartTriggers__option_t, std::string option, bool value, SmtEngine* smt);
345 #line 62 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/quantifiers/options"
347 #line 62 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/quantifiers/options"
349 #line 62 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/quantifiers/options"
350 template <> void Options::assignBool(options::relevantTriggers__option_t, std::string option, bool value, SmtEngine* smt);
351 #line 64 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/quantifiers/options"
353 #line 64 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/quantifiers/options"
355 #line 64 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/quantifiers/options"
356 template <> void Options::assignBool(options::relationalTriggers__option_t, std::string option, bool value, SmtEngine* smt);
357 #line 68 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/quantifiers/options"
359 #line 68 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/quantifiers/options"
361 #line 68 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/quantifiers/options"
362 template <> void Options::assignBool(options::registerQuantBodyTerms__option_t, std::string option, bool value, SmtEngine* smt);
363 #line 71 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/quantifiers/options"
365 #line 71 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/quantifiers/options"
367 #line 71 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/quantifiers/options"
369 #line 71 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/quantifiers/options"
370 template <> void Options::assign(options::instWhenMode__option_t, std::string option, std::string value, SmtEngine* smt);
371 #line 73 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/quantifiers/options"
373 #line 73 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/quantifiers/options"
375 #line 73 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/quantifiers/options"
376 template <> void Options::assign(options::instMaxLevel__option_t, std::string option, std::string value, SmtEngine* smt);
377 #line 76 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/quantifiers/options"
379 #line 76 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/quantifiers/options"
381 #line 76 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/quantifiers/options"
382 template <> void Options::assignBool(options::eagerInstQuant__option_t, std::string option, bool value, SmtEngine* smt);
383 #line 79 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/quantifiers/options"
385 #line 79 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/quantifiers/options"
387 #line 79 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/quantifiers/options"
388 template <> void Options::assignBool(options::fullSaturateQuant__option_t, std::string option, bool value, SmtEngine* smt);
389 #line 82 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/quantifiers/options"
391 #line 82 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/quantifiers/options"
393 #line 82 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/quantifiers/options"
394 template <> void Options::assign(options::literalMatchMode__option_t, std::string option, std::string value, SmtEngine* smt);
395 #line 85 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/quantifiers/options"
397 #line 85 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/quantifiers/options"
399 #line 85 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/quantifiers/options"
400 template <> bool Options::wasSetByUser(options::cbqi__option_t) const;
401 #line 85 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/quantifiers/options"
402 template <> void Options::assignBool(options::cbqi__option_t, std::string option, bool value, SmtEngine* smt);
403 #line 88 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/quantifiers/options"
405 #line 88 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/quantifiers/options"
407 #line 88 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/quantifiers/options"
408 template <> void Options::assignBool(options::recurseCbqi__option_t, std::string option, bool value, SmtEngine* smt);
409 #line 91 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/quantifiers/options"
411 #line 91 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/quantifiers/options"
413 #line 91 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/quantifiers/options"
414 template <> void Options::assign(options::userPatternsQuant__option_t, std::string option, std::string value, SmtEngine* smt);
415 #line 94 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/quantifiers/options"
417 #line 94 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/quantifiers/options"
419 #line 94 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/quantifiers/options"
420 template <> void Options::assignBool(options::flipDecision__option_t, std::string option, bool value, SmtEngine* smt);
421 #line 97 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/quantifiers/options"
423 #line 97 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/quantifiers/options"
425 #line 97 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/quantifiers/options"
426 template <> void Options::assignBool(options::internalReps__option_t, std::string option, bool value, SmtEngine* smt);
427 #line 100 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/quantifiers/options"
429 #line 100 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/quantifiers/options"
431 #line 100 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/quantifiers/options"
433 #line 100 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/quantifiers/options"
434 template <> void Options::assignBool(options::finiteModelFind__option_t, std::string option, bool value, SmtEngine* smt);
435 #line 103 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/quantifiers/options"
437 #line 103 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/quantifiers/options"
439 #line 103 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/quantifiers/options"
440 template <> bool Options::wasSetByUser(options::mbqiMode__option_t) const;
441 #line 103 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/quantifiers/options"
442 template <> void Options::assign(options::mbqiMode__option_t, std::string option, std::string value, SmtEngine* smt);
443 #line 105 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/quantifiers/options"
445 #line 105 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/quantifiers/options"
447 #line 105 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/quantifiers/options"
448 template <> void Options::assignBool(options::fmfOneInstPerRound__option_t, std::string option, bool value, SmtEngine* smt);
449 #line 107 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/quantifiers/options"
451 #line 107 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/quantifiers/options"
453 #line 107 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/quantifiers/options"
454 template <> void Options::assignBool(options::fmfOneQuantPerRound__option_t, std::string option, bool value, SmtEngine* smt);
455 #line 110 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/quantifiers/options"
457 #line 110 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/quantifiers/options"
459 #line 110 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/quantifiers/options"
460 template <> void Options::assignBool(options::fmfInstEngine__option_t, std::string option, bool value, SmtEngine* smt);
461 #line 112 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/quantifiers/options"
463 #line 112 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/quantifiers/options"
465 #line 112 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/quantifiers/options"
466 template <> void Options::assignBool(options::fmfInstGen__option_t, std::string option, bool value, SmtEngine* smt);
467 #line 114 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/quantifiers/options"
469 #line 114 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/quantifiers/options"
471 #line 114 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/quantifiers/options"
472 template <> void Options::assignBool(options::fmfInstGenOneQuantPerRound__option_t, std::string option, bool value, SmtEngine* smt);
473 #line 116 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/quantifiers/options"
475 #line 116 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/quantifiers/options"
477 #line 116 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/quantifiers/options"
478 template <> void Options::assignBool(options::fmfFreshDistConst__option_t, std::string option, bool value, SmtEngine* smt);
479 #line 118 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/quantifiers/options"
481 #line 118 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/quantifiers/options"
483 #line 118 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/quantifiers/options"
484 template <> void Options::assignBool(options::fmfFmcSimple__option_t, std::string option, bool value, SmtEngine* smt);
485 #line 120 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/quantifiers/options"
487 #line 120 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/quantifiers/options"
489 #line 120 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/quantifiers/options"
491 #line 120 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/quantifiers/options"
492 template <> void Options::assignBool(options::fmfBoundInt__option_t, std::string option, bool value, SmtEngine* smt);
493 #line 122 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/quantifiers/options"
495 #line 122 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/quantifiers/options"
497 #line 122 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/quantifiers/options"
499 #line 122 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/quantifiers/options"
500 template <> void Options::assignBool(options::fmfBoundIntLazy__option_t, std::string option, bool value, SmtEngine* smt);
501 #line 125 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/quantifiers/options"
503 #line 125 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/quantifiers/options"
505 #line 125 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/quantifiers/options"
506 template <> void Options::assign(options::axiomInstMode__option_t, std::string option, std::string value, SmtEngine* smt);
507 #line 128 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/quantifiers/options"
509 #line 128 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/quantifiers/options"
511 #line 128 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/quantifiers/options"
513 #line 128 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/quantifiers/options"
514 template <> void Options::assignBool(options::quantConflictFind__option_t, std::string option, bool value, SmtEngine* smt);
515 #line 130 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/quantifiers/options"
517 #line 130 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/quantifiers/options"
518 template <> bool Options::wasSetByUser(options::qcfMode__option_t) const;
519 #line 130 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/quantifiers/options"
520 template <> void Options::assign(options::qcfMode__option_t, std::string option, std::string value, SmtEngine* smt);
521 #line 132 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/quantifiers/options"
523 #line 132 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/quantifiers/options"
525 #line 132 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/quantifiers/options"
526 template <> void Options::assign(options::qcfWhenMode__option_t, std::string option, std::string value, SmtEngine* smt);
527 #line 134 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/quantifiers/options"
529 #line 134 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/quantifiers/options"
531 #line 134 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/quantifiers/options"
533 #line 134 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/quantifiers/options"
534 template <> void Options::assignBool(options::qcfTConstraint__option_t, std::string option, bool value, SmtEngine* smt);
535 #line 137 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/quantifiers/options"
537 #line 137 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/quantifiers/options"
539 #line 137 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/quantifiers/options"
540 template <> void Options::assignBool(options::quantRewriteRules__option_t, std::string option, bool value, SmtEngine* smt);
541 #line 139 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/quantifiers/options"
543 #line 139 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/quantifiers/options"
545 #line 139 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/quantifiers/options"
546 template <> void Options::assignBool(options::rrOneInstPerRound__option_t, std::string option, bool value, SmtEngine* smt);
547 #line 142 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/quantifiers/options"
549 #line 142 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/quantifiers/options"
551 #line 142 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/quantifiers/options"
552 template <> void Options::assignBool(options::dtStcInduction__option_t, std::string option, bool value, SmtEngine* smt);
553 
554 #line 44 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/base_options_template.h"
555 
556 namespace options {
557 
558 
559 #line 11 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/quantifiers/options"
561 #line 11 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/quantifiers/options"
563 
564 #line 17 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/quantifiers/options"
566 #line 17 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/quantifiers/options"
568 
569 #line 21 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/quantifiers/options"
571 #line 21 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/quantifiers/options"
572 inline bool prenexQuant__option_t::wasSetByUser() const { return Options::current().wasSetByUser(*this); }
573 
574 #line 27 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/quantifiers/options"
576 #line 27 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/quantifiers/options"
578 
579 #line 30 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/quantifiers/options"
581 #line 30 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/quantifiers/options"
583 
584 #line 34 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/quantifiers/options"
586 #line 34 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/quantifiers/options"
587 inline bool cnfQuant__option_t::wasSetByUser() const { return Options::current().wasSetByUser(*this); }
588 
589 #line 37 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/quantifiers/options"
591 #line 37 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/quantifiers/options"
592 inline bool nnfQuant__option_t::wasSetByUser() const { return Options::current().wasSetByUser(*this); }
593 
594 #line 40 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/quantifiers/options"
596 #line 40 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/quantifiers/options"
597 inline bool clauseSplit__option_t::wasSetByUser() const { return Options::current().wasSetByUser(*this); }
598 
599 #line 46 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/quantifiers/options"
601 #line 46 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/quantifiers/options"
603 #line 46 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/quantifiers/options"
605 
606 #line 49 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/quantifiers/options"
608 #line 49 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/quantifiers/options"
610 
611 #line 52 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/quantifiers/options"
613 #line 52 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/quantifiers/options"
614 inline bool macrosQuant__option_t::wasSetByUser() const { return Options::current().wasSetByUser(*this); }
615 
616 #line 55 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/quantifiers/options"
618 #line 55 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/quantifiers/options"
619 inline bool foPropQuant__option_t::wasSetByUser() const { return Options::current().wasSetByUser(*this); }
620 
621 #line 59 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/quantifiers/options"
623 #line 59 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/quantifiers/options"
625 
626 #line 62 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/quantifiers/options"
628 #line 62 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/quantifiers/options"
630 
631 #line 64 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/quantifiers/options"
633 #line 64 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/quantifiers/options"
635 
636 #line 68 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/quantifiers/options"
638 #line 68 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/quantifiers/options"
640 
641 #line 71 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/quantifiers/options"
643 #line 71 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/quantifiers/options"
645 #line 71 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/quantifiers/options"
647 
648 #line 73 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/quantifiers/options"
650 #line 73 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/quantifiers/options"
652 
653 #line 76 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/quantifiers/options"
655 #line 76 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/quantifiers/options"
657 
658 #line 79 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/quantifiers/options"
660 #line 79 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/quantifiers/options"
662 
663 #line 82 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/quantifiers/options"
665 #line 82 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/quantifiers/options"
667 
668 #line 85 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/quantifiers/options"
670 #line 85 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/quantifiers/options"
671 inline bool cbqi__option_t::wasSetByUser() const { return Options::current().wasSetByUser(*this); }
672 #line 85 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/quantifiers/options"
673 inline void cbqi__option_t::set(const cbqi__option_t::type& v) { Options::current().set(*this, v); }
674 
675 #line 88 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/quantifiers/options"
677 #line 88 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/quantifiers/options"
678 inline bool recurseCbqi__option_t::wasSetByUser() const { return Options::current().wasSetByUser(*this); }
679 
680 #line 91 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/quantifiers/options"
682 #line 91 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/quantifiers/options"
684 
685 #line 94 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/quantifiers/options"
687 #line 94 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/quantifiers/options"
689 
690 #line 97 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/quantifiers/options"
692 #line 97 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/quantifiers/options"
694 
695 #line 100 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/quantifiers/options"
697 #line 100 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/quantifiers/options"
699 #line 100 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/quantifiers/options"
701 
702 #line 103 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/quantifiers/options"
704 #line 103 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/quantifiers/options"
705 inline bool mbqiMode__option_t::wasSetByUser() const { return Options::current().wasSetByUser(*this); }
706 #line 103 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/quantifiers/options"
708 
709 #line 105 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/quantifiers/options"
711 #line 105 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/quantifiers/options"
713 
714 #line 107 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/quantifiers/options"
716 #line 107 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/quantifiers/options"
718 
719 #line 110 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/quantifiers/options"
721 #line 110 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/quantifiers/options"
723 
724 #line 112 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/quantifiers/options"
726 #line 112 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/quantifiers/options"
727 inline bool fmfInstGen__option_t::wasSetByUser() const { return Options::current().wasSetByUser(*this); }
728 
729 #line 114 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/quantifiers/options"
731 #line 114 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/quantifiers/options"
733 
734 #line 116 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/quantifiers/options"
736 #line 116 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/quantifiers/options"
738 
739 #line 118 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/quantifiers/options"
741 #line 118 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/quantifiers/options"
743 
744 #line 120 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/quantifiers/options"
746 #line 120 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/quantifiers/options"
747 inline bool fmfBoundInt__option_t::wasSetByUser() const { return Options::current().wasSetByUser(*this); }
748 #line 120 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/quantifiers/options"
750 
751 #line 122 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/quantifiers/options"
753 #line 122 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/quantifiers/options"
755 #line 122 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/quantifiers/options"
757 
758 #line 125 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/quantifiers/options"
760 #line 125 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/quantifiers/options"
762 
763 #line 128 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/quantifiers/options"
765 #line 128 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/quantifiers/options"
767 #line 128 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/quantifiers/options"
769 
770 #line 130 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/quantifiers/options"
772 #line 130 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/quantifiers/options"
773 inline bool qcfMode__option_t::wasSetByUser() const { return Options::current().wasSetByUser(*this); }
774 
775 #line 132 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/quantifiers/options"
777 #line 132 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/quantifiers/options"
778 inline bool qcfWhenMode__option_t::wasSetByUser() const { return Options::current().wasSetByUser(*this); }
779 
780 #line 134 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/quantifiers/options"
782 #line 134 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/quantifiers/options"
784 #line 134 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/quantifiers/options"
786 
787 #line 137 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/quantifiers/options"
789 #line 137 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/quantifiers/options"
791 
792 #line 139 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/quantifiers/options"
794 #line 139 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/quantifiers/options"
796 
797 #line 142 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/quantifiers/options"
799 #line 142 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/quantifiers/options"
801 
802 #line 50 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/base_options_template.h"
803 
804 }/* CVC4::options namespace */
805 
806 }/* CVC4 namespace */
807 
808 #endif /* __CVC4__OPTIONS__QUANTIFIERS_H */
struct CVC4::options::foPropQuant__option_t foPropQuant
struct CVC4::options::fmfBoundIntLazy__option_t fmfBoundIntLazy
CVC4::theory::quantifiers::QcfMode type
Definition: options.h:248
struct CVC4::options::fmfOneInstPerRound__option_t fmfOneInstPerRound
struct CVC4::options::quantConflictFind__option_t quantConflictFind
struct CVC4::options::quantRewriteRules__option_t quantRewriteRules
struct CVC4::options::fullSaturateQuant__option_t fullSaturateQuant
struct CVC4::options::finiteModelFind__option_t finiteModelFind
struct CVC4::options::mbqiMode__option_t mbqiMode
struct CVC4::options::fmfBoundInt__option_t fmfBoundInt
struct CVC4::options::rrOneInstPerRound__option_t rrOneInstPerRound
struct CVC4::options::userPatternsQuant__option_t userPatternsQuant
CVC4::theory::quantifiers::AxiomInstMode type
Definition: options.h:244
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
CVC4::theory::quantifiers::UserPatMode type
Definition: options.h:216
CVC4::theory::quantifiers::MbqiMode type
Definition: options.h:224
struct CVC4::options::miniscopeQuantFreeVar__option_t miniscopeQuantFreeVar
struct CVC4::options::simpleIteLiftQuant__option_t simpleIteLiftQuant
CVC4::theory::quantifiers::InstWhenMode type
Definition: options.h:202
CVC4::theory::quantifiers::QcfWhenMode type
Definition: options.h:250
struct CVC4::options::prenexQuant__option_t prenexQuant
struct CVC4::options::aggressiveMiniscopeQuant__option_t aggressiveMiniscopeQuant
struct CVC4::options::instWhenMode__option_t instWhenMode
const T::type & operator[](T) const
Get the value of the given option.
struct CVC4::options::dtStcInduction__option_t dtStcInduction
struct CVC4::options::smartTriggers__option_t smartTriggers
struct CVC4::options::axiomInstMode__option_t axiomInstMode
struct CVC4::options::qcfWhenMode__option_t qcfWhenMode
struct CVC4::options::instMaxLevel__option_t instMaxLevel
#define CVC4_PUBLIC
Definition: cvc4_public.h:30
struct CVC4::options::fmfInstEngine__option_t fmfInstEngine
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::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::varElimQuant__option_t varElimQuant
Global (command-line, set-option, ...) parameters for SMT.
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
void set(const type &v)
Definition: options.h:707
struct CVC4::options::miniscopeQuant__option_t miniscopeQuant
struct CVC4::options::fmfFreshDistConst__option_t fmfFreshDistConst
CVC4::theory::quantifiers::LiteralMatchMode type
Definition: options.h:210
struct CVC4::options::nnfQuant__option_t nnfQuant
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::relationalTriggers__option_t relationalTriggers
struct CVC4::options::flipDecision__option_t flipDecision
struct CVC4::options::qcfTConstraint__option_t qcfTConstraint
struct CVC4::options::qcfMode__option_t qcfMode
struct CVC4::options::fmfInstGenOneQuantPerRound__option_t fmfInstGenOneQuantPerRound
void set(const type &v)
Definition: options.h:673