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__ARITH_H
49 #define __CVC4__OPTIONS__ARITH_H
50 
51 #include "options/options.h"
52 
53 #line 8 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/arith/options"
55 #line 11 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/arith/options"
57 #line 28 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/arith/options"
59 
60 #line 26 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../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  useApprox__option_t::type useApprox; \
104  bool useApprox__setByUser__; \
105  maxApproxDepth__option_t::type maxApproxDepth; \
106  bool maxApproxDepth__setByUser__; \
107  exportDioDecompositions__option_t::type exportDioDecompositions; \
108  bool exportDioDecompositions__setByUser__; \
109  newProp__option_t::type newProp; \
110  bool newProp__setByUser__; \
111  arithPropAsLemmaLength__option_t::type arithPropAsLemmaLength; \
112  bool arithPropAsLemmaLength__setByUser__; \
113  soiQuickExplain__option_t::type soiQuickExplain; \
114  bool soiQuickExplain__setByUser__; \
115  rewriteDivk__option_t::type rewriteDivk; \
116  bool rewriteDivk__setByUser__; \
117  trySolveIntStandardEffort__option_t::type trySolveIntStandardEffort; \
118  bool trySolveIntStandardEffort__setByUser__; \
119  replayFailureLemma__option_t::type replayFailureLemma; \
120  bool replayFailureLemma__setByUser__; \
121  dioSolverTurns__option_t::type dioSolverTurns; \
122  bool dioSolverTurns__setByUser__; \
123  rrTurns__option_t::type rrTurns; \
124  bool rrTurns__setByUser__; \
125  dioRepeat__option_t::type dioRepeat; \
126  bool dioRepeat__setByUser__; \
127  replayEarlyCloseDepths__option_t::type replayEarlyCloseDepths; \
128  bool replayEarlyCloseDepths__setByUser__; \
129  replayFailurePenalty__option_t::type replayFailurePenalty; \
130  bool replayFailurePenalty__setByUser__; \
131  replayNumericFailurePenalty__option_t::type replayNumericFailurePenalty; \
132  bool replayNumericFailurePenalty__setByUser__; \
133  replayRejectCutSize__option_t::type replayRejectCutSize; \
134  bool replayRejectCutSize__setByUser__; \
135  lemmaRejectCutSize__option_t::type lemmaRejectCutSize; \
136  bool lemmaRejectCutSize__setByUser__; \
137  soiApproxMajorFailure__option_t::type soiApproxMajorFailure; \
138  bool soiApproxMajorFailure__setByUser__; \
139  soiApproxMajorFailurePen__option_t::type soiApproxMajorFailurePen; \
140  bool soiApproxMajorFailurePen__setByUser__; \
141  soiApproxMinorFailure__option_t::type soiApproxMinorFailure; \
142  bool soiApproxMinorFailure__setByUser__; \
143  soiApproxMinorFailurePen__option_t::type soiApproxMinorFailurePen; \
144  bool soiApproxMinorFailurePen__setByUser__; \
145  ppAssertMaxSubSize__option_t::type ppAssertMaxSubSize; \
146  bool ppAssertMaxSubSize__setByUser__; \
147  maxReplayTree__option_t::type maxReplayTree; \
148  bool maxReplayTree__setByUser__; \
149  pbRewrites__option_t::type pbRewrites; \
150  bool pbRewrites__setByUser__; \
151  pbRewriteThreshold__option_t::type pbRewriteThreshold; \
152  bool pbRewriteThreshold__setByUser__;
153 
154 #line 30 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/base_options_template.h"
155 
156 namespace CVC4 {
157 
158 namespace options {
159 
160 
161 #line 8 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/arith/options"
162 extern struct CVC4_PUBLIC arithUnateLemmaMode__option_t { typedef ArithUnateLemmaMode type; type operator()() const; bool wasSetByUser() const; } arithUnateLemmaMode CVC4_PUBLIC;
163 #line 11 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/arith/options"
164 extern struct CVC4_PUBLIC arithPropagationMode__option_t { typedef ArithPropagationMode type; type operator()() const; bool wasSetByUser() const; } arithPropagationMode CVC4_PUBLIC;
165 #line 18 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/arith/options"
166 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;
167 #line 25 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/arith/options"
168 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;
169 #line 28 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/arith/options"
170 extern struct CVC4_PUBLIC arithErrorSelectionRule__option_t { typedef ErrorSelectionRule type; type operator()() const; bool wasSetByUser() const; } arithErrorSelectionRule CVC4_PUBLIC;
171 #line 32 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/arith/options"
172 extern struct CVC4_PUBLIC arithSimplexCheckPeriod__option_t { typedef uint16_t type; type operator()() const; bool wasSetByUser() const; } arithSimplexCheckPeriod CVC4_PUBLIC;
173 #line 39 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/arith/options"
174 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;
175 #line 42 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/arith/options"
176 extern struct CVC4_PUBLIC arithPropagateMaxLength__option_t { typedef uint16_t type; type operator()() const; bool wasSetByUser() const; } arithPropagateMaxLength CVC4_PUBLIC;
177 #line 45 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/arith/options"
178 extern struct CVC4_PUBLIC arithDioSolver__option_t { typedef bool type; type operator()() const; bool wasSetByUser() const; } arithDioSolver CVC4_PUBLIC;
179 #line 50 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/arith/options"
180 extern struct CVC4_PUBLIC arithRewriteEq__option_t { typedef bool type; type operator()() const; bool wasSetByUser() const; void set(const type& v); } arithRewriteEq CVC4_PUBLIC;
181 #line 55 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/arith/options"
182 extern struct CVC4_PUBLIC arithMLTrick__option_t { typedef bool type; type operator()() const; bool wasSetByUser() const; } arithMLTrick CVC4_PUBLIC;
183 #line 59 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/arith/options"
184 extern struct CVC4_PUBLIC arithMLTrickSubstitutions__option_t { typedef unsigned type; type operator()() const; bool wasSetByUser() const; } arithMLTrickSubstitutions CVC4_PUBLIC;
185 #line 62 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/arith/options"
186 extern struct CVC4_PUBLIC doCutAllBounded__option_t { typedef bool type; type operator()() const; bool wasSetByUser() const; void set(const type& v); } doCutAllBounded CVC4_PUBLIC;
187 #line 66 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/arith/options"
188 extern struct CVC4_PUBLIC maxCutsInContext__option_t { typedef unsigned type; type operator()() const; bool wasSetByUser() const; } maxCutsInContext CVC4_PUBLIC;
189 #line 69 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/arith/options"
190 extern struct CVC4_PUBLIC revertArithModels__option_t { typedef bool type; type operator()() const; bool wasSetByUser() const; } revertArithModels CVC4_PUBLIC;
191 #line 72 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/arith/options"
192 extern struct CVC4_PUBLIC havePenalties__option_t { typedef bool type; type operator()() const; bool wasSetByUser() const; void set(const type& v); } havePenalties CVC4_PUBLIC;
193 #line 76 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/arith/options"
194 extern struct CVC4_PUBLIC useFC__option_t { typedef bool type; type operator()() const; bool wasSetByUser() const; void set(const type& v); } useFC CVC4_PUBLIC;
195 #line 79 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/arith/options"
196 extern struct CVC4_PUBLIC useSOI__option_t { typedef bool type; type operator()() const; bool wasSetByUser() const; void set(const type& v); } useSOI CVC4_PUBLIC;
197 #line 82 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/arith/options"
198 extern struct CVC4_PUBLIC restrictedPivots__option_t { typedef bool type; type operator()() const; bool wasSetByUser() const; void set(const type& v); } restrictedPivots CVC4_PUBLIC;
199 #line 85 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/arith/options"
200 extern struct CVC4_PUBLIC collectPivots__option_t { typedef bool type; type operator()() const; bool wasSetByUser() const; void set(const type& v); } collectPivots CVC4_PUBLIC;
201 #line 88 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/arith/options"
202 extern struct CVC4_PUBLIC useApprox__option_t { typedef bool type; type operator()() const; bool wasSetByUser() const; void set(const type& v); } useApprox CVC4_PUBLIC;
203 #line 91 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/arith/options"
204 extern struct CVC4_PUBLIC maxApproxDepth__option_t { typedef int16_t type; type operator()() const; bool wasSetByUser() const; void set(const type& v); } maxApproxDepth CVC4_PUBLIC;
205 #line 94 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/arith/options"
206 extern struct CVC4_PUBLIC exportDioDecompositions__option_t { typedef bool type; type operator()() const; bool wasSetByUser() const; void set(const type& v); } exportDioDecompositions CVC4_PUBLIC;
207 #line 97 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/arith/options"
208 extern struct CVC4_PUBLIC newProp__option_t { typedef bool type; type operator()() const; bool wasSetByUser() const; void set(const type& v); } newProp CVC4_PUBLIC;
209 #line 100 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/arith/options"
210 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;
211 #line 103 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/arith/options"
212 extern struct CVC4_PUBLIC soiQuickExplain__option_t { typedef bool type; type operator()() const; bool wasSetByUser() const; void set(const type& v); } soiQuickExplain CVC4_PUBLIC;
213 #line 106 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/arith/options"
214 extern struct CVC4_PUBLIC rewriteDivk__option_t { typedef bool type; type operator()() const; bool wasSetByUser() const; void set(const type& v); } rewriteDivk CVC4_PUBLIC;
215 #line 109 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/arith/options"
216 extern struct CVC4_PUBLIC trySolveIntStandardEffort__option_t { typedef bool type; type operator()() const; bool wasSetByUser() const; } trySolveIntStandardEffort CVC4_PUBLIC;
217 #line 112 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/arith/options"
218 extern struct CVC4_PUBLIC replayFailureLemma__option_t { typedef bool type; type operator()() const; bool wasSetByUser() const; } replayFailureLemma CVC4_PUBLIC;
219 #line 115 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/arith/options"
220 extern struct CVC4_PUBLIC dioSolverTurns__option_t { typedef int type; type operator()() const; bool wasSetByUser() const; } dioSolverTurns CVC4_PUBLIC;
221 #line 118 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/arith/options"
222 extern struct CVC4_PUBLIC rrTurns__option_t { typedef int type; type operator()() const; bool wasSetByUser() const; } rrTurns CVC4_PUBLIC;
223 #line 121 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/arith/options"
224 extern struct CVC4_PUBLIC dioRepeat__option_t { typedef bool type; type operator()() const; bool wasSetByUser() const; } dioRepeat CVC4_PUBLIC;
225 #line 124 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/arith/options"
226 extern struct CVC4_PUBLIC replayEarlyCloseDepths__option_t { typedef int type; type operator()() const; bool wasSetByUser() const; } replayEarlyCloseDepths CVC4_PUBLIC;
227 #line 127 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/arith/options"
228 extern struct CVC4_PUBLIC replayFailurePenalty__option_t { typedef int type; type operator()() const; bool wasSetByUser() const; } replayFailurePenalty CVC4_PUBLIC;
229 #line 130 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/arith/options"
230 extern struct CVC4_PUBLIC replayNumericFailurePenalty__option_t { typedef int type; type operator()() const; bool wasSetByUser() const; } replayNumericFailurePenalty CVC4_PUBLIC;
231 #line 133 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/arith/options"
232 extern struct CVC4_PUBLIC replayRejectCutSize__option_t { typedef unsigned type; type operator()() const; bool wasSetByUser() const; } replayRejectCutSize CVC4_PUBLIC;
233 #line 136 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/arith/options"
234 extern struct CVC4_PUBLIC lemmaRejectCutSize__option_t { typedef unsigned type; type operator()() const; bool wasSetByUser() const; } lemmaRejectCutSize CVC4_PUBLIC;
235 #line 139 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/arith/options"
236 extern struct CVC4_PUBLIC soiApproxMajorFailure__option_t { typedef double type; type operator()() const; bool wasSetByUser() const; } soiApproxMajorFailure CVC4_PUBLIC;
237 #line 142 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/arith/options"
238 extern struct CVC4_PUBLIC soiApproxMajorFailurePen__option_t { typedef int type; type operator()() const; bool wasSetByUser() const; } soiApproxMajorFailurePen CVC4_PUBLIC;
239 #line 145 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/arith/options"
240 extern struct CVC4_PUBLIC soiApproxMinorFailure__option_t { typedef double type; type operator()() const; bool wasSetByUser() const; } soiApproxMinorFailure CVC4_PUBLIC;
241 #line 148 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/arith/options"
242 extern struct CVC4_PUBLIC soiApproxMinorFailurePen__option_t { typedef int type; type operator()() const; bool wasSetByUser() const; } soiApproxMinorFailurePen CVC4_PUBLIC;
243 #line 151 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/arith/options"
244 extern struct CVC4_PUBLIC ppAssertMaxSubSize__option_t { typedef unsigned type; type operator()() const; bool wasSetByUser() const; } ppAssertMaxSubSize CVC4_PUBLIC;
245 #line 154 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/arith/options"
246 extern struct CVC4_PUBLIC maxReplayTree__option_t { typedef int type; type operator()() const; bool wasSetByUser() const; } maxReplayTree CVC4_PUBLIC;
247 #line 158 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/arith/options"
248 extern struct CVC4_PUBLIC pbRewrites__option_t { typedef bool type; type operator()() const; bool wasSetByUser() const; } pbRewrites CVC4_PUBLIC;
249 #line 161 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/arith/options"
250 extern struct CVC4_PUBLIC pbRewriteThreshold__option_t { typedef int type; type operator()() const; bool wasSetByUser() const; } pbRewriteThreshold CVC4_PUBLIC;
251 
252 #line 38 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/base_options_template.h"
253 
254 }/* CVC4::options namespace */
255 
256 
257 #line 8 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/arith/options"
259 #line 8 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/arith/options"
261 #line 8 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/arith/options"
262 template <> void Options::assign(options::arithUnateLemmaMode__option_t, std::string option, std::string value, SmtEngine* smt);
263 #line 11 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/arith/options"
265 #line 11 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/arith/options"
267 #line 11 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/arith/options"
268 template <> void Options::assign(options::arithPropagationMode__option_t, std::string option, std::string value, SmtEngine* smt);
269 #line 18 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/arith/options"
271 #line 18 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/arith/options"
273 #line 18 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/arith/options"
275 #line 18 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/arith/options"
276 template <> void Options::assign(options::arithHeuristicPivots__option_t, std::string option, std::string value, SmtEngine* smt);
277 #line 25 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/arith/options"
279 #line 25 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/arith/options"
281 #line 25 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/arith/options"
283 #line 25 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/arith/options"
284 template <> void Options::assign(options::arithStandardCheckVarOrderPivots__option_t, std::string option, std::string value, SmtEngine* smt);
285 #line 28 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/arith/options"
287 #line 28 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/arith/options"
289 #line 28 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/arith/options"
290 template <> void Options::assign(options::arithErrorSelectionRule__option_t, std::string option, std::string value, SmtEngine* smt);
291 #line 32 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/arith/options"
293 #line 32 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/arith/options"
295 #line 32 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/arith/options"
296 template <> void Options::assign(options::arithSimplexCheckPeriod__option_t, std::string option, std::string value, SmtEngine* smt);
297 #line 39 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/arith/options"
299 #line 39 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/arith/options"
301 #line 39 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/arith/options"
303 #line 39 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/arith/options"
304 template <> void Options::assign(options::arithPivotThreshold__option_t, std::string option, std::string value, SmtEngine* smt);
305 #line 42 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/arith/options"
307 #line 42 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/arith/options"
309 #line 42 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/arith/options"
310 template <> void Options::assign(options::arithPropagateMaxLength__option_t, std::string option, std::string value, SmtEngine* smt);
311 #line 45 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/arith/options"
313 #line 45 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/arith/options"
315 #line 45 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/arith/options"
316 template <> void Options::assignBool(options::arithDioSolver__option_t, std::string option, bool value, SmtEngine* smt);
317 #line 50 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/arith/options"
319 #line 50 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/arith/options"
321 #line 50 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/arith/options"
323 #line 50 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/arith/options"
324 template <> void Options::assignBool(options::arithRewriteEq__option_t, std::string option, bool value, SmtEngine* smt);
325 #line 55 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/arith/options"
327 #line 55 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/arith/options"
329 #line 55 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/arith/options"
330 template <> void Options::assignBool(options::arithMLTrick__option_t, std::string option, bool value, SmtEngine* smt);
331 #line 59 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/arith/options"
333 #line 59 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/arith/options"
335 #line 59 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/arith/options"
336 template <> void Options::assign(options::arithMLTrickSubstitutions__option_t, std::string option, std::string value, SmtEngine* smt);
337 #line 62 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/arith/options"
339 #line 62 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/arith/options"
341 #line 62 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/arith/options"
343 #line 62 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/arith/options"
344 template <> void Options::assignBool(options::doCutAllBounded__option_t, std::string option, bool value, SmtEngine* smt);
345 #line 66 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/arith/options"
347 #line 66 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/arith/options"
349 #line 66 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/arith/options"
350 template <> void Options::assign(options::maxCutsInContext__option_t, std::string option, std::string value, SmtEngine* smt);
351 #line 69 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/arith/options"
353 #line 69 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/arith/options"
355 #line 69 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/arith/options"
356 template <> void Options::assignBool(options::revertArithModels__option_t, std::string option, bool value, SmtEngine* smt);
357 #line 72 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/arith/options"
359 #line 72 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/arith/options"
361 #line 72 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/arith/options"
363 #line 72 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/arith/options"
364 template <> void Options::assignBool(options::havePenalties__option_t, std::string option, bool value, SmtEngine* smt);
365 #line 76 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/arith/options"
367 #line 76 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/arith/options"
369 #line 76 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/arith/options"
370 template <> bool Options::wasSetByUser(options::useFC__option_t) const;
371 #line 76 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/arith/options"
372 template <> void Options::assignBool(options::useFC__option_t, std::string option, bool value, SmtEngine* smt);
373 #line 79 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/arith/options"
375 #line 79 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/arith/options"
377 #line 79 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/arith/options"
378 template <> bool Options::wasSetByUser(options::useSOI__option_t) const;
379 #line 79 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/arith/options"
380 template <> void Options::assignBool(options::useSOI__option_t, std::string option, bool value, SmtEngine* smt);
381 #line 82 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/arith/options"
383 #line 82 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/arith/options"
385 #line 82 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/arith/options"
387 #line 82 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/arith/options"
388 template <> void Options::assignBool(options::restrictedPivots__option_t, std::string option, bool value, SmtEngine* smt);
389 #line 85 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/arith/options"
391 #line 85 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/arith/options"
393 #line 85 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/arith/options"
395 #line 85 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/arith/options"
396 template <> void Options::assignBool(options::collectPivots__option_t, std::string option, bool value, SmtEngine* smt);
397 #line 88 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/arith/options"
399 #line 88 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/arith/options"
401 #line 88 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/arith/options"
403 #line 88 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/arith/options"
404 template <> void Options::assignBool(options::useApprox__option_t, std::string option, bool value, SmtEngine* smt);
405 #line 91 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/arith/options"
407 #line 91 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/arith/options"
409 #line 91 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/arith/options"
411 #line 91 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/arith/options"
412 template <> void Options::assign(options::maxApproxDepth__option_t, std::string option, std::string value, SmtEngine* smt);
413 #line 94 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/arith/options"
415 #line 94 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/arith/options"
417 #line 94 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/arith/options"
419 #line 94 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/arith/options"
420 template <> void Options::assignBool(options::exportDioDecompositions__option_t, std::string option, bool value, SmtEngine* smt);
421 #line 97 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/arith/options"
423 #line 97 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/arith/options"
425 #line 97 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/arith/options"
426 template <> bool Options::wasSetByUser(options::newProp__option_t) const;
427 #line 97 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/arith/options"
428 template <> void Options::assignBool(options::newProp__option_t, std::string option, bool value, SmtEngine* smt);
429 #line 100 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/arith/options"
431 #line 100 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/arith/options"
433 #line 100 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/arith/options"
435 #line 100 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/arith/options"
436 template <> void Options::assign(options::arithPropAsLemmaLength__option_t, std::string option, std::string value, SmtEngine* smt);
437 #line 103 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/arith/options"
439 #line 103 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/arith/options"
441 #line 103 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/arith/options"
443 #line 103 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/arith/options"
444 template <> void Options::assignBool(options::soiQuickExplain__option_t, std::string option, bool value, SmtEngine* smt);
445 #line 106 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/arith/options"
447 #line 106 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/arith/options"
449 #line 106 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/arith/options"
451 #line 106 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/arith/options"
452 template <> void Options::assignBool(options::rewriteDivk__option_t, std::string option, bool value, SmtEngine* smt);
453 #line 109 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/arith/options"
455 #line 109 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/arith/options"
457 #line 109 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/arith/options"
458 template <> void Options::assignBool(options::trySolveIntStandardEffort__option_t, std::string option, bool value, SmtEngine* smt);
459 #line 112 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/arith/options"
461 #line 112 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/arith/options"
463 #line 112 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/arith/options"
464 template <> void Options::assignBool(options::replayFailureLemma__option_t, std::string option, bool value, SmtEngine* smt);
465 #line 115 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/arith/options"
467 #line 115 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/arith/options"
469 #line 115 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/arith/options"
470 template <> void Options::assign(options::dioSolverTurns__option_t, std::string option, std::string value, SmtEngine* smt);
471 #line 118 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/arith/options"
473 #line 118 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/arith/options"
474 template <> bool Options::wasSetByUser(options::rrTurns__option_t) const;
475 #line 118 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/arith/options"
476 template <> void Options::assign(options::rrTurns__option_t, std::string option, std::string value, SmtEngine* smt);
477 #line 121 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/arith/options"
479 #line 121 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/arith/options"
481 #line 121 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/arith/options"
482 template <> void Options::assignBool(options::dioRepeat__option_t, std::string option, bool value, SmtEngine* smt);
483 #line 124 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/arith/options"
485 #line 124 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/arith/options"
487 #line 124 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/arith/options"
488 template <> void Options::assign(options::replayEarlyCloseDepths__option_t, std::string option, std::string value, SmtEngine* smt);
489 #line 127 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/arith/options"
491 #line 127 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/arith/options"
493 #line 127 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/arith/options"
494 template <> void Options::assign(options::replayFailurePenalty__option_t, std::string option, std::string value, SmtEngine* smt);
495 #line 130 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/arith/options"
497 #line 130 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/arith/options"
499 #line 130 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/arith/options"
500 template <> void Options::assign(options::replayNumericFailurePenalty__option_t, std::string option, std::string value, SmtEngine* smt);
501 #line 133 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/arith/options"
503 #line 133 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/arith/options"
505 #line 133 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/arith/options"
506 template <> void Options::assign(options::replayRejectCutSize__option_t, std::string option, std::string value, SmtEngine* smt);
507 #line 136 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/arith/options"
509 #line 136 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/arith/options"
511 #line 136 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/arith/options"
512 template <> void Options::assign(options::lemmaRejectCutSize__option_t, std::string option, std::string value, SmtEngine* smt);
513 #line 139 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/arith/options"
515 #line 139 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/arith/options"
517 #line 139 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/arith/options"
518 template <> void Options::assign(options::soiApproxMajorFailure__option_t, std::string option, std::string value, SmtEngine* smt);
519 #line 142 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/arith/options"
521 #line 142 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/arith/options"
523 #line 142 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/arith/options"
524 template <> void Options::assign(options::soiApproxMajorFailurePen__option_t, std::string option, std::string value, SmtEngine* smt);
525 #line 145 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/arith/options"
527 #line 145 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/arith/options"
529 #line 145 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/arith/options"
530 template <> void Options::assign(options::soiApproxMinorFailure__option_t, std::string option, std::string value, SmtEngine* smt);
531 #line 148 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/arith/options"
533 #line 148 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/arith/options"
535 #line 148 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/arith/options"
536 template <> void Options::assign(options::soiApproxMinorFailurePen__option_t, std::string option, std::string value, SmtEngine* smt);
537 #line 151 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/arith/options"
539 #line 151 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/arith/options"
541 #line 151 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/arith/options"
542 template <> void Options::assign(options::ppAssertMaxSubSize__option_t, std::string option, std::string value, SmtEngine* smt);
543 #line 154 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/arith/options"
545 #line 154 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/arith/options"
547 #line 154 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/arith/options"
548 template <> void Options::assign(options::maxReplayTree__option_t, std::string option, std::string value, SmtEngine* smt);
549 #line 158 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/arith/options"
551 #line 158 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/arith/options"
553 #line 158 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/arith/options"
554 template <> void Options::assignBool(options::pbRewrites__option_t, std::string option, bool value, SmtEngine* smt);
555 #line 161 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/arith/options"
557 #line 161 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/arith/options"
559 #line 161 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/arith/options"
560 template <> void Options::assign(options::pbRewriteThreshold__option_t, std::string option, std::string value, SmtEngine* smt);
561 
562 #line 44 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/base_options_template.h"
563 
564 namespace options {
565 
566 
567 #line 8 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/arith/options"
569 #line 8 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/arith/options"
571 
572 #line 11 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/arith/options"
574 #line 11 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/arith/options"
576 
577 #line 18 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/arith/options"
579 #line 18 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/arith/options"
581 #line 18 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/arith/options"
583 
584 #line 25 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/arith/options"
586 #line 25 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/arith/options"
588 #line 25 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/arith/options"
590 
591 #line 28 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/arith/options"
593 #line 28 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/arith/options"
595 
596 #line 32 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/arith/options"
598 #line 32 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/arith/options"
600 
601 #line 39 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/arith/options"
603 #line 39 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/arith/options"
605 #line 39 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/arith/options"
607 
608 #line 42 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/arith/options"
610 #line 42 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/arith/options"
612 
613 #line 45 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/arith/options"
615 #line 45 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/arith/options"
617 
618 #line 50 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/arith/options"
620 #line 50 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/arith/options"
622 #line 50 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/arith/options"
624 
625 #line 55 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/arith/options"
627 #line 55 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/arith/options"
629 
630 #line 59 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/arith/options"
632 #line 59 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/arith/options"
634 
635 #line 62 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/arith/options"
637 #line 62 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/arith/options"
639 #line 62 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/arith/options"
641 
642 #line 66 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/arith/options"
644 #line 66 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/arith/options"
646 
647 #line 69 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/arith/options"
649 #line 69 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/arith/options"
651 
652 #line 72 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/arith/options"
654 #line 72 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/arith/options"
656 #line 72 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/arith/options"
658 
659 #line 76 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/arith/options"
661 #line 76 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/arith/options"
662 inline bool useFC__option_t::wasSetByUser() const { return Options::current().wasSetByUser(*this); }
663 #line 76 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/arith/options"
664 inline void useFC__option_t::set(const useFC__option_t::type& v) { Options::current().set(*this, v); }
665 
666 #line 79 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/arith/options"
668 #line 79 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/arith/options"
669 inline bool useSOI__option_t::wasSetByUser() const { return Options::current().wasSetByUser(*this); }
670 #line 79 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/arith/options"
671 inline void useSOI__option_t::set(const useSOI__option_t::type& v) { Options::current().set(*this, v); }
672 
673 #line 82 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/arith/options"
675 #line 82 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/arith/options"
677 #line 82 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/arith/options"
679 
680 #line 85 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/arith/options"
682 #line 85 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/arith/options"
684 #line 85 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/arith/options"
686 
687 #line 88 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/arith/options"
689 #line 88 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/arith/options"
690 inline bool useApprox__option_t::wasSetByUser() const { return Options::current().wasSetByUser(*this); }
691 #line 88 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/arith/options"
693 
694 #line 91 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/arith/options"
696 #line 91 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/arith/options"
698 #line 91 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/arith/options"
700 
701 #line 94 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/arith/options"
703 #line 94 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/arith/options"
705 #line 94 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/arith/options"
707 
708 #line 97 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/arith/options"
710 #line 97 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/arith/options"
711 inline bool newProp__option_t::wasSetByUser() const { return Options::current().wasSetByUser(*this); }
712 #line 97 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/arith/options"
714 
715 #line 100 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/arith/options"
717 #line 100 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/arith/options"
719 #line 100 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/arith/options"
721 
722 #line 103 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/arith/options"
724 #line 103 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/arith/options"
726 #line 103 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/arith/options"
728 
729 #line 106 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/arith/options"
731 #line 106 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/arith/options"
732 inline bool rewriteDivk__option_t::wasSetByUser() const { return Options::current().wasSetByUser(*this); }
733 #line 106 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/arith/options"
735 
736 #line 109 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/arith/options"
738 #line 109 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/arith/options"
740 
741 #line 112 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/arith/options"
743 #line 112 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/arith/options"
745 
746 #line 115 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/arith/options"
748 #line 115 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/arith/options"
750 
751 #line 118 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/arith/options"
753 #line 118 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/arith/options"
754 inline bool rrTurns__option_t::wasSetByUser() const { return Options::current().wasSetByUser(*this); }
755 
756 #line 121 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/arith/options"
758 #line 121 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/arith/options"
759 inline bool dioRepeat__option_t::wasSetByUser() const { return Options::current().wasSetByUser(*this); }
760 
761 #line 124 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/arith/options"
763 #line 124 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/arith/options"
765 
766 #line 127 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/arith/options"
768 #line 127 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/arith/options"
770 
771 #line 130 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/arith/options"
773 #line 130 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/arith/options"
775 
776 #line 133 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/arith/options"
778 #line 133 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/arith/options"
780 
781 #line 136 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/arith/options"
783 #line 136 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/arith/options"
785 
786 #line 139 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/arith/options"
788 #line 139 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/arith/options"
790 
791 #line 142 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/arith/options"
793 #line 142 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/arith/options"
795 
796 #line 145 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/arith/options"
798 #line 145 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/arith/options"
800 
801 #line 148 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/arith/options"
803 #line 148 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/arith/options"
805 
806 #line 151 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/arith/options"
808 #line 151 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/arith/options"
810 
811 #line 154 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/arith/options"
813 #line 154 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/arith/options"
815 
816 #line 158 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/arith/options"
818 #line 158 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/arith/options"
819 inline bool pbRewrites__option_t::wasSetByUser() const { return Options::current().wasSetByUser(*this); }
820 
821 #line 161 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/arith/options"
823 #line 161 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/../theory/arith/options"
825 
826 #line 50 "/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/production/../../../src/options/base_options_template.h"
827 
828 }/* CVC4::options namespace */
829 
830 }/* CVC4 namespace */
831 
832 #endif /* __CVC4__OPTIONS__ARITH_H */
struct CVC4::options::doCutAllBounded__option_t doCutAllBounded
struct CVC4::options::trySolveIntStandardEffort__option_t trySolveIntStandardEffort
struct CVC4::options::restrictedPivots__option_t restrictedPivots
struct CVC4::options::arithPropagateMaxLength__option_t arithPropagateMaxLength
struct CVC4::options::maxReplayTree__option_t maxReplayTree
Definition: options.h:94
struct CVC4::options::replayNumericFailurePenalty__option_t replayNumericFailurePenalty
[[ Add one-line brief description here ]]
struct CVC4::options::soiQuickExplain__option_t soiQuickExplain
struct CVC4::options::useSOI__option_t useSOI
struct CVC4::options::arithStandardCheckVarOrderPivots__option_t arithStandardCheckVarOrderPivots
struct CVC4::options::dioRepeat__option_t dioRepeat
struct CVC4::options::maxCutsInContext__option_t maxCutsInContext
void set(const type &v)
Definition: options.h:692
struct CVC4::options::arithHeuristicPivots__option_t arithHeuristicPivots
struct CVC4::options::newProp__option_t newProp
struct CVC4::options::arithPropagationMode__option_t arithPropagationMode
const T::type & operator[](T) const
Get the value of the given option.
struct CVC4::options::maxApproxDepth__option_t maxApproxDepth
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::dioSolverTurns__option_t dioSolverTurns
struct CVC4::options::lemmaRejectCutSize__option_t lemmaRejectCutSize
struct CVC4::options::revertArithModels__option_t revertArithModels
struct CVC4::options::arithPropAsLemmaLength__option_t arithPropAsLemmaLength
struct CVC4::options::replayFailurePenalty__option_t replayFailurePenalty
struct CVC4::options::soiApproxMinorFailure__option_t soiApproxMinorFailure
struct CVC4::options::arithErrorSelectionRule__option_t arithErrorSelectionRule
[[ Add one-line brief description here ]]
struct CVC4::options::replayFailureLemma__option_t replayFailureLemma
#define CVC4_PUBLIC
Definition: cvc4_public.h:30
struct CVC4::options::arithMLTrickSubstitutions__option_t arithMLTrickSubstitutions
void set(const type &v)
Definition: options.h:671
struct CVC4::options::rrTurns__option_t rrTurns
struct CVC4::options::arithSimplexCheckPeriod__option_t arithSimplexCheckPeriod
struct CVC4::options::soiApproxMajorFailure__option_t soiApproxMajorFailure
struct CVC4::options::exportDioDecompositions__option_t exportDioDecompositions
Global (command-line, set-option, ...) parameters for SMT.
void set(const type &v)
Definition: options.h:664
struct CVC4::options::replayEarlyCloseDepths__option_t replayEarlyCloseDepths
struct CVC4::options::ppAssertMaxSubSize__option_t ppAssertMaxSubSize
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::replayRejectCutSize__option_t replayRejectCutSize
void set(const type &v)
Definition: options.h:713
struct CVC4::options::arithMLTrick__option_t arithMLTrick
[[ Add one-line brief description here ]]
struct CVC4::options::pbRewrites__option_t pbRewrites
struct CVC4::options::rewriteDivk__option_t rewriteDivk
struct CVC4::options::collectPivots__option_t collectPivots
struct CVC4::options::useFC__option_t useFC
struct CVC4::options::arithUnateLemmaMode__option_t arithUnateLemmaMode
void set(T, const typename T::type &)
Set the value of the given option.
Definition: options.h:78
struct CVC4::options::arithPivotThreshold__option_t arithPivotThreshold
struct CVC4::options::havePenalties__option_t havePenalties
struct CVC4::options::useApprox__option_t useApprox
struct CVC4::options::soiApproxMajorFailurePen__option_t soiApproxMajorFailurePen
struct CVC4::options::arithRewriteEq__option_t arithRewriteEq
struct CVC4::options::soiApproxMinorFailurePen__option_t soiApproxMinorFailurePen
bool wasSetByUser() const
Definition: options.h:662
struct CVC4::options::arithDioSolver__option_t arithDioSolver
struct CVC4::options::pbRewriteThreshold__option_t pbRewriteThreshold