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__BV_H
49 #define __CVC4__OPTIONS__BV_H
50 
51 #include "options/options.h"
52 
53 #line 10 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/bv/options"
54 #include "theory/bv/bitblast_mode.h"
55 #line 29 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/bv/options"
56 #include "theory/bv/bitblast_mode.h"
57 
58 #line 26 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/base_options_template.h"
59 
60 #define CVC4_OPTIONS__BV__FOR_OPTION_HOLDER \
61  bitblastMode__option_t::type bitblastMode; \
62  bool bitblastMode__setByUser__; \
63  bitvectorAig__option_t::type bitvectorAig; \
64  bool bitvectorAig__setByUser__; \
65  bitvectorAigSimplifications__option_t::type bitvectorAigSimplifications; \
66  bool bitvectorAigSimplifications__setByUser__; \
67  bitvectorPropagate__option_t::type bitvectorPropagate; \
68  bool bitvectorPropagate__setByUser__; \
69  bitvectorEqualitySolver__option_t::type bitvectorEqualitySolver; \
70  bool bitvectorEqualitySolver__setByUser__; \
71  bitvectorEqualitySlicer__option_t::type bitvectorEqualitySlicer; \
72  bool bitvectorEqualitySlicer__setByUser__; \
73  bitvectorInequalitySolver__option_t::type bitvectorInequalitySolver; \
74  bool bitvectorInequalitySolver__setByUser__; \
75  bitvectorAlgebraicSolver__option_t::type bitvectorAlgebraicSolver; \
76  bool bitvectorAlgebraicSolver__setByUser__; \
77  bitvectorAlgebraicBudget__option_t::type bitvectorAlgebraicBudget; \
78  bool bitvectorAlgebraicBudget__setByUser__; \
79  bitvectorToBool__option_t::type bitvectorToBool; \
80  bool bitvectorToBool__setByUser__; \
81  bitvectorDivByZeroConst__option_t::type bitvectorDivByZeroConst; \
82  bool bitvectorDivByZeroConst__setByUser__; \
83  bvAbstraction__option_t::type bvAbstraction; \
84  bool bvAbstraction__setByUser__; \
85  skolemizeArguments__option_t::type skolemizeArguments; \
86  bool skolemizeArguments__setByUser__; \
87  bvNumFunc__option_t::type bvNumFunc; \
88  bool bvNumFunc__setByUser__; \
89  bvEagerExplanations__option_t::type bvEagerExplanations; \
90  bool bvEagerExplanations__setByUser__; \
91  bitvectorQuickXplain__option_t::type bitvectorQuickXplain; \
92  bool bitvectorQuickXplain__setByUser__; \
93  bvIntroducePow2__option_t::type bvIntroducePow2; \
94  bool bvIntroducePow2__setByUser__;
95 
96 #line 30 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/base_options_template.h"
97 
98 namespace CVC4 {
99 
100 namespace options {
101 
102 
103 #line 10 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/bv/options"
104 extern struct CVC4_PUBLIC bitblastMode__option_t { typedef CVC4::theory::bv::BitblastMode type; type operator()() const; bool wasSetByUser() const; void set(const type& v); } bitblastMode CVC4_PUBLIC;
105 #line 15 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/bv/options"
106 extern struct CVC4_PUBLIC bitvectorAig__option_t { typedef bool type; type operator()() const; bool wasSetByUser() const; void set(const type& v); } bitvectorAig CVC4_PUBLIC;
107 #line 18 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/bv/options"
108 extern struct CVC4_PUBLIC bitvectorAigSimplifications__option_t { typedef std::string type; type operator()() const; bool wasSetByUser() const; void set(const type& v); } bitvectorAigSimplifications CVC4_PUBLIC;
109 #line 23 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/bv/options"
110 extern struct CVC4_PUBLIC bitvectorPropagate__option_t { typedef bool type; type operator()() const; bool wasSetByUser() const; void set(const type& v); } bitvectorPropagate CVC4_PUBLIC;
111 #line 26 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/bv/options"
112 extern struct CVC4_PUBLIC bitvectorEqualitySolver__option_t { typedef bool type; type operator()() const; bool wasSetByUser() const; void set(const type& v); } bitvectorEqualitySolver CVC4_PUBLIC;
113 #line 29 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/bv/options"
114 extern struct CVC4_PUBLIC bitvectorEqualitySlicer__option_t { typedef CVC4::theory::bv::BvSlicerMode type; type operator()() const; bool wasSetByUser() const; void set(const type& v); } bitvectorEqualitySlicer CVC4_PUBLIC;
115 #line 32 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/bv/options"
116 extern struct CVC4_PUBLIC bitvectorInequalitySolver__option_t { typedef bool type; type operator()() const; bool wasSetByUser() const; void set(const type& v); } bitvectorInequalitySolver CVC4_PUBLIC;
117 #line 35 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/bv/options"
118 extern struct CVC4_PUBLIC bitvectorAlgebraicSolver__option_t { typedef bool type; type operator()() const; bool wasSetByUser() const; void set(const type& v); } bitvectorAlgebraicSolver CVC4_PUBLIC;
119 #line 38 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/bv/options"
120 extern struct CVC4_PUBLIC bitvectorAlgebraicBudget__option_t { typedef unsigned type; type operator()() const; bool wasSetByUser() const; void set(const type& v); } bitvectorAlgebraicBudget CVC4_PUBLIC;
121 #line 43 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/bv/options"
122 extern struct CVC4_PUBLIC bitvectorToBool__option_t { typedef bool type; type operator()() const; bool wasSetByUser() const; void set(const type& v); } bitvectorToBool CVC4_PUBLIC;
123 #line 46 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/bv/options"
124 extern struct CVC4_PUBLIC bitvectorDivByZeroConst__option_t { typedef bool type; type operator()() const; bool wasSetByUser() const; } bitvectorDivByZeroConst CVC4_PUBLIC;
125 #line 49 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/bv/options"
126 extern struct CVC4_PUBLIC bvAbstraction__option_t { typedef bool type; type operator()() const; bool wasSetByUser() const; void set(const type& v); } bvAbstraction CVC4_PUBLIC;
127 #line 52 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/bv/options"
128 extern struct CVC4_PUBLIC skolemizeArguments__option_t { typedef bool type; type operator()() const; bool wasSetByUser() const; void set(const type& v); } skolemizeArguments CVC4_PUBLIC;
129 #line 55 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/bv/options"
130 extern struct CVC4_PUBLIC bvNumFunc__option_t { typedef unsigned type; type operator()() const; bool wasSetByUser() const; } bvNumFunc CVC4_PUBLIC;
131 #line 58 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/bv/options"
132 extern struct CVC4_PUBLIC bvEagerExplanations__option_t { typedef bool type; type operator()() const; bool wasSetByUser() const; void set(const type& v); } bvEagerExplanations CVC4_PUBLIC;
133 #line 61 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/bv/options"
134 extern struct CVC4_PUBLIC bitvectorQuickXplain__option_t { typedef bool type; type operator()() const; bool wasSetByUser() const; } bitvectorQuickXplain CVC4_PUBLIC;
135 #line 64 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/bv/options"
136 extern struct CVC4_PUBLIC bvIntroducePow2__option_t { typedef bool type; type operator()() const; bool wasSetByUser() const; } bvIntroducePow2 CVC4_PUBLIC;
137 
138 #line 38 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/base_options_template.h"
139 
140 }/* CVC4::options namespace */
141 
142 
143 #line 10 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/bv/options"
145 #line 10 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/bv/options"
147 #line 10 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/bv/options"
149 #line 10 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/bv/options"
150 template <> void Options::assign(options::bitblastMode__option_t, std::string option, std::string value, SmtEngine* smt);
151 #line 15 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/bv/options"
153 #line 15 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/bv/options"
155 #line 15 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/bv/options"
157 #line 15 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/bv/options"
158 template <> void Options::assignBool(options::bitvectorAig__option_t, std::string option, bool value, SmtEngine* smt);
159 #line 18 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/bv/options"
161 #line 18 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/bv/options"
163 #line 18 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/bv/options"
165 #line 18 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/bv/options"
166 template <> void Options::assign(options::bitvectorAigSimplifications__option_t, std::string option, std::string value, SmtEngine* smt);
167 #line 23 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/bv/options"
169 #line 23 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/bv/options"
171 #line 23 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/bv/options"
173 #line 23 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/bv/options"
174 template <> void Options::assignBool(options::bitvectorPropagate__option_t, std::string option, bool value, SmtEngine* smt);
175 #line 26 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/bv/options"
177 #line 26 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/bv/options"
179 #line 26 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/bv/options"
181 #line 26 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/bv/options"
182 template <> void Options::assignBool(options::bitvectorEqualitySolver__option_t, std::string option, bool value, SmtEngine* smt);
183 #line 29 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/bv/options"
185 #line 29 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/bv/options"
187 #line 29 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/bv/options"
189 #line 29 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/bv/options"
190 template <> void Options::assign(options::bitvectorEqualitySlicer__option_t, std::string option, std::string value, SmtEngine* smt);
191 #line 32 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/bv/options"
193 #line 32 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/bv/options"
195 #line 32 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/bv/options"
197 #line 32 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/bv/options"
198 template <> void Options::assignBool(options::bitvectorInequalitySolver__option_t, std::string option, bool value, SmtEngine* smt);
199 #line 35 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/bv/options"
201 #line 35 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/bv/options"
203 #line 35 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/bv/options"
205 #line 35 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/bv/options"
206 template <> void Options::assignBool(options::bitvectorAlgebraicSolver__option_t, std::string option, bool value, SmtEngine* smt);
207 #line 38 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/bv/options"
209 #line 38 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/bv/options"
211 #line 38 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/bv/options"
213 #line 38 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/bv/options"
214 template <> void Options::assign(options::bitvectorAlgebraicBudget__option_t, std::string option, std::string value, SmtEngine* smt);
215 #line 43 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/bv/options"
217 #line 43 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/bv/options"
219 #line 43 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/bv/options"
221 #line 43 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/bv/options"
222 template <> void Options::assignBool(options::bitvectorToBool__option_t, std::string option, bool value, SmtEngine* smt);
223 #line 46 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/bv/options"
225 #line 46 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/bv/options"
227 #line 46 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/bv/options"
228 template <> void Options::assignBool(options::bitvectorDivByZeroConst__option_t, std::string option, bool value, SmtEngine* smt);
229 #line 49 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/bv/options"
231 #line 49 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/bv/options"
233 #line 49 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/bv/options"
235 #line 49 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/bv/options"
236 template <> void Options::assignBool(options::bvAbstraction__option_t, std::string option, bool value, SmtEngine* smt);
237 #line 52 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/bv/options"
239 #line 52 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/bv/options"
241 #line 52 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/bv/options"
243 #line 52 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/bv/options"
244 template <> void Options::assignBool(options::skolemizeArguments__option_t, std::string option, bool value, SmtEngine* smt);
245 #line 55 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/bv/options"
247 #line 55 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/bv/options"
249 #line 55 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/bv/options"
250 template <> void Options::assign(options::bvNumFunc__option_t, std::string option, std::string value, SmtEngine* smt);
251 #line 58 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/bv/options"
253 #line 58 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/bv/options"
255 #line 58 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/bv/options"
257 #line 58 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/bv/options"
258 template <> void Options::assignBool(options::bvEagerExplanations__option_t, std::string option, bool value, SmtEngine* smt);
259 #line 61 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/bv/options"
261 #line 61 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/bv/options"
263 #line 61 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/bv/options"
264 template <> void Options::assignBool(options::bitvectorQuickXplain__option_t, std::string option, bool value, SmtEngine* smt);
265 #line 64 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/bv/options"
267 #line 64 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/bv/options"
269 #line 64 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/bv/options"
270 template <> void Options::assignBool(options::bvIntroducePow2__option_t, std::string option, bool value, SmtEngine* smt);
271 
272 #line 44 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/base_options_template.h"
273 
274 namespace options {
275 
276 
277 #line 10 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/bv/options"
279 #line 10 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/bv/options"
281 #line 10 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/bv/options"
283 
284 #line 15 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/bv/options"
286 #line 15 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/bv/options"
288 #line 15 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/bv/options"
290 
291 #line 18 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/bv/options"
293 #line 18 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/bv/options"
295 #line 18 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/bv/options"
297 
298 #line 23 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/bv/options"
300 #line 23 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/bv/options"
302 #line 23 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/bv/options"
304 
305 #line 26 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/bv/options"
307 #line 26 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/bv/options"
309 #line 26 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/bv/options"
311 
312 #line 29 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/bv/options"
314 #line 29 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/bv/options"
316 #line 29 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/bv/options"
318 
319 #line 32 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/bv/options"
321 #line 32 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/bv/options"
323 #line 32 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/bv/options"
325 
326 #line 35 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/bv/options"
328 #line 35 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/bv/options"
330 #line 35 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/bv/options"
332 
333 #line 38 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/bv/options"
335 #line 38 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/bv/options"
337 #line 38 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/bv/options"
339 
340 #line 43 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/bv/options"
342 #line 43 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/bv/options"
344 #line 43 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/bv/options"
346 
347 #line 46 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/bv/options"
349 #line 46 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/bv/options"
351 
352 #line 49 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/bv/options"
354 #line 49 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/bv/options"
356 #line 49 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/bv/options"
358 
359 #line 52 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/bv/options"
361 #line 52 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/bv/options"
363 #line 52 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/bv/options"
365 
366 #line 55 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/bv/options"
368 #line 55 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/bv/options"
369 inline bool bvNumFunc__option_t::wasSetByUser() const { return Options::current().wasSetByUser(*this); }
370 
371 #line 58 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/bv/options"
373 #line 58 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/bv/options"
375 #line 58 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/bv/options"
377 
378 #line 61 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/bv/options"
380 #line 61 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/bv/options"
382 
383 #line 64 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/bv/options"
385 #line 64 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/bv/options"
387 
388 #line 50 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/base_options_template.h"
389 
390 }/* CVC4::options namespace */
391 
392 }/* CVC4 namespace */
393 
394 #endif /* __CVC4__OPTIONS__BV_H */
Definition: kind.h:57
struct CVC4::options::bvEagerExplanations__option_t bvEagerExplanations
struct CVC4::options::bitvectorEqualitySlicer__option_t bitvectorEqualitySlicer
struct CVC4::options::skolemizeArguments__option_t skolemizeArguments
CVC4::theory::bv::BvSlicerMode type
Definition: options.h:114
struct CVC4::options::bitvectorEqualitySolver__option_t bitvectorEqualitySolver
struct CVC4::options::bitvectorToBool__option_t bitvectorToBool
struct CVC4::options::bitvectorAlgebraicSolver__option_t bitvectorAlgebraicSolver
struct CVC4::options::bitvectorPropagate__option_t bitvectorPropagate
struct CVC4::options::bitvectorAigSimplifications__option_t bitvectorAigSimplifications
struct CVC4::options::bitvectorQuickXplain__option_t bitvectorQuickXplain
struct CVC4::options::bvIntroducePow2__option_t bvIntroducePow2
const T::type & operator[](T) const
Get the value of the given option.
struct CVC4::options::bitvectorDivByZeroConst__option_t bitvectorDivByZeroConst
struct CVC4::options::bvAbstraction__option_t bvAbstraction
#define CVC4_PUBLIC
Definition: cvc4_public.h:30
struct CVC4::options::bitvectorInequalitySolver__option_t bitvectorInequalitySolver
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...
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::bitvectorAlgebraicBudget__option_t bitvectorAlgebraicBudget
struct CVC4::options::bitvectorAig__option_t bitvectorAig
struct CVC4::options::bitblastMode__option_t bitblastMode
void set(T, const typename T::type &)
Set the value of the given option.
Definition: options.h:78
CVC4::theory::bv::BitblastMode type
Definition: options.h:104
struct CVC4::options::bvNumFunc__option_t bvNumFunc