48 #ifndef __CVC4__OPTIONS__BV_H
49 #define __CVC4__OPTIONS__BV_H
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"
58 #line 26 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/base_options_template.h"
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__;
96 #line 30 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/base_options_template.h"
103 #line 10 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/bv/options"
105 #line 15 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/bv/options"
107 #line 18 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/bv/options"
109 #line 23 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/bv/options"
111 #line 26 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/bv/options"
113 #line 29 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/bv/options"
115 #line 32 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/bv/options"
117 #line 35 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/bv/options"
119 #line 38 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/bv/options"
121 #line 43 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/bv/options"
123 #line 46 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/bv/options"
125 #line 49 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/bv/options"
127 #line 52 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/bv/options"
129 #line 55 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/bv/options"
131 #line 58 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/bv/options"
133 #line 61 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/bv/options"
135 #line 64 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/bv/options"
138 #line 38 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/base_options_template.h"
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"
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"
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"
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"
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"
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"
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"
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"
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"
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"
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"
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"
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"
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"
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"
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"
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"
272 #line 44 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/base_options_template.h"
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"
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"
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"
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"
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"
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"
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"
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"
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"
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"
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"
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"
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"
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"
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"
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"
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"
388 #line 50 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/base_options_template.h"
struct CVC4::options::bvEagerExplanations__option_t bvEagerExplanations
bool wasSetByUser() const
bool wasSetByUser() const
struct CVC4::options::bitvectorEqualitySlicer__option_t bitvectorEqualitySlicer
bool wasSetByUser() const
bool wasSetByUser() const
struct CVC4::options::skolemizeArguments__option_t skolemizeArguments
bool wasSetByUser() const
CVC4::theory::bv::BvSlicerMode type
struct CVC4::options::bitvectorEqualitySolver__option_t bitvectorEqualitySolver
struct CVC4::options::bitvectorToBool__option_t bitvectorToBool
struct CVC4::options::bitvectorAlgebraicSolver__option_t bitvectorAlgebraicSolver
const T::type & operator[](T) const
Get the value of the given option.
bool wasSetByUser() const
struct CVC4::options::bitvectorPropagate__option_t bitvectorPropagate
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::bitvectorAigSimplifications__option_t bitvectorAigSimplifications
struct CVC4::options::bitvectorQuickXplain__option_t bitvectorQuickXplain
struct CVC4::options::bvIntroducePow2__option_t bvIntroducePow2
bool wasSetByUser() const
struct CVC4::options::bitvectorDivByZeroConst__option_t bitvectorDivByZeroConst
struct CVC4::options::bvAbstraction__option_t bvAbstraction
bool wasSetByUser() const
struct CVC4::options::bitvectorInequalitySolver__option_t bitvectorInequalitySolver
bool wasSetByUser() const
Global (command-line, set-option, ...) parameters for SMT.
static Options & current()
Get the current Options in effect.
Macros that should be defined everywhere during the building of the libraries and driver binary...
bool wasSetByUser() const
struct CVC4::options::bitvectorAlgebraicBudget__option_t bitvectorAlgebraicBudget
struct CVC4::options::bitvectorAig__option_t bitvectorAig
struct CVC4::options::bitblastMode__option_t bitblastMode
bool wasSetByUser() const
void set(T, const typename T::type &)
Set the value of the given option.
bool wasSetByUser() const
bool wasSetByUser() const
CVC4::theory::bv::BitblastMode type
bool wasSetByUser() const
bool wasSetByUser() const
bool wasSetByUser() const
struct CVC4::options::bvNumFunc__option_t bvNumFunc
bool wasSetByUser() const