cvc4-1.3
options.h
Go to the documentation of this file.
1 /********************* */
14 /* THIS FILE IS AUTOMATICALLY GENERATED, DO NOT EDIT ! */
15 /* THIS FILE IS AUTOMATICALLY GENERATED, DO NOT EDIT ! */
16 /* THIS FILE IS AUTOMATICALLY GENERATED, DO NOT EDIT ! */
17 /* THIS FILE IS AUTOMATICALLY GENERATED, DO NOT EDIT ! */
18 /* THIS FILE IS AUTOMATICALLY GENERATED, DO NOT EDIT ! */
19 /* THIS FILE IS AUTOMATICALLY GENERATED, DO NOT EDIT ! */
20 
21 /* THIS FILE IS AUTOMATICALLY GENERATED, DO NOT EDIT ! */
22 /* THIS FILE IS AUTOMATICALLY GENERATED, DO NOT EDIT ! */
23 /* THIS FILE IS AUTOMATICALLY GENERATED, DO NOT EDIT ! */
24 /* THIS FILE IS AUTOMATICALLY GENERATED, DO NOT EDIT ! */
25 /* THIS FILE IS AUTOMATICALLY GENERATED, DO NOT EDIT ! */
26 /* THIS FILE IS AUTOMATICALLY GENERATED, DO NOT EDIT ! */
27 
28 /* Edit the template file instead. */
29 
30 /********************* */
46 #include "cvc4_public.h"
47 
48 #ifndef __CVC4__OPTIONS__ARITH_H
49 #define __CVC4__OPTIONS__ARITH_H
50 
51 #include "options/options.h"
52 
53 #line 8 "/builddir/build/BUILD/cvc4-1.3/builds/powerpc-redhat-linux-gnu/default-proof/../../../src/options/../theory/arith/options"
55 #line 11 "/builddir/build/BUILD/cvc4-1.3/builds/powerpc-redhat-linux-gnu/default-proof/../../../src/options/../theory/arith/options"
57 #line 28 "/builddir/build/BUILD/cvc4-1.3/builds/powerpc-redhat-linux-gnu/default-proof/../../../src/options/../theory/arith/options"
59 
60 #line 26 "/builddir/build/BUILD/cvc4-1.3/builds/powerpc-redhat-linux-gnu/default-proof/../../../src/options/base_options_template.h"
61 
62 #define CVC4_OPTIONS__ARITH__FOR_OPTION_HOLDER \
63  arithUnateLemmaMode__option_t::type arithUnateLemmaMode; \
64  bool arithUnateLemmaMode__setByUser__; \
65  arithPropagationMode__option_t::type arithPropagationMode; \
66  bool arithPropagationMode__setByUser__; \
67  arithHeuristicPivots__option_t::type arithHeuristicPivots; \
68  bool arithHeuristicPivots__setByUser__; \
69  arithStandardCheckVarOrderPivots__option_t::type arithStandardCheckVarOrderPivots; \
70  bool arithStandardCheckVarOrderPivots__setByUser__; \
71  arithErrorSelectionRule__option_t::type arithErrorSelectionRule; \
72  bool arithErrorSelectionRule__setByUser__; \
73  arithSimplexCheckPeriod__option_t::type arithSimplexCheckPeriod; \
74  bool arithSimplexCheckPeriod__setByUser__; \
75  arithPivotThreshold__option_t::type arithPivotThreshold; \
76  bool arithPivotThreshold__setByUser__; \
77  arithPropagateMaxLength__option_t::type arithPropagateMaxLength; \
78  bool arithPropagateMaxLength__setByUser__; \
79  arithDioSolver__option_t::type arithDioSolver; \
80  bool arithDioSolver__setByUser__; \
81  arithRewriteEq__option_t::type arithRewriteEq; \
82  bool arithRewriteEq__setByUser__; \
83  arithMLTrick__option_t::type arithMLTrick; \
84  bool arithMLTrick__setByUser__; \
85  arithMLTrickSubstitutions__option_t::type arithMLTrickSubstitutions; \
86  bool arithMLTrickSubstitutions__setByUser__; \
87  doCutAllBounded__option_t::type doCutAllBounded; \
88  bool doCutAllBounded__setByUser__; \
89  maxCutsInContext__option_t::type maxCutsInContext; \
90  bool maxCutsInContext__setByUser__; \
91  revertArithModels__option_t::type revertArithModels; \
92  bool revertArithModels__setByUser__; \
93  havePenalties__option_t::type havePenalties; \
94  bool havePenalties__setByUser__; \
95  useFC__option_t::type useFC; \
96  bool useFC__setByUser__; \
97  useSOI__option_t::type useSOI; \
98  bool useSOI__setByUser__; \
99  restrictedPivots__option_t::type restrictedPivots; \
100  bool restrictedPivots__setByUser__; \
101  collectPivots__option_t::type collectPivots; \
102  bool collectPivots__setByUser__; \
103  fancyFinal__option_t::type fancyFinal; \
104  bool fancyFinal__setByUser__; \
105  exportDioDecompositions__option_t::type exportDioDecompositions; \
106  bool exportDioDecompositions__setByUser__; \
107  newProp__option_t::type newProp; \
108  bool newProp__setByUser__; \
109  arithPropAsLemmaLength__option_t::type arithPropAsLemmaLength; \
110  bool arithPropAsLemmaLength__setByUser__; \
111  soiQuickExplain__option_t::type soiQuickExplain; \
112  bool soiQuickExplain__setByUser__; \
113  rewriteDivk__option_t::type rewriteDivk; \
114  bool rewriteDivk__setByUser__;
115 
116 #line 30 "/builddir/build/BUILD/cvc4-1.3/builds/powerpc-redhat-linux-gnu/default-proof/../../../src/options/base_options_template.h"
117 
118 namespace CVC4 {
119 
120 namespace options {
121 
122 
123 #line 8 "/builddir/build/BUILD/cvc4-1.3/builds/powerpc-redhat-linux-gnu/default-proof/../../../src/options/../theory/arith/options"
124 extern struct CVC4_PUBLIC arithUnateLemmaMode__option_t { typedef ArithUnateLemmaMode type; type operator()() const; bool wasSetByUser() const; } arithUnateLemmaMode CVC4_PUBLIC;
125 #line 11 "/builddir/build/BUILD/cvc4-1.3/builds/powerpc-redhat-linux-gnu/default-proof/../../../src/options/../theory/arith/options"
126 extern struct CVC4_PUBLIC arithPropagationMode__option_t { typedef ArithPropagationMode type; type operator()() const; bool wasSetByUser() const; } arithPropagationMode CVC4_PUBLIC;
127 #line 18 "/builddir/build/BUILD/cvc4-1.3/builds/powerpc-redhat-linux-gnu/default-proof/../../../src/options/../theory/arith/options"
128 extern struct CVC4_PUBLIC arithHeuristicPivots__option_t { typedef int16_t type; type operator()() const; bool wasSetByUser() const; void set(const type& v); } arithHeuristicPivots CVC4_PUBLIC;
129 #line 25 "/builddir/build/BUILD/cvc4-1.3/builds/powerpc-redhat-linux-gnu/default-proof/../../../src/options/../theory/arith/options"
130 extern struct CVC4_PUBLIC arithStandardCheckVarOrderPivots__option_t { typedef int16_t type; type operator()() const; bool wasSetByUser() const; void set(const type& v); } arithStandardCheckVarOrderPivots CVC4_PUBLIC;
131 #line 28 "/builddir/build/BUILD/cvc4-1.3/builds/powerpc-redhat-linux-gnu/default-proof/../../../src/options/../theory/arith/options"
132 extern struct CVC4_PUBLIC arithErrorSelectionRule__option_t { typedef ErrorSelectionRule type; type operator()() const; bool wasSetByUser() const; } arithErrorSelectionRule CVC4_PUBLIC;
133 #line 32 "/builddir/build/BUILD/cvc4-1.3/builds/powerpc-redhat-linux-gnu/default-proof/../../../src/options/../theory/arith/options"
134 extern struct CVC4_PUBLIC arithSimplexCheckPeriod__option_t { typedef uint16_t type; type operator()() const; bool wasSetByUser() const; } arithSimplexCheckPeriod CVC4_PUBLIC;
135 #line 39 "/builddir/build/BUILD/cvc4-1.3/builds/powerpc-redhat-linux-gnu/default-proof/../../../src/options/../theory/arith/options"
136 extern struct CVC4_PUBLIC arithPivotThreshold__option_t { typedef uint16_t type; type operator()() const; bool wasSetByUser() const; void set(const type& v); } arithPivotThreshold CVC4_PUBLIC;
137 #line 42 "/builddir/build/BUILD/cvc4-1.3/builds/powerpc-redhat-linux-gnu/default-proof/../../../src/options/../theory/arith/options"
138 extern struct CVC4_PUBLIC arithPropagateMaxLength__option_t { typedef uint16_t type; type operator()() const; bool wasSetByUser() const; } arithPropagateMaxLength CVC4_PUBLIC;
139 #line 45 "/builddir/build/BUILD/cvc4-1.3/builds/powerpc-redhat-linux-gnu/default-proof/../../../src/options/../theory/arith/options"
140 extern struct CVC4_PUBLIC arithDioSolver__option_t { typedef bool type; type operator()() const; bool wasSetByUser() const; } arithDioSolver CVC4_PUBLIC;
141 #line 50 "/builddir/build/BUILD/cvc4-1.3/builds/powerpc-redhat-linux-gnu/default-proof/../../../src/options/../theory/arith/options"
142 extern struct CVC4_PUBLIC arithRewriteEq__option_t { typedef bool type; type operator()() const; bool wasSetByUser() const; void set(const type& v); } arithRewriteEq CVC4_PUBLIC;
143 #line 55 "/builddir/build/BUILD/cvc4-1.3/builds/powerpc-redhat-linux-gnu/default-proof/../../../src/options/../theory/arith/options"
144 extern struct CVC4_PUBLIC arithMLTrick__option_t { typedef bool type; type operator()() const; bool wasSetByUser() const; } arithMLTrick CVC4_PUBLIC;
145 #line 59 "/builddir/build/BUILD/cvc4-1.3/builds/powerpc-redhat-linux-gnu/default-proof/../../../src/options/../theory/arith/options"
146 extern struct CVC4_PUBLIC arithMLTrickSubstitutions__option_t { typedef unsigned type; type operator()() const; bool wasSetByUser() const; } arithMLTrickSubstitutions CVC4_PUBLIC;
147 #line 62 "/builddir/build/BUILD/cvc4-1.3/builds/powerpc-redhat-linux-gnu/default-proof/../../../src/options/../theory/arith/options"
148 extern struct CVC4_PUBLIC doCutAllBounded__option_t { typedef bool type; type operator()() const; bool wasSetByUser() const; void set(const type& v); } doCutAllBounded CVC4_PUBLIC;
149 #line 66 "/builddir/build/BUILD/cvc4-1.3/builds/powerpc-redhat-linux-gnu/default-proof/../../../src/options/../theory/arith/options"
150 extern struct CVC4_PUBLIC maxCutsInContext__option_t { typedef unsigned type; type operator()() const; bool wasSetByUser() const; } maxCutsInContext CVC4_PUBLIC;
151 #line 69 "/builddir/build/BUILD/cvc4-1.3/builds/powerpc-redhat-linux-gnu/default-proof/../../../src/options/../theory/arith/options"
152 extern struct CVC4_PUBLIC revertArithModels__option_t { typedef bool type; type operator()() const; bool wasSetByUser() const; } revertArithModels CVC4_PUBLIC;
153 #line 72 "/builddir/build/BUILD/cvc4-1.3/builds/powerpc-redhat-linux-gnu/default-proof/../../../src/options/../theory/arith/options"
154 extern struct CVC4_PUBLIC havePenalties__option_t { typedef bool type; type operator()() const; bool wasSetByUser() const; void set(const type& v); } havePenalties CVC4_PUBLIC;
155 #line 76 "/builddir/build/BUILD/cvc4-1.3/builds/powerpc-redhat-linux-gnu/default-proof/../../../src/options/../theory/arith/options"
156 extern struct CVC4_PUBLIC useFC__option_t { typedef bool type; type operator()() const; bool wasSetByUser() const; void set(const type& v); } useFC CVC4_PUBLIC;
157 #line 79 "/builddir/build/BUILD/cvc4-1.3/builds/powerpc-redhat-linux-gnu/default-proof/../../../src/options/../theory/arith/options"
158 extern struct CVC4_PUBLIC useSOI__option_t { typedef bool type; type operator()() const; bool wasSetByUser() const; void set(const type& v); } useSOI CVC4_PUBLIC;
159 #line 82 "/builddir/build/BUILD/cvc4-1.3/builds/powerpc-redhat-linux-gnu/default-proof/../../../src/options/../theory/arith/options"
160 extern struct CVC4_PUBLIC restrictedPivots__option_t { typedef bool type; type operator()() const; bool wasSetByUser() const; void set(const type& v); } restrictedPivots CVC4_PUBLIC;
161 #line 85 "/builddir/build/BUILD/cvc4-1.3/builds/powerpc-redhat-linux-gnu/default-proof/../../../src/options/../theory/arith/options"
162 extern struct CVC4_PUBLIC collectPivots__option_t { typedef bool type; type operator()() const; bool wasSetByUser() const; void set(const type& v); } collectPivots CVC4_PUBLIC;
163 #line 88 "/builddir/build/BUILD/cvc4-1.3/builds/powerpc-redhat-linux-gnu/default-proof/../../../src/options/../theory/arith/options"
164 extern struct CVC4_PUBLIC fancyFinal__option_t { typedef bool type; type operator()() const; bool wasSetByUser() const; void set(const type& v); } fancyFinal CVC4_PUBLIC;
165 #line 91 "/builddir/build/BUILD/cvc4-1.3/builds/powerpc-redhat-linux-gnu/default-proof/../../../src/options/../theory/arith/options"
166 extern struct CVC4_PUBLIC exportDioDecompositions__option_t { typedef bool type; type operator()() const; bool wasSetByUser() const; void set(const type& v); } exportDioDecompositions CVC4_PUBLIC;
167 #line 94 "/builddir/build/BUILD/cvc4-1.3/builds/powerpc-redhat-linux-gnu/default-proof/../../../src/options/../theory/arith/options"
168 extern struct CVC4_PUBLIC newProp__option_t { typedef bool type; type operator()() const; bool wasSetByUser() const; void set(const type& v); } newProp CVC4_PUBLIC;
169 #line 97 "/builddir/build/BUILD/cvc4-1.3/builds/powerpc-redhat-linux-gnu/default-proof/../../../src/options/../theory/arith/options"
170 extern struct CVC4_PUBLIC arithPropAsLemmaLength__option_t { typedef uint16_t type; type operator()() const; bool wasSetByUser() const; void set(const type& v); } arithPropAsLemmaLength CVC4_PUBLIC;
171 #line 100 "/builddir/build/BUILD/cvc4-1.3/builds/powerpc-redhat-linux-gnu/default-proof/../../../src/options/../theory/arith/options"
172 extern struct CVC4_PUBLIC soiQuickExplain__option_t { typedef bool type; type operator()() const; bool wasSetByUser() const; void set(const type& v); } soiQuickExplain CVC4_PUBLIC;
173 #line 103 "/builddir/build/BUILD/cvc4-1.3/builds/powerpc-redhat-linux-gnu/default-proof/../../../src/options/../theory/arith/options"
174 extern struct CVC4_PUBLIC rewriteDivk__option_t { typedef bool type; type operator()() const; bool wasSetByUser() const; } rewriteDivk CVC4_PUBLIC;
175 
176 #line 38 "/builddir/build/BUILD/cvc4-1.3/builds/powerpc-redhat-linux-gnu/default-proof/../../../src/options/base_options_template.h"
177 
178 }/* CVC4::options namespace */
179 
180 
181 #line 8 "/builddir/build/BUILD/cvc4-1.3/builds/powerpc-redhat-linux-gnu/default-proof/../../../src/options/../theory/arith/options"
183 #line 8 "/builddir/build/BUILD/cvc4-1.3/builds/powerpc-redhat-linux-gnu/default-proof/../../../src/options/../theory/arith/options"
185 #line 8 "/builddir/build/BUILD/cvc4-1.3/builds/powerpc-redhat-linux-gnu/default-proof/../../../src/options/../theory/arith/options"
186 template <> void Options::assign(options::arithUnateLemmaMode__option_t, std::string option, std::string value, SmtEngine* smt);
187 #line 11 "/builddir/build/BUILD/cvc4-1.3/builds/powerpc-redhat-linux-gnu/default-proof/../../../src/options/../theory/arith/options"
189 #line 11 "/builddir/build/BUILD/cvc4-1.3/builds/powerpc-redhat-linux-gnu/default-proof/../../../src/options/../theory/arith/options"
191 #line 11 "/builddir/build/BUILD/cvc4-1.3/builds/powerpc-redhat-linux-gnu/default-proof/../../../src/options/../theory/arith/options"
192 template <> void Options::assign(options::arithPropagationMode__option_t, std::string option, std::string value, SmtEngine* smt);
193 #line 18 "/builddir/build/BUILD/cvc4-1.3/builds/powerpc-redhat-linux-gnu/default-proof/../../../src/options/../theory/arith/options"
195 #line 18 "/builddir/build/BUILD/cvc4-1.3/builds/powerpc-redhat-linux-gnu/default-proof/../../../src/options/../theory/arith/options"
197 #line 18 "/builddir/build/BUILD/cvc4-1.3/builds/powerpc-redhat-linux-gnu/default-proof/../../../src/options/../theory/arith/options"
199 #line 18 "/builddir/build/BUILD/cvc4-1.3/builds/powerpc-redhat-linux-gnu/default-proof/../../../src/options/../theory/arith/options"
200 template <> void Options::assign(options::arithHeuristicPivots__option_t, std::string option, std::string value, SmtEngine* smt);
201 #line 25 "/builddir/build/BUILD/cvc4-1.3/builds/powerpc-redhat-linux-gnu/default-proof/../../../src/options/../theory/arith/options"
203 #line 25 "/builddir/build/BUILD/cvc4-1.3/builds/powerpc-redhat-linux-gnu/default-proof/../../../src/options/../theory/arith/options"
205 #line 25 "/builddir/build/BUILD/cvc4-1.3/builds/powerpc-redhat-linux-gnu/default-proof/../../../src/options/../theory/arith/options"
207 #line 25 "/builddir/build/BUILD/cvc4-1.3/builds/powerpc-redhat-linux-gnu/default-proof/../../../src/options/../theory/arith/options"
208 template <> void Options::assign(options::arithStandardCheckVarOrderPivots__option_t, std::string option, std::string value, SmtEngine* smt);
209 #line 28 "/builddir/build/BUILD/cvc4-1.3/builds/powerpc-redhat-linux-gnu/default-proof/../../../src/options/../theory/arith/options"
211 #line 28 "/builddir/build/BUILD/cvc4-1.3/builds/powerpc-redhat-linux-gnu/default-proof/../../../src/options/../theory/arith/options"
213 #line 28 "/builddir/build/BUILD/cvc4-1.3/builds/powerpc-redhat-linux-gnu/default-proof/../../../src/options/../theory/arith/options"
214 template <> void Options::assign(options::arithErrorSelectionRule__option_t, std::string option, std::string value, SmtEngine* smt);
215 #line 32 "/builddir/build/BUILD/cvc4-1.3/builds/powerpc-redhat-linux-gnu/default-proof/../../../src/options/../theory/arith/options"
217 #line 32 "/builddir/build/BUILD/cvc4-1.3/builds/powerpc-redhat-linux-gnu/default-proof/../../../src/options/../theory/arith/options"
219 #line 32 "/builddir/build/BUILD/cvc4-1.3/builds/powerpc-redhat-linux-gnu/default-proof/../../../src/options/../theory/arith/options"
220 template <> void Options::assign(options::arithSimplexCheckPeriod__option_t, std::string option, std::string value, SmtEngine* smt);
221 #line 39 "/builddir/build/BUILD/cvc4-1.3/builds/powerpc-redhat-linux-gnu/default-proof/../../../src/options/../theory/arith/options"
223 #line 39 "/builddir/build/BUILD/cvc4-1.3/builds/powerpc-redhat-linux-gnu/default-proof/../../../src/options/../theory/arith/options"
225 #line 39 "/builddir/build/BUILD/cvc4-1.3/builds/powerpc-redhat-linux-gnu/default-proof/../../../src/options/../theory/arith/options"
227 #line 39 "/builddir/build/BUILD/cvc4-1.3/builds/powerpc-redhat-linux-gnu/default-proof/../../../src/options/../theory/arith/options"
228 template <> void Options::assign(options::arithPivotThreshold__option_t, std::string option, std::string value, SmtEngine* smt);
229 #line 42 "/builddir/build/BUILD/cvc4-1.3/builds/powerpc-redhat-linux-gnu/default-proof/../../../src/options/../theory/arith/options"
231 #line 42 "/builddir/build/BUILD/cvc4-1.3/builds/powerpc-redhat-linux-gnu/default-proof/../../../src/options/../theory/arith/options"
233 #line 42 "/builddir/build/BUILD/cvc4-1.3/builds/powerpc-redhat-linux-gnu/default-proof/../../../src/options/../theory/arith/options"
234 template <> void Options::assign(options::arithPropagateMaxLength__option_t, std::string option, std::string value, SmtEngine* smt);
235 #line 45 "/builddir/build/BUILD/cvc4-1.3/builds/powerpc-redhat-linux-gnu/default-proof/../../../src/options/../theory/arith/options"
237 #line 45 "/builddir/build/BUILD/cvc4-1.3/builds/powerpc-redhat-linux-gnu/default-proof/../../../src/options/../theory/arith/options"
239 #line 45 "/builddir/build/BUILD/cvc4-1.3/builds/powerpc-redhat-linux-gnu/default-proof/../../../src/options/../theory/arith/options"
240 template <> void Options::assignBool(options::arithDioSolver__option_t, std::string option, bool value, SmtEngine* smt);
241 #line 50 "/builddir/build/BUILD/cvc4-1.3/builds/powerpc-redhat-linux-gnu/default-proof/../../../src/options/../theory/arith/options"
243 #line 50 "/builddir/build/BUILD/cvc4-1.3/builds/powerpc-redhat-linux-gnu/default-proof/../../../src/options/../theory/arith/options"
245 #line 50 "/builddir/build/BUILD/cvc4-1.3/builds/powerpc-redhat-linux-gnu/default-proof/../../../src/options/../theory/arith/options"
247 #line 50 "/builddir/build/BUILD/cvc4-1.3/builds/powerpc-redhat-linux-gnu/default-proof/../../../src/options/../theory/arith/options"
248 template <> void Options::assignBool(options::arithRewriteEq__option_t, std::string option, bool value, SmtEngine* smt);
249 #line 55 "/builddir/build/BUILD/cvc4-1.3/builds/powerpc-redhat-linux-gnu/default-proof/../../../src/options/../theory/arith/options"
251 #line 55 "/builddir/build/BUILD/cvc4-1.3/builds/powerpc-redhat-linux-gnu/default-proof/../../../src/options/../theory/arith/options"
253 #line 55 "/builddir/build/BUILD/cvc4-1.3/builds/powerpc-redhat-linux-gnu/default-proof/../../../src/options/../theory/arith/options"
254 template <> void Options::assignBool(options::arithMLTrick__option_t, std::string option, bool value, SmtEngine* smt);
255 #line 59 "/builddir/build/BUILD/cvc4-1.3/builds/powerpc-redhat-linux-gnu/default-proof/../../../src/options/../theory/arith/options"
257 #line 59 "/builddir/build/BUILD/cvc4-1.3/builds/powerpc-redhat-linux-gnu/default-proof/../../../src/options/../theory/arith/options"
259 #line 59 "/builddir/build/BUILD/cvc4-1.3/builds/powerpc-redhat-linux-gnu/default-proof/../../../src/options/../theory/arith/options"
260 template <> void Options::assign(options::arithMLTrickSubstitutions__option_t, std::string option, std::string value, SmtEngine* smt);
261 #line 62 "/builddir/build/BUILD/cvc4-1.3/builds/powerpc-redhat-linux-gnu/default-proof/../../../src/options/../theory/arith/options"
263 #line 62 "/builddir/build/BUILD/cvc4-1.3/builds/powerpc-redhat-linux-gnu/default-proof/../../../src/options/../theory/arith/options"
265 #line 62 "/builddir/build/BUILD/cvc4-1.3/builds/powerpc-redhat-linux-gnu/default-proof/../../../src/options/../theory/arith/options"
267 #line 62 "/builddir/build/BUILD/cvc4-1.3/builds/powerpc-redhat-linux-gnu/default-proof/../../../src/options/../theory/arith/options"
268 template <> void Options::assignBool(options::doCutAllBounded__option_t, std::string option, bool value, SmtEngine* smt);
269 #line 66 "/builddir/build/BUILD/cvc4-1.3/builds/powerpc-redhat-linux-gnu/default-proof/../../../src/options/../theory/arith/options"
271 #line 66 "/builddir/build/BUILD/cvc4-1.3/builds/powerpc-redhat-linux-gnu/default-proof/../../../src/options/../theory/arith/options"
273 #line 66 "/builddir/build/BUILD/cvc4-1.3/builds/powerpc-redhat-linux-gnu/default-proof/../../../src/options/../theory/arith/options"
274 template <> void Options::assign(options::maxCutsInContext__option_t, std::string option, std::string value, SmtEngine* smt);
275 #line 69 "/builddir/build/BUILD/cvc4-1.3/builds/powerpc-redhat-linux-gnu/default-proof/../../../src/options/../theory/arith/options"
277 #line 69 "/builddir/build/BUILD/cvc4-1.3/builds/powerpc-redhat-linux-gnu/default-proof/../../../src/options/../theory/arith/options"
279 #line 69 "/builddir/build/BUILD/cvc4-1.3/builds/powerpc-redhat-linux-gnu/default-proof/../../../src/options/../theory/arith/options"
280 template <> void Options::assignBool(options::revertArithModels__option_t, std::string option, bool value, SmtEngine* smt);
281 #line 72 "/builddir/build/BUILD/cvc4-1.3/builds/powerpc-redhat-linux-gnu/default-proof/../../../src/options/../theory/arith/options"
283 #line 72 "/builddir/build/BUILD/cvc4-1.3/builds/powerpc-redhat-linux-gnu/default-proof/../../../src/options/../theory/arith/options"
285 #line 72 "/builddir/build/BUILD/cvc4-1.3/builds/powerpc-redhat-linux-gnu/default-proof/../../../src/options/../theory/arith/options"
287 #line 72 "/builddir/build/BUILD/cvc4-1.3/builds/powerpc-redhat-linux-gnu/default-proof/../../../src/options/../theory/arith/options"
288 template <> void Options::assignBool(options::havePenalties__option_t, std::string option, bool value, SmtEngine* smt);
289 #line 76 "/builddir/build/BUILD/cvc4-1.3/builds/powerpc-redhat-linux-gnu/default-proof/../../../src/options/../theory/arith/options"
291 #line 76 "/builddir/build/BUILD/cvc4-1.3/builds/powerpc-redhat-linux-gnu/default-proof/../../../src/options/../theory/arith/options"
293 #line 76 "/builddir/build/BUILD/cvc4-1.3/builds/powerpc-redhat-linux-gnu/default-proof/../../../src/options/../theory/arith/options"
294 template <> bool Options::wasSetByUser(options::useFC__option_t) const;
295 #line 76 "/builddir/build/BUILD/cvc4-1.3/builds/powerpc-redhat-linux-gnu/default-proof/../../../src/options/../theory/arith/options"
296 template <> void Options::assignBool(options::useFC__option_t, std::string option, bool value, SmtEngine* smt);
297 #line 79 "/builddir/build/BUILD/cvc4-1.3/builds/powerpc-redhat-linux-gnu/default-proof/../../../src/options/../theory/arith/options"
299 #line 79 "/builddir/build/BUILD/cvc4-1.3/builds/powerpc-redhat-linux-gnu/default-proof/../../../src/options/../theory/arith/options"
301 #line 79 "/builddir/build/BUILD/cvc4-1.3/builds/powerpc-redhat-linux-gnu/default-proof/../../../src/options/../theory/arith/options"
302 template <> bool Options::wasSetByUser(options::useSOI__option_t) const;
303 #line 79 "/builddir/build/BUILD/cvc4-1.3/builds/powerpc-redhat-linux-gnu/default-proof/../../../src/options/../theory/arith/options"
304 template <> void Options::assignBool(options::useSOI__option_t, std::string option, bool value, SmtEngine* smt);
305 #line 82 "/builddir/build/BUILD/cvc4-1.3/builds/powerpc-redhat-linux-gnu/default-proof/../../../src/options/../theory/arith/options"
307 #line 82 "/builddir/build/BUILD/cvc4-1.3/builds/powerpc-redhat-linux-gnu/default-proof/../../../src/options/../theory/arith/options"
309 #line 82 "/builddir/build/BUILD/cvc4-1.3/builds/powerpc-redhat-linux-gnu/default-proof/../../../src/options/../theory/arith/options"
311 #line 82 "/builddir/build/BUILD/cvc4-1.3/builds/powerpc-redhat-linux-gnu/default-proof/../../../src/options/../theory/arith/options"
312 template <> void Options::assignBool(options::restrictedPivots__option_t, std::string option, bool value, SmtEngine* smt);
313 #line 85 "/builddir/build/BUILD/cvc4-1.3/builds/powerpc-redhat-linux-gnu/default-proof/../../../src/options/../theory/arith/options"
315 #line 85 "/builddir/build/BUILD/cvc4-1.3/builds/powerpc-redhat-linux-gnu/default-proof/../../../src/options/../theory/arith/options"
317 #line 85 "/builddir/build/BUILD/cvc4-1.3/builds/powerpc-redhat-linux-gnu/default-proof/../../../src/options/../theory/arith/options"
319 #line 85 "/builddir/build/BUILD/cvc4-1.3/builds/powerpc-redhat-linux-gnu/default-proof/../../../src/options/../theory/arith/options"
320 template <> void Options::assignBool(options::collectPivots__option_t, std::string option, bool value, SmtEngine* smt);
321 #line 88 "/builddir/build/BUILD/cvc4-1.3/builds/powerpc-redhat-linux-gnu/default-proof/../../../src/options/../theory/arith/options"
323 #line 88 "/builddir/build/BUILD/cvc4-1.3/builds/powerpc-redhat-linux-gnu/default-proof/../../../src/options/../theory/arith/options"
325 #line 88 "/builddir/build/BUILD/cvc4-1.3/builds/powerpc-redhat-linux-gnu/default-proof/../../../src/options/../theory/arith/options"
327 #line 88 "/builddir/build/BUILD/cvc4-1.3/builds/powerpc-redhat-linux-gnu/default-proof/../../../src/options/../theory/arith/options"
328 template <> void Options::assignBool(options::fancyFinal__option_t, std::string option, bool value, SmtEngine* smt);
329 #line 91 "/builddir/build/BUILD/cvc4-1.3/builds/powerpc-redhat-linux-gnu/default-proof/../../../src/options/../theory/arith/options"
331 #line 91 "/builddir/build/BUILD/cvc4-1.3/builds/powerpc-redhat-linux-gnu/default-proof/../../../src/options/../theory/arith/options"
333 #line 91 "/builddir/build/BUILD/cvc4-1.3/builds/powerpc-redhat-linux-gnu/default-proof/../../../src/options/../theory/arith/options"
335 #line 91 "/builddir/build/BUILD/cvc4-1.3/builds/powerpc-redhat-linux-gnu/default-proof/../../../src/options/../theory/arith/options"
336 template <> void Options::assignBool(options::exportDioDecompositions__option_t, std::string option, bool value, SmtEngine* smt);
337 #line 94 "/builddir/build/BUILD/cvc4-1.3/builds/powerpc-redhat-linux-gnu/default-proof/../../../src/options/../theory/arith/options"
339 #line 94 "/builddir/build/BUILD/cvc4-1.3/builds/powerpc-redhat-linux-gnu/default-proof/../../../src/options/../theory/arith/options"
341 #line 94 "/builddir/build/BUILD/cvc4-1.3/builds/powerpc-redhat-linux-gnu/default-proof/../../../src/options/../theory/arith/options"
342 template <> bool Options::wasSetByUser(options::newProp__option_t) const;
343 #line 94 "/builddir/build/BUILD/cvc4-1.3/builds/powerpc-redhat-linux-gnu/default-proof/../../../src/options/../theory/arith/options"
344 template <> void Options::assignBool(options::newProp__option_t, std::string option, bool value, SmtEngine* smt);
345 #line 97 "/builddir/build/BUILD/cvc4-1.3/builds/powerpc-redhat-linux-gnu/default-proof/../../../src/options/../theory/arith/options"
347 #line 97 "/builddir/build/BUILD/cvc4-1.3/builds/powerpc-redhat-linux-gnu/default-proof/../../../src/options/../theory/arith/options"
349 #line 97 "/builddir/build/BUILD/cvc4-1.3/builds/powerpc-redhat-linux-gnu/default-proof/../../../src/options/../theory/arith/options"
351 #line 97 "/builddir/build/BUILD/cvc4-1.3/builds/powerpc-redhat-linux-gnu/default-proof/../../../src/options/../theory/arith/options"
352 template <> void Options::assign(options::arithPropAsLemmaLength__option_t, std::string option, std::string value, SmtEngine* smt);
353 #line 100 "/builddir/build/BUILD/cvc4-1.3/builds/powerpc-redhat-linux-gnu/default-proof/../../../src/options/../theory/arith/options"
355 #line 100 "/builddir/build/BUILD/cvc4-1.3/builds/powerpc-redhat-linux-gnu/default-proof/../../../src/options/../theory/arith/options"
357 #line 100 "/builddir/build/BUILD/cvc4-1.3/builds/powerpc-redhat-linux-gnu/default-proof/../../../src/options/../theory/arith/options"
359 #line 100 "/builddir/build/BUILD/cvc4-1.3/builds/powerpc-redhat-linux-gnu/default-proof/../../../src/options/../theory/arith/options"
360 template <> void Options::assignBool(options::soiQuickExplain__option_t, std::string option, bool value, SmtEngine* smt);
361 #line 103 "/builddir/build/BUILD/cvc4-1.3/builds/powerpc-redhat-linux-gnu/default-proof/../../../src/options/../theory/arith/options"
363 #line 103 "/builddir/build/BUILD/cvc4-1.3/builds/powerpc-redhat-linux-gnu/default-proof/../../../src/options/../theory/arith/options"
365 #line 103 "/builddir/build/BUILD/cvc4-1.3/builds/powerpc-redhat-linux-gnu/default-proof/../../../src/options/../theory/arith/options"
366 template <> void Options::assignBool(options::rewriteDivk__option_t, std::string option, bool value, SmtEngine* smt);
367 
368 #line 44 "/builddir/build/BUILD/cvc4-1.3/builds/powerpc-redhat-linux-gnu/default-proof/../../../src/options/base_options_template.h"
369 
370 namespace options {
371 
372 
373 #line 8 "/builddir/build/BUILD/cvc4-1.3/builds/powerpc-redhat-linux-gnu/default-proof/../../../src/options/../theory/arith/options"
375 #line 8 "/builddir/build/BUILD/cvc4-1.3/builds/powerpc-redhat-linux-gnu/default-proof/../../../src/options/../theory/arith/options"
376 inline bool arithUnateLemmaMode__option_t::wasSetByUser() const { return Options::current().wasSetByUser(*this); }
377 
378 #line 11 "/builddir/build/BUILD/cvc4-1.3/builds/powerpc-redhat-linux-gnu/default-proof/../../../src/options/../theory/arith/options"
380 #line 11 "/builddir/build/BUILD/cvc4-1.3/builds/powerpc-redhat-linux-gnu/default-proof/../../../src/options/../theory/arith/options"
381 inline bool arithPropagationMode__option_t::wasSetByUser() const { return Options::current().wasSetByUser(*this); }
382 
383 #line 18 "/builddir/build/BUILD/cvc4-1.3/builds/powerpc-redhat-linux-gnu/default-proof/../../../src/options/../theory/arith/options"
385 #line 18 "/builddir/build/BUILD/cvc4-1.3/builds/powerpc-redhat-linux-gnu/default-proof/../../../src/options/../theory/arith/options"
386 inline bool arithHeuristicPivots__option_t::wasSetByUser() const { return Options::current().wasSetByUser(*this); }
387 #line 18 "/builddir/build/BUILD/cvc4-1.3/builds/powerpc-redhat-linux-gnu/default-proof/../../../src/options/../theory/arith/options"
389 
390 #line 25 "/builddir/build/BUILD/cvc4-1.3/builds/powerpc-redhat-linux-gnu/default-proof/../../../src/options/../theory/arith/options"
392 #line 25 "/builddir/build/BUILD/cvc4-1.3/builds/powerpc-redhat-linux-gnu/default-proof/../../../src/options/../theory/arith/options"
394 #line 25 "/builddir/build/BUILD/cvc4-1.3/builds/powerpc-redhat-linux-gnu/default-proof/../../../src/options/../theory/arith/options"
396 
397 #line 28 "/builddir/build/BUILD/cvc4-1.3/builds/powerpc-redhat-linux-gnu/default-proof/../../../src/options/../theory/arith/options"
399 #line 28 "/builddir/build/BUILD/cvc4-1.3/builds/powerpc-redhat-linux-gnu/default-proof/../../../src/options/../theory/arith/options"
401 
402 #line 32 "/builddir/build/BUILD/cvc4-1.3/builds/powerpc-redhat-linux-gnu/default-proof/../../../src/options/../theory/arith/options"
404 #line 32 "/builddir/build/BUILD/cvc4-1.3/builds/powerpc-redhat-linux-gnu/default-proof/../../../src/options/../theory/arith/options"
406 
407 #line 39 "/builddir/build/BUILD/cvc4-1.3/builds/powerpc-redhat-linux-gnu/default-proof/../../../src/options/../theory/arith/options"
409 #line 39 "/builddir/build/BUILD/cvc4-1.3/builds/powerpc-redhat-linux-gnu/default-proof/../../../src/options/../theory/arith/options"
410 inline bool arithPivotThreshold__option_t::wasSetByUser() const { return Options::current().wasSetByUser(*this); }
411 #line 39 "/builddir/build/BUILD/cvc4-1.3/builds/powerpc-redhat-linux-gnu/default-proof/../../../src/options/../theory/arith/options"
413 
414 #line 42 "/builddir/build/BUILD/cvc4-1.3/builds/powerpc-redhat-linux-gnu/default-proof/../../../src/options/../theory/arith/options"
416 #line 42 "/builddir/build/BUILD/cvc4-1.3/builds/powerpc-redhat-linux-gnu/default-proof/../../../src/options/../theory/arith/options"
418 
419 #line 45 "/builddir/build/BUILD/cvc4-1.3/builds/powerpc-redhat-linux-gnu/default-proof/../../../src/options/../theory/arith/options"
421 #line 45 "/builddir/build/BUILD/cvc4-1.3/builds/powerpc-redhat-linux-gnu/default-proof/../../../src/options/../theory/arith/options"
422 inline bool arithDioSolver__option_t::wasSetByUser() const { return Options::current().wasSetByUser(*this); }
423 
424 #line 50 "/builddir/build/BUILD/cvc4-1.3/builds/powerpc-redhat-linux-gnu/default-proof/../../../src/options/../theory/arith/options"
426 #line 50 "/builddir/build/BUILD/cvc4-1.3/builds/powerpc-redhat-linux-gnu/default-proof/../../../src/options/../theory/arith/options"
427 inline bool arithRewriteEq__option_t::wasSetByUser() const { return Options::current().wasSetByUser(*this); }
428 #line 50 "/builddir/build/BUILD/cvc4-1.3/builds/powerpc-redhat-linux-gnu/default-proof/../../../src/options/../theory/arith/options"
430 
431 #line 55 "/builddir/build/BUILD/cvc4-1.3/builds/powerpc-redhat-linux-gnu/default-proof/../../../src/options/../theory/arith/options"
433 #line 55 "/builddir/build/BUILD/cvc4-1.3/builds/powerpc-redhat-linux-gnu/default-proof/../../../src/options/../theory/arith/options"
434 inline bool arithMLTrick__option_t::wasSetByUser() const { return Options::current().wasSetByUser(*this); }
435 
436 #line 59 "/builddir/build/BUILD/cvc4-1.3/builds/powerpc-redhat-linux-gnu/default-proof/../../../src/options/../theory/arith/options"
438 #line 59 "/builddir/build/BUILD/cvc4-1.3/builds/powerpc-redhat-linux-gnu/default-proof/../../../src/options/../theory/arith/options"
440 
441 #line 62 "/builddir/build/BUILD/cvc4-1.3/builds/powerpc-redhat-linux-gnu/default-proof/../../../src/options/../theory/arith/options"
443 #line 62 "/builddir/build/BUILD/cvc4-1.3/builds/powerpc-redhat-linux-gnu/default-proof/../../../src/options/../theory/arith/options"
444 inline bool doCutAllBounded__option_t::wasSetByUser() const { return Options::current().wasSetByUser(*this); }
445 #line 62 "/builddir/build/BUILD/cvc4-1.3/builds/powerpc-redhat-linux-gnu/default-proof/../../../src/options/../theory/arith/options"
447 
448 #line 66 "/builddir/build/BUILD/cvc4-1.3/builds/powerpc-redhat-linux-gnu/default-proof/../../../src/options/../theory/arith/options"
450 #line 66 "/builddir/build/BUILD/cvc4-1.3/builds/powerpc-redhat-linux-gnu/default-proof/../../../src/options/../theory/arith/options"
451 inline bool maxCutsInContext__option_t::wasSetByUser() const { return Options::current().wasSetByUser(*this); }
452 
453 #line 69 "/builddir/build/BUILD/cvc4-1.3/builds/powerpc-redhat-linux-gnu/default-proof/../../../src/options/../theory/arith/options"
455 #line 69 "/builddir/build/BUILD/cvc4-1.3/builds/powerpc-redhat-linux-gnu/default-proof/../../../src/options/../theory/arith/options"
456 inline bool revertArithModels__option_t::wasSetByUser() const { return Options::current().wasSetByUser(*this); }
457 
458 #line 72 "/builddir/build/BUILD/cvc4-1.3/builds/powerpc-redhat-linux-gnu/default-proof/../../../src/options/../theory/arith/options"
460 #line 72 "/builddir/build/BUILD/cvc4-1.3/builds/powerpc-redhat-linux-gnu/default-proof/../../../src/options/../theory/arith/options"
461 inline bool havePenalties__option_t::wasSetByUser() const { return Options::current().wasSetByUser(*this); }
462 #line 72 "/builddir/build/BUILD/cvc4-1.3/builds/powerpc-redhat-linux-gnu/default-proof/../../../src/options/../theory/arith/options"
464 
465 #line 76 "/builddir/build/BUILD/cvc4-1.3/builds/powerpc-redhat-linux-gnu/default-proof/../../../src/options/../theory/arith/options"
466 inline useFC__option_t::type useFC__option_t::operator()() const { return Options::current()[*this]; }
467 #line 76 "/builddir/build/BUILD/cvc4-1.3/builds/powerpc-redhat-linux-gnu/default-proof/../../../src/options/../theory/arith/options"
468 inline bool useFC__option_t::wasSetByUser() const { return Options::current().wasSetByUser(*this); }
469 #line 76 "/builddir/build/BUILD/cvc4-1.3/builds/powerpc-redhat-linux-gnu/default-proof/../../../src/options/../theory/arith/options"
470 inline void useFC__option_t::set(const useFC__option_t::type& v) { Options::current().set(*this, v); }
471 
472 #line 79 "/builddir/build/BUILD/cvc4-1.3/builds/powerpc-redhat-linux-gnu/default-proof/../../../src/options/../theory/arith/options"
473 inline useSOI__option_t::type useSOI__option_t::operator()() const { return Options::current()[*this]; }
474 #line 79 "/builddir/build/BUILD/cvc4-1.3/builds/powerpc-redhat-linux-gnu/default-proof/../../../src/options/../theory/arith/options"
475 inline bool useSOI__option_t::wasSetByUser() const { return Options::current().wasSetByUser(*this); }
476 #line 79 "/builddir/build/BUILD/cvc4-1.3/builds/powerpc-redhat-linux-gnu/default-proof/../../../src/options/../theory/arith/options"
477 inline void useSOI__option_t::set(const useSOI__option_t::type& v) { Options::current().set(*this, v); }
478 
479 #line 82 "/builddir/build/BUILD/cvc4-1.3/builds/powerpc-redhat-linux-gnu/default-proof/../../../src/options/../theory/arith/options"
481 #line 82 "/builddir/build/BUILD/cvc4-1.3/builds/powerpc-redhat-linux-gnu/default-proof/../../../src/options/../theory/arith/options"
482 inline bool restrictedPivots__option_t::wasSetByUser() const { return Options::current().wasSetByUser(*this); }
483 #line 82 "/builddir/build/BUILD/cvc4-1.3/builds/powerpc-redhat-linux-gnu/default-proof/../../../src/options/../theory/arith/options"
485 
486 #line 85 "/builddir/build/BUILD/cvc4-1.3/builds/powerpc-redhat-linux-gnu/default-proof/../../../src/options/../theory/arith/options"
488 #line 85 "/builddir/build/BUILD/cvc4-1.3/builds/powerpc-redhat-linux-gnu/default-proof/../../../src/options/../theory/arith/options"
489 inline bool collectPivots__option_t::wasSetByUser() const { return Options::current().wasSetByUser(*this); }
490 #line 85 "/builddir/build/BUILD/cvc4-1.3/builds/powerpc-redhat-linux-gnu/default-proof/../../../src/options/../theory/arith/options"
492 
493 #line 88 "/builddir/build/BUILD/cvc4-1.3/builds/powerpc-redhat-linux-gnu/default-proof/../../../src/options/../theory/arith/options"
495 #line 88 "/builddir/build/BUILD/cvc4-1.3/builds/powerpc-redhat-linux-gnu/default-proof/../../../src/options/../theory/arith/options"
496 inline bool fancyFinal__option_t::wasSetByUser() const { return Options::current().wasSetByUser(*this); }
497 #line 88 "/builddir/build/BUILD/cvc4-1.3/builds/powerpc-redhat-linux-gnu/default-proof/../../../src/options/../theory/arith/options"
498 inline void fancyFinal__option_t::set(const fancyFinal__option_t::type& v) { Options::current().set(*this, v); }
499 
500 #line 91 "/builddir/build/BUILD/cvc4-1.3/builds/powerpc-redhat-linux-gnu/default-proof/../../../src/options/../theory/arith/options"
502 #line 91 "/builddir/build/BUILD/cvc4-1.3/builds/powerpc-redhat-linux-gnu/default-proof/../../../src/options/../theory/arith/options"
504 #line 91 "/builddir/build/BUILD/cvc4-1.3/builds/powerpc-redhat-linux-gnu/default-proof/../../../src/options/../theory/arith/options"
506 
507 #line 94 "/builddir/build/BUILD/cvc4-1.3/builds/powerpc-redhat-linux-gnu/default-proof/../../../src/options/../theory/arith/options"
509 #line 94 "/builddir/build/BUILD/cvc4-1.3/builds/powerpc-redhat-linux-gnu/default-proof/../../../src/options/../theory/arith/options"
510 inline bool newProp__option_t::wasSetByUser() const { return Options::current().wasSetByUser(*this); }
511 #line 94 "/builddir/build/BUILD/cvc4-1.3/builds/powerpc-redhat-linux-gnu/default-proof/../../../src/options/../theory/arith/options"
512 inline void newProp__option_t::set(const newProp__option_t::type& v) { Options::current().set(*this, v); }
513 
514 #line 97 "/builddir/build/BUILD/cvc4-1.3/builds/powerpc-redhat-linux-gnu/default-proof/../../../src/options/../theory/arith/options"
516 #line 97 "/builddir/build/BUILD/cvc4-1.3/builds/powerpc-redhat-linux-gnu/default-proof/../../../src/options/../theory/arith/options"
518 #line 97 "/builddir/build/BUILD/cvc4-1.3/builds/powerpc-redhat-linux-gnu/default-proof/../../../src/options/../theory/arith/options"
520 
521 #line 100 "/builddir/build/BUILD/cvc4-1.3/builds/powerpc-redhat-linux-gnu/default-proof/../../../src/options/../theory/arith/options"
523 #line 100 "/builddir/build/BUILD/cvc4-1.3/builds/powerpc-redhat-linux-gnu/default-proof/../../../src/options/../theory/arith/options"
524 inline bool soiQuickExplain__option_t::wasSetByUser() const { return Options::current().wasSetByUser(*this); }
525 #line 100 "/builddir/build/BUILD/cvc4-1.3/builds/powerpc-redhat-linux-gnu/default-proof/../../../src/options/../theory/arith/options"
527 
528 #line 103 "/builddir/build/BUILD/cvc4-1.3/builds/powerpc-redhat-linux-gnu/default-proof/../../../src/options/../theory/arith/options"
530 #line 103 "/builddir/build/BUILD/cvc4-1.3/builds/powerpc-redhat-linux-gnu/default-proof/../../../src/options/../theory/arith/options"
531 inline bool rewriteDivk__option_t::wasSetByUser() const { return Options::current().wasSetByUser(*this); }
532 
533 #line 50 "/builddir/build/BUILD/cvc4-1.3/builds/powerpc-redhat-linux-gnu/default-proof/../../../src/options/base_options_template.h"
534 
535 }/* CVC4::options namespace */
536 
537 }/* CVC4 namespace */
538 
539 #endif /* __CVC4__OPTIONS__ARITH_H */
struct CVC4::options::maxCutsInContext__option_t maxCutsInContext
[[ Add one-line brief description here ]]
struct CVC4::options::arithDioSolver__option_t arithDioSolver
struct CVC4::options::arithMLTrickSubstitutions__option_t arithMLTrickSubstitutions
const T::type & operator[](T) const
Get the value of the given option.
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::arithErrorSelectionRule__option_t arithErrorSelectionRule
struct CVC4::options::arithRewriteEq__option_t arithRewriteEq
struct CVC4::options::collectPivots__option_t collectPivots
This is CVC4 release version For build and installation please see the INSTALL file included with this distribution This first official release of CVC4 is the result of more than three years of efforts by researchers at New York University and The University of Iowa The project leaders are Clark please refer to the AUTHORS file in the source distribution CVC4 is a tool for determining the satisfiability of a first order formula modulo a first order CVC CVC3 but does not directly incorporate code from any previous version CVC4 is intended to be an open and extensible SMT engine It can be used as a stand alone tool or as a library It has been designed to increase the performance and reduce the memory overhead of its predecessors It is written entirely in C and is released under a free software see the INSTALL file that comes with this distribution We recommend that you visit our CVC4 tutorials online please write to the cvc users cs nyu edu mailing list *if you need to report a bug with CVC4
Definition: README:39
struct CVC4::options::exportDioDecompositions__option_t exportDioDecompositions
[[ Add one-line brief description here ]]
struct CVC4::options::arithHeuristicPivots__option_t arithHeuristicPivots
struct CVC4::options::arithSimplexCheckPeriod__option_t arithSimplexCheckPeriod
struct CVC4::options::soiQuickExplain__option_t soiQuickExplain
#define CVC4_PUBLIC
Definition: cvc4_public.h:30
void set(const type &v)
Definition: options.h:477
void set(const type &v)
Definition: options.h:470
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::arithMLTrick__option_t arithMLTrick
void set(const type &v)
Definition: options.h:512
struct CVC4::options::arithPropagateMaxLength__option_t arithPropagateMaxLength
struct CVC4::options::doCutAllBounded__option_t doCutAllBounded
[[ Add one-line brief description here ]]
struct CVC4::options::arithPropagationMode__option_t arithPropagationMode
struct CVC4::options::fancyFinal__option_t fancyFinal
struct CVC4::options::arithPropAsLemmaLength__option_t arithPropAsLemmaLength
struct CVC4::options::arithUnateLemmaMode__option_t arithUnateLemmaMode
struct CVC4::options::rewriteDivk__option_t rewriteDivk
struct CVC4::options::arithPivotThreshold__option_t arithPivotThreshold
struct CVC4::options::newProp__option_t newProp
struct CVC4::options::useFC__option_t useFC
void set(T, const typename T::type &)
Set the value of the given option.
Definition: options.h:78
struct CVC4::options::revertArithModels__option_t revertArithModels
struct CVC4::options::useSOI__option_t useSOI
struct CVC4::options::havePenalties__option_t havePenalties
Global (command-line, set-option, ...) parameters for SMT.
struct CVC4::options::arithStandardCheckVarOrderPivots__option_t arithStandardCheckVarOrderPivots
bool wasSetByUser() const
Definition: options.h:468
struct CVC4::options::restrictedPivots__option_t restrictedPivots