1 |
|
/****************************************************************************** |
2 |
|
* Top contributors (to current version): |
3 |
|
* Mathias Preiner, Aina Niemetz |
4 |
|
* |
5 |
|
* This file is part of the cvc5 project. |
6 |
|
* |
7 |
|
* Copyright (c) 2009-2021 by the authors listed in the file AUTHORS |
8 |
|
* in the top-level source directory and their institutional affiliations. |
9 |
|
* All rights reserved. See the file COPYING in the top-level source |
10 |
|
* directory for licensing information. |
11 |
|
* **************************************************************************** |
12 |
|
* |
13 |
|
* Option template for option modules. |
14 |
|
* |
15 |
|
* For each <module>_options.toml configuration file, mkoptions.py |
16 |
|
* expands this template and generates a <module>_options.cpp file. |
17 |
|
*/ |
18 |
|
#include "options/arith_options.h" |
19 |
|
|
20 |
|
#include <iostream> |
21 |
|
|
22 |
|
#include "base/check.h" |
23 |
|
#include "options/option_exception.h" |
24 |
|
|
25 |
|
// clang-format off |
26 |
|
namespace cvc5 { |
27 |
|
|
28 |
|
template <> options::maxApproxDepth__option_t::type& Options::ref( |
29 |
|
options::maxApproxDepth__option_t) |
30 |
|
{ |
31 |
|
return arith().maxApproxDepth; |
32 |
|
} |
33 |
|
template <> const options::maxApproxDepth__option_t::type& Options::operator[]( |
34 |
|
options::maxApproxDepth__option_t) const |
35 |
|
{ |
36 |
|
return arith().maxApproxDepth; |
37 |
|
} |
38 |
|
template <> bool Options::wasSetByUser(options::maxApproxDepth__option_t) const |
39 |
|
{ |
40 |
|
return arith().maxApproxDepth__setByUser__; |
41 |
|
} |
42 |
|
template <> options::brabTest__option_t::type& Options::ref( |
43 |
|
options::brabTest__option_t) |
44 |
|
{ |
45 |
|
return arith().brabTest; |
46 |
|
} |
47 |
1096 |
template <> const options::brabTest__option_t::type& Options::operator[]( |
48 |
|
options::brabTest__option_t) const |
49 |
|
{ |
50 |
1096 |
return arith().brabTest; |
51 |
|
} |
52 |
|
template <> bool Options::wasSetByUser(options::brabTest__option_t) const |
53 |
|
{ |
54 |
|
return arith().brabTest__setByUser__; |
55 |
|
} |
56 |
|
template <> options::arithNoPartialFun__option_t::type& Options::ref( |
57 |
|
options::arithNoPartialFun__option_t) |
58 |
|
{ |
59 |
|
return arith().arithNoPartialFun; |
60 |
|
} |
61 |
633 |
template <> const options::arithNoPartialFun__option_t::type& Options::operator[]( |
62 |
|
options::arithNoPartialFun__option_t) const |
63 |
|
{ |
64 |
633 |
return arith().arithNoPartialFun; |
65 |
|
} |
66 |
|
template <> bool Options::wasSetByUser(options::arithNoPartialFun__option_t) const |
67 |
|
{ |
68 |
|
return arith().arithNoPartialFun__setByUser__; |
69 |
|
} |
70 |
|
template <> options::arithPropAsLemmaLength__option_t::type& Options::ref( |
71 |
|
options::arithPropAsLemmaLength__option_t) |
72 |
|
{ |
73 |
|
return arith().arithPropAsLemmaLength; |
74 |
|
} |
75 |
119987 |
template <> const options::arithPropAsLemmaLength__option_t::type& Options::operator[]( |
76 |
|
options::arithPropAsLemmaLength__option_t) const |
77 |
|
{ |
78 |
119987 |
return arith().arithPropAsLemmaLength; |
79 |
|
} |
80 |
|
template <> bool Options::wasSetByUser(options::arithPropAsLemmaLength__option_t) const |
81 |
|
{ |
82 |
|
return arith().arithPropAsLemmaLength__setByUser__; |
83 |
|
} |
84 |
|
template <> options::arithPropagationMode__option_t::type& Options::ref( |
85 |
|
options::arithPropagationMode__option_t) |
86 |
|
{ |
87 |
|
return arith().arithPropagationMode; |
88 |
|
} |
89 |
7096310 |
template <> const options::arithPropagationMode__option_t::type& Options::operator[]( |
90 |
|
options::arithPropagationMode__option_t) const |
91 |
|
{ |
92 |
7096310 |
return arith().arithPropagationMode; |
93 |
|
} |
94 |
|
template <> bool Options::wasSetByUser(options::arithPropagationMode__option_t) const |
95 |
|
{ |
96 |
|
return arith().arithPropagationMode__setByUser__; |
97 |
|
} |
98 |
9451 |
template <> options::arithRewriteEq__option_t::type& Options::ref( |
99 |
|
options::arithRewriteEq__option_t) |
100 |
|
{ |
101 |
9451 |
return arith().arithRewriteEq; |
102 |
|
} |
103 |
31497 |
template <> const options::arithRewriteEq__option_t::type& Options::operator[]( |
104 |
|
options::arithRewriteEq__option_t) const |
105 |
|
{ |
106 |
31497 |
return arith().arithRewriteEq; |
107 |
|
} |
108 |
9460 |
template <> bool Options::wasSetByUser(options::arithRewriteEq__option_t) const |
109 |
|
{ |
110 |
9460 |
return arith().arithRewriteEq__setByUser__; |
111 |
|
} |
112 |
|
template <> options::collectPivots__option_t::type& Options::ref( |
113 |
|
options::collectPivots__option_t) |
114 |
|
{ |
115 |
|
return arith().collectPivots; |
116 |
|
} |
117 |
1325885 |
template <> const options::collectPivots__option_t::type& Options::operator[]( |
118 |
|
options::collectPivots__option_t) const |
119 |
|
{ |
120 |
1325885 |
return arith().collectPivots; |
121 |
|
} |
122 |
|
template <> bool Options::wasSetByUser(options::collectPivots__option_t) const |
123 |
|
{ |
124 |
|
return arith().collectPivots__setByUser__; |
125 |
|
} |
126 |
|
template <> options::doCutAllBounded__option_t::type& Options::ref( |
127 |
|
options::doCutAllBounded__option_t) |
128 |
|
{ |
129 |
|
return arith().doCutAllBounded; |
130 |
|
} |
131 |
|
template <> const options::doCutAllBounded__option_t::type& Options::operator[]( |
132 |
|
options::doCutAllBounded__option_t) const |
133 |
|
{ |
134 |
|
return arith().doCutAllBounded; |
135 |
|
} |
136 |
|
template <> bool Options::wasSetByUser(options::doCutAllBounded__option_t) const |
137 |
|
{ |
138 |
|
return arith().doCutAllBounded__setByUser__; |
139 |
|
} |
140 |
|
template <> options::exportDioDecompositions__option_t::type& Options::ref( |
141 |
|
options::exportDioDecompositions__option_t) |
142 |
|
{ |
143 |
|
return arith().exportDioDecompositions; |
144 |
|
} |
145 |
334 |
template <> const options::exportDioDecompositions__option_t::type& Options::operator[]( |
146 |
|
options::exportDioDecompositions__option_t) const |
147 |
|
{ |
148 |
334 |
return arith().exportDioDecompositions; |
149 |
|
} |
150 |
|
template <> bool Options::wasSetByUser(options::exportDioDecompositions__option_t) const |
151 |
|
{ |
152 |
|
return arith().exportDioDecompositions__setByUser__; |
153 |
|
} |
154 |
|
template <> options::dioRepeat__option_t::type& Options::ref( |
155 |
|
options::dioRepeat__option_t) |
156 |
|
{ |
157 |
|
return arith().dioRepeat; |
158 |
|
} |
159 |
|
template <> const options::dioRepeat__option_t::type& Options::operator[]( |
160 |
|
options::dioRepeat__option_t) const |
161 |
|
{ |
162 |
|
return arith().dioRepeat; |
163 |
|
} |
164 |
|
template <> bool Options::wasSetByUser(options::dioRepeat__option_t) const |
165 |
|
{ |
166 |
|
return arith().dioRepeat__setByUser__; |
167 |
|
} |
168 |
|
template <> options::arithDioSolver__option_t::type& Options::ref( |
169 |
|
options::arithDioSolver__option_t) |
170 |
|
{ |
171 |
|
return arith().arithDioSolver; |
172 |
|
} |
173 |
5079 |
template <> const options::arithDioSolver__option_t::type& Options::operator[]( |
174 |
|
options::arithDioSolver__option_t) const |
175 |
|
{ |
176 |
5079 |
return arith().arithDioSolver; |
177 |
|
} |
178 |
|
template <> bool Options::wasSetByUser(options::arithDioSolver__option_t) const |
179 |
|
{ |
180 |
|
return arith().arithDioSolver__setByUser__; |
181 |
|
} |
182 |
|
template <> options::dioSolverTurns__option_t::type& Options::ref( |
183 |
|
options::dioSolverTurns__option_t) |
184 |
|
{ |
185 |
|
return arith().dioSolverTurns; |
186 |
|
} |
187 |
411 |
template <> const options::dioSolverTurns__option_t::type& Options::operator[]( |
188 |
|
options::dioSolverTurns__option_t) const |
189 |
|
{ |
190 |
411 |
return arith().dioSolverTurns; |
191 |
|
} |
192 |
|
template <> bool Options::wasSetByUser(options::dioSolverTurns__option_t) const |
193 |
|
{ |
194 |
|
return arith().dioSolverTurns__setByUser__; |
195 |
|
} |
196 |
|
template <> options::arithErrorSelectionRule__option_t::type& Options::ref( |
197 |
|
options::arithErrorSelectionRule__option_t) |
198 |
|
{ |
199 |
|
return arith().arithErrorSelectionRule; |
200 |
|
} |
201 |
37840 |
template <> const options::arithErrorSelectionRule__option_t::type& Options::operator[]( |
202 |
|
options::arithErrorSelectionRule__option_t) const |
203 |
|
{ |
204 |
37840 |
return arith().arithErrorSelectionRule; |
205 |
|
} |
206 |
|
template <> bool Options::wasSetByUser(options::arithErrorSelectionRule__option_t) const |
207 |
|
{ |
208 |
|
return arith().arithErrorSelectionRule__setByUser__; |
209 |
|
} |
210 |
|
template <> options::havePenalties__option_t::type& Options::ref( |
211 |
|
options::havePenalties__option_t) |
212 |
|
{ |
213 |
|
return arith().havePenalties; |
214 |
|
} |
215 |
|
template <> const options::havePenalties__option_t::type& Options::operator[]( |
216 |
|
options::havePenalties__option_t) const |
217 |
|
{ |
218 |
|
return arith().havePenalties; |
219 |
|
} |
220 |
|
template <> bool Options::wasSetByUser(options::havePenalties__option_t) const |
221 |
|
{ |
222 |
|
return arith().havePenalties__setByUser__; |
223 |
|
} |
224 |
9460 |
template <> options::arithHeuristicPivots__option_t::type& Options::ref( |
225 |
|
options::arithHeuristicPivots__option_t) |
226 |
|
{ |
227 |
9460 |
return arith().arithHeuristicPivots; |
228 |
|
} |
229 |
156180 |
template <> const options::arithHeuristicPivots__option_t::type& Options::operator[]( |
230 |
|
options::arithHeuristicPivots__option_t) const |
231 |
|
{ |
232 |
156180 |
return arith().arithHeuristicPivots; |
233 |
|
} |
234 |
9460 |
template <> bool Options::wasSetByUser(options::arithHeuristicPivots__option_t) const |
235 |
|
{ |
236 |
9460 |
return arith().arithHeuristicPivots__setByUser__; |
237 |
|
} |
238 |
|
template <> options::replayFailureLemma__option_t::type& Options::ref( |
239 |
|
options::replayFailureLemma__option_t) |
240 |
|
{ |
241 |
|
return arith().replayFailureLemma; |
242 |
|
} |
243 |
|
template <> const options::replayFailureLemma__option_t::type& Options::operator[]( |
244 |
|
options::replayFailureLemma__option_t) const |
245 |
|
{ |
246 |
|
return arith().replayFailureLemma; |
247 |
|
} |
248 |
|
template <> bool Options::wasSetByUser(options::replayFailureLemma__option_t) const |
249 |
|
{ |
250 |
|
return arith().replayFailureLemma__setByUser__; |
251 |
|
} |
252 |
|
template <> options::maxCutsInContext__option_t::type& Options::ref( |
253 |
|
options::maxCutsInContext__option_t) |
254 |
|
{ |
255 |
|
return arith().maxCutsInContext; |
256 |
|
} |
257 |
2613 |
template <> const options::maxCutsInContext__option_t::type& Options::operator[]( |
258 |
|
options::maxCutsInContext__option_t) const |
259 |
|
{ |
260 |
2613 |
return arith().maxCutsInContext; |
261 |
|
} |
262 |
|
template <> bool Options::wasSetByUser(options::maxCutsInContext__option_t) const |
263 |
|
{ |
264 |
|
return arith().maxCutsInContext__setByUser__; |
265 |
|
} |
266 |
2049 |
template <> options::arithMLTrick__option_t::type& Options::ref( |
267 |
|
options::arithMLTrick__option_t) |
268 |
|
{ |
269 |
2049 |
return arith().arithMLTrick; |
270 |
|
} |
271 |
18229 |
template <> const options::arithMLTrick__option_t::type& Options::operator[]( |
272 |
|
options::arithMLTrick__option_t) const |
273 |
|
{ |
274 |
18229 |
return arith().arithMLTrick; |
275 |
|
} |
276 |
|
template <> bool Options::wasSetByUser(options::arithMLTrick__option_t) const |
277 |
|
{ |
278 |
|
return arith().arithMLTrick__setByUser__; |
279 |
|
} |
280 |
|
template <> options::arithMLTrickSubstitutions__option_t::type& Options::ref( |
281 |
|
options::arithMLTrickSubstitutions__option_t) |
282 |
|
{ |
283 |
|
return arith().arithMLTrickSubstitutions; |
284 |
|
} |
285 |
|
template <> const options::arithMLTrickSubstitutions__option_t::type& Options::operator[]( |
286 |
|
options::arithMLTrickSubstitutions__option_t) const |
287 |
|
{ |
288 |
|
return arith().arithMLTrickSubstitutions; |
289 |
|
} |
290 |
|
template <> bool Options::wasSetByUser(options::arithMLTrickSubstitutions__option_t) const |
291 |
|
{ |
292 |
|
return arith().arithMLTrickSubstitutions__setByUser__; |
293 |
|
} |
294 |
|
template <> options::newProp__option_t::type& Options::ref( |
295 |
|
options::newProp__option_t) |
296 |
|
{ |
297 |
|
return arith().newProp; |
298 |
|
} |
299 |
851361 |
template <> const options::newProp__option_t::type& Options::operator[]( |
300 |
|
options::newProp__option_t) const |
301 |
|
{ |
302 |
851361 |
return arith().newProp; |
303 |
|
} |
304 |
|
template <> bool Options::wasSetByUser(options::newProp__option_t) const |
305 |
|
{ |
306 |
|
return arith().newProp__setByUser__; |
307 |
|
} |
308 |
100 |
template <> options::nlCad__option_t::type& Options::ref( |
309 |
|
options::nlCad__option_t) |
310 |
|
{ |
311 |
100 |
return arith().nlCad; |
312 |
|
} |
313 |
1244 |
template <> const options::nlCad__option_t::type& Options::operator[]( |
314 |
|
options::nlCad__option_t) const |
315 |
|
{ |
316 |
1244 |
return arith().nlCad; |
317 |
|
} |
318 |
100 |
template <> bool Options::wasSetByUser(options::nlCad__option_t) const |
319 |
|
{ |
320 |
100 |
return arith().nlCad__setByUser__; |
321 |
|
} |
322 |
|
template <> options::nlCadUseInitial__option_t::type& Options::ref( |
323 |
|
options::nlCadUseInitial__option_t) |
324 |
|
{ |
325 |
|
return arith().nlCadUseInitial; |
326 |
|
} |
327 |
182 |
template <> const options::nlCadUseInitial__option_t::type& Options::operator[]( |
328 |
|
options::nlCadUseInitial__option_t) const |
329 |
|
{ |
330 |
182 |
return arith().nlCadUseInitial; |
331 |
|
} |
332 |
|
template <> bool Options::wasSetByUser(options::nlCadUseInitial__option_t) const |
333 |
|
{ |
334 |
|
return arith().nlCadUseInitial__setByUser__; |
335 |
|
} |
336 |
|
template <> options::nlExtEntailConflicts__option_t::type& Options::ref( |
337 |
|
options::nlExtEntailConflicts__option_t) |
338 |
|
{ |
339 |
|
return arith().nlExtEntailConflicts; |
340 |
|
} |
341 |
8954 |
template <> const options::nlExtEntailConflicts__option_t::type& Options::operator[]( |
342 |
|
options::nlExtEntailConflicts__option_t) const |
343 |
|
{ |
344 |
8954 |
return arith().nlExtEntailConflicts; |
345 |
|
} |
346 |
|
template <> bool Options::wasSetByUser(options::nlExtEntailConflicts__option_t) const |
347 |
|
{ |
348 |
|
return arith().nlExtEntailConflicts__setByUser__; |
349 |
|
} |
350 |
|
template <> options::nlExtFactor__option_t::type& Options::ref( |
351 |
|
options::nlExtFactor__option_t) |
352 |
|
{ |
353 |
|
return arith().nlExtFactor; |
354 |
|
} |
355 |
403 |
template <> const options::nlExtFactor__option_t::type& Options::operator[]( |
356 |
|
options::nlExtFactor__option_t) const |
357 |
|
{ |
358 |
403 |
return arith().nlExtFactor; |
359 |
|
} |
360 |
|
template <> bool Options::wasSetByUser(options::nlExtFactor__option_t) const |
361 |
|
{ |
362 |
|
return arith().nlExtFactor__setByUser__; |
363 |
|
} |
364 |
|
template <> options::nlExtIncPrecision__option_t::type& Options::ref( |
365 |
|
options::nlExtIncPrecision__option_t) |
366 |
|
{ |
367 |
|
return arith().nlExtIncPrecision; |
368 |
|
} |
369 |
18 |
template <> const options::nlExtIncPrecision__option_t::type& Options::operator[]( |
370 |
|
options::nlExtIncPrecision__option_t) const |
371 |
|
{ |
372 |
18 |
return arith().nlExtIncPrecision; |
373 |
|
} |
374 |
|
template <> bool Options::wasSetByUser(options::nlExtIncPrecision__option_t) const |
375 |
|
{ |
376 |
|
return arith().nlExtIncPrecision__setByUser__; |
377 |
|
} |
378 |
|
template <> options::nlExtPurify__option_t::type& Options::ref( |
379 |
|
options::nlExtPurify__option_t) |
380 |
|
{ |
381 |
|
return arith().nlExtPurify; |
382 |
|
} |
383 |
12885 |
template <> const options::nlExtPurify__option_t::type& Options::operator[]( |
384 |
|
options::nlExtPurify__option_t) const |
385 |
|
{ |
386 |
12885 |
return arith().nlExtPurify; |
387 |
|
} |
388 |
|
template <> bool Options::wasSetByUser(options::nlExtPurify__option_t) const |
389 |
|
{ |
390 |
|
return arith().nlExtPurify__setByUser__; |
391 |
|
} |
392 |
|
template <> options::nlExtResBound__option_t::type& Options::ref( |
393 |
|
options::nlExtResBound__option_t) |
394 |
|
{ |
395 |
|
return arith().nlExtResBound; |
396 |
|
} |
397 |
403 |
template <> const options::nlExtResBound__option_t::type& Options::operator[]( |
398 |
|
options::nlExtResBound__option_t) const |
399 |
|
{ |
400 |
403 |
return arith().nlExtResBound; |
401 |
|
} |
402 |
|
template <> bool Options::wasSetByUser(options::nlExtResBound__option_t) const |
403 |
|
{ |
404 |
|
return arith().nlExtResBound__setByUser__; |
405 |
|
} |
406 |
|
template <> options::nlExtRewrites__option_t::type& Options::ref( |
407 |
|
options::nlExtRewrites__option_t) |
408 |
|
{ |
409 |
|
return arith().nlExtRewrites; |
410 |
|
} |
411 |
26424 |
template <> const options::nlExtRewrites__option_t::type& Options::operator[]( |
412 |
|
options::nlExtRewrites__option_t) const |
413 |
|
{ |
414 |
26424 |
return arith().nlExtRewrites; |
415 |
|
} |
416 |
|
template <> bool Options::wasSetByUser(options::nlExtRewrites__option_t) const |
417 |
|
{ |
418 |
|
return arith().nlExtRewrites__setByUser__; |
419 |
|
} |
420 |
|
template <> options::nlExtSplitZero__option_t::type& Options::ref( |
421 |
|
options::nlExtSplitZero__option_t) |
422 |
|
{ |
423 |
|
return arith().nlExtSplitZero; |
424 |
|
} |
425 |
403 |
template <> const options::nlExtSplitZero__option_t::type& Options::operator[]( |
426 |
|
options::nlExtSplitZero__option_t) const |
427 |
|
{ |
428 |
403 |
return arith().nlExtSplitZero; |
429 |
|
} |
430 |
|
template <> bool Options::wasSetByUser(options::nlExtSplitZero__option_t) const |
431 |
|
{ |
432 |
|
return arith().nlExtSplitZero__setByUser__; |
433 |
|
} |
434 |
|
template <> options::nlExtTfTaylorDegree__option_t::type& Options::ref( |
435 |
|
options::nlExtTfTaylorDegree__option_t) |
436 |
|
{ |
437 |
|
return arith().nlExtTfTaylorDegree; |
438 |
|
} |
439 |
4914 |
template <> const options::nlExtTfTaylorDegree__option_t::type& Options::operator[]( |
440 |
|
options::nlExtTfTaylorDegree__option_t) const |
441 |
|
{ |
442 |
4914 |
return arith().nlExtTfTaylorDegree; |
443 |
|
} |
444 |
|
template <> bool Options::wasSetByUser(options::nlExtTfTaylorDegree__option_t) const |
445 |
|
{ |
446 |
|
return arith().nlExtTfTaylorDegree__setByUser__; |
447 |
|
} |
448 |
|
template <> options::nlExtTfTangentPlanes__option_t::type& Options::ref( |
449 |
|
options::nlExtTfTangentPlanes__option_t) |
450 |
|
{ |
451 |
|
return arith().nlExtTfTangentPlanes; |
452 |
|
} |
453 |
403 |
template <> const options::nlExtTfTangentPlanes__option_t::type& Options::operator[]( |
454 |
|
options::nlExtTfTangentPlanes__option_t) const |
455 |
|
{ |
456 |
403 |
return arith().nlExtTfTangentPlanes; |
457 |
|
} |
458 |
|
template <> bool Options::wasSetByUser(options::nlExtTfTangentPlanes__option_t) const |
459 |
|
{ |
460 |
|
return arith().nlExtTfTangentPlanes__setByUser__; |
461 |
|
} |
462 |
799 |
template <> options::nlExtTangentPlanes__option_t::type& Options::ref( |
463 |
|
options::nlExtTangentPlanes__option_t) |
464 |
|
{ |
465 |
799 |
return arith().nlExtTangentPlanes; |
466 |
|
} |
467 |
62468 |
template <> const options::nlExtTangentPlanes__option_t::type& Options::operator[]( |
468 |
|
options::nlExtTangentPlanes__option_t) const |
469 |
|
{ |
470 |
62468 |
return arith().nlExtTangentPlanes; |
471 |
|
} |
472 |
813 |
template <> bool Options::wasSetByUser(options::nlExtTangentPlanes__option_t) const |
473 |
|
{ |
474 |
813 |
return arith().nlExtTangentPlanes__setByUser__; |
475 |
|
} |
476 |
505 |
template <> options::nlExtTangentPlanesInterleave__option_t::type& Options::ref( |
477 |
|
options::nlExtTangentPlanesInterleave__option_t) |
478 |
|
{ |
479 |
505 |
return arith().nlExtTangentPlanesInterleave; |
480 |
|
} |
481 |
144 |
template <> const options::nlExtTangentPlanesInterleave__option_t::type& Options::operator[]( |
482 |
|
options::nlExtTangentPlanesInterleave__option_t) const |
483 |
|
{ |
484 |
144 |
return arith().nlExtTangentPlanesInterleave; |
485 |
|
} |
486 |
505 |
template <> bool Options::wasSetByUser(options::nlExtTangentPlanesInterleave__option_t) const |
487 |
|
{ |
488 |
505 |
return arith().nlExtTangentPlanesInterleave__setByUser__; |
489 |
|
} |
490 |
48 |
template <> options::nlExt__option_t::type& Options::ref( |
491 |
|
options::nlExt__option_t) |
492 |
|
{ |
493 |
48 |
return arith().nlExt; |
494 |
|
} |
495 |
2085 |
template <> const options::nlExt__option_t::type& Options::operator[]( |
496 |
|
options::nlExt__option_t) const |
497 |
|
{ |
498 |
2085 |
return arith().nlExt; |
499 |
|
} |
500 |
100 |
template <> bool Options::wasSetByUser(options::nlExt__option_t) const |
501 |
|
{ |
502 |
100 |
return arith().nlExt__setByUser__; |
503 |
|
} |
504 |
|
template <> options::nlICP__option_t::type& Options::ref( |
505 |
|
options::nlICP__option_t) |
506 |
|
{ |
507 |
|
return arith().nlICP; |
508 |
|
} |
509 |
437 |
template <> const options::nlICP__option_t::type& Options::operator[]( |
510 |
|
options::nlICP__option_t) const |
511 |
|
{ |
512 |
437 |
return arith().nlICP; |
513 |
|
} |
514 |
|
template <> bool Options::wasSetByUser(options::nlICP__option_t) const |
515 |
|
{ |
516 |
|
return arith().nlICP__setByUser__; |
517 |
|
} |
518 |
100 |
template <> options::nlRlvMode__option_t::type& Options::ref( |
519 |
|
options::nlRlvMode__option_t) |
520 |
|
{ |
521 |
100 |
return arith().nlRlvMode; |
522 |
|
} |
523 |
10418 |
template <> const options::nlRlvMode__option_t::type& Options::operator[]( |
524 |
|
options::nlRlvMode__option_t) const |
525 |
|
{ |
526 |
10418 |
return arith().nlRlvMode; |
527 |
|
} |
528 |
100 |
template <> bool Options::wasSetByUser(options::nlRlvMode__option_t) const |
529 |
|
{ |
530 |
100 |
return arith().nlRlvMode__setByUser__; |
531 |
|
} |
532 |
|
template <> options::pbRewrites__option_t::type& Options::ref( |
533 |
|
options::pbRewrites__option_t) |
534 |
|
{ |
535 |
|
return arith().pbRewrites; |
536 |
|
} |
537 |
15299 |
template <> const options::pbRewrites__option_t::type& Options::operator[]( |
538 |
|
options::pbRewrites__option_t) const |
539 |
|
{ |
540 |
15299 |
return arith().pbRewrites; |
541 |
|
} |
542 |
|
template <> bool Options::wasSetByUser(options::pbRewrites__option_t) const |
543 |
|
{ |
544 |
|
return arith().pbRewrites__setByUser__; |
545 |
|
} |
546 |
9460 |
template <> options::arithPivotThreshold__option_t::type& Options::ref( |
547 |
|
options::arithPivotThreshold__option_t) |
548 |
|
{ |
549 |
9460 |
return arith().arithPivotThreshold; |
550 |
|
} |
551 |
390284 |
template <> const options::arithPivotThreshold__option_t::type& Options::operator[]( |
552 |
|
options::arithPivotThreshold__option_t) const |
553 |
|
{ |
554 |
390284 |
return arith().arithPivotThreshold; |
555 |
|
} |
556 |
9460 |
template <> bool Options::wasSetByUser(options::arithPivotThreshold__option_t) const |
557 |
|
{ |
558 |
9460 |
return arith().arithPivotThreshold__setByUser__; |
559 |
|
} |
560 |
|
template <> options::ppAssertMaxSubSize__option_t::type& Options::ref( |
561 |
|
options::ppAssertMaxSubSize__option_t) |
562 |
|
{ |
563 |
|
return arith().ppAssertMaxSubSize; |
564 |
|
} |
565 |
1378 |
template <> const options::ppAssertMaxSubSize__option_t::type& Options::operator[]( |
566 |
|
options::ppAssertMaxSubSize__option_t) const |
567 |
|
{ |
568 |
1378 |
return arith().ppAssertMaxSubSize; |
569 |
|
} |
570 |
|
template <> bool Options::wasSetByUser(options::ppAssertMaxSubSize__option_t) const |
571 |
|
{ |
572 |
|
return arith().ppAssertMaxSubSize__setByUser__; |
573 |
|
} |
574 |
|
template <> options::arithPropagateMaxLength__option_t::type& Options::ref( |
575 |
|
options::arithPropagateMaxLength__option_t) |
576 |
|
{ |
577 |
|
return arith().arithPropagateMaxLength; |
578 |
|
} |
579 |
9737988 |
template <> const options::arithPropagateMaxLength__option_t::type& Options::operator[]( |
580 |
|
options::arithPropagateMaxLength__option_t) const |
581 |
|
{ |
582 |
9737988 |
return arith().arithPropagateMaxLength; |
583 |
|
} |
584 |
|
template <> bool Options::wasSetByUser(options::arithPropagateMaxLength__option_t) const |
585 |
|
{ |
586 |
|
return arith().arithPropagateMaxLength__setByUser__; |
587 |
|
} |
588 |
|
template <> options::replayEarlyCloseDepths__option_t::type& Options::ref( |
589 |
|
options::replayEarlyCloseDepths__option_t) |
590 |
|
{ |
591 |
|
return arith().replayEarlyCloseDepths; |
592 |
|
} |
593 |
|
template <> const options::replayEarlyCloseDepths__option_t::type& Options::operator[]( |
594 |
|
options::replayEarlyCloseDepths__option_t) const |
595 |
|
{ |
596 |
|
return arith().replayEarlyCloseDepths; |
597 |
|
} |
598 |
|
template <> bool Options::wasSetByUser(options::replayEarlyCloseDepths__option_t) const |
599 |
|
{ |
600 |
|
return arith().replayEarlyCloseDepths__setByUser__; |
601 |
|
} |
602 |
|
template <> options::replayFailurePenalty__option_t::type& Options::ref( |
603 |
|
options::replayFailurePenalty__option_t) |
604 |
|
{ |
605 |
|
return arith().replayFailurePenalty; |
606 |
|
} |
607 |
|
template <> const options::replayFailurePenalty__option_t::type& Options::operator[]( |
608 |
|
options::replayFailurePenalty__option_t) const |
609 |
|
{ |
610 |
|
return arith().replayFailurePenalty; |
611 |
|
} |
612 |
|
template <> bool Options::wasSetByUser(options::replayFailurePenalty__option_t) const |
613 |
|
{ |
614 |
|
return arith().replayFailurePenalty__setByUser__; |
615 |
|
} |
616 |
|
template <> options::lemmaRejectCutSize__option_t::type& Options::ref( |
617 |
|
options::lemmaRejectCutSize__option_t) |
618 |
|
{ |
619 |
|
return arith().lemmaRejectCutSize; |
620 |
|
} |
621 |
|
template <> const options::lemmaRejectCutSize__option_t::type& Options::operator[]( |
622 |
|
options::lemmaRejectCutSize__option_t) const |
623 |
|
{ |
624 |
|
return arith().lemmaRejectCutSize; |
625 |
|
} |
626 |
|
template <> bool Options::wasSetByUser(options::lemmaRejectCutSize__option_t) const |
627 |
|
{ |
628 |
|
return arith().lemmaRejectCutSize__setByUser__; |
629 |
|
} |
630 |
|
template <> options::replayNumericFailurePenalty__option_t::type& Options::ref( |
631 |
|
options::replayNumericFailurePenalty__option_t) |
632 |
|
{ |
633 |
|
return arith().replayNumericFailurePenalty; |
634 |
|
} |
635 |
|
template <> const options::replayNumericFailurePenalty__option_t::type& Options::operator[]( |
636 |
|
options::replayNumericFailurePenalty__option_t) const |
637 |
|
{ |
638 |
|
return arith().replayNumericFailurePenalty; |
639 |
|
} |
640 |
|
template <> bool Options::wasSetByUser(options::replayNumericFailurePenalty__option_t) const |
641 |
|
{ |
642 |
|
return arith().replayNumericFailurePenalty__setByUser__; |
643 |
|
} |
644 |
|
template <> options::replayRejectCutSize__option_t::type& Options::ref( |
645 |
|
options::replayRejectCutSize__option_t) |
646 |
|
{ |
647 |
|
return arith().replayRejectCutSize; |
648 |
|
} |
649 |
|
template <> const options::replayRejectCutSize__option_t::type& Options::operator[]( |
650 |
|
options::replayRejectCutSize__option_t) const |
651 |
|
{ |
652 |
|
return arith().replayRejectCutSize; |
653 |
|
} |
654 |
|
template <> bool Options::wasSetByUser(options::replayRejectCutSize__option_t) const |
655 |
|
{ |
656 |
|
return arith().replayRejectCutSize__setByUser__; |
657 |
|
} |
658 |
|
template <> options::soiApproxMajorFailurePen__option_t::type& Options::ref( |
659 |
|
options::soiApproxMajorFailurePen__option_t) |
660 |
|
{ |
661 |
|
return arith().soiApproxMajorFailurePen; |
662 |
|
} |
663 |
|
template <> const options::soiApproxMajorFailurePen__option_t::type& Options::operator[]( |
664 |
|
options::soiApproxMajorFailurePen__option_t) const |
665 |
|
{ |
666 |
|
return arith().soiApproxMajorFailurePen; |
667 |
|
} |
668 |
|
template <> bool Options::wasSetByUser(options::soiApproxMajorFailurePen__option_t) const |
669 |
|
{ |
670 |
|
return arith().soiApproxMajorFailurePen__setByUser__; |
671 |
|
} |
672 |
|
template <> options::soiApproxMajorFailure__option_t::type& Options::ref( |
673 |
|
options::soiApproxMajorFailure__option_t) |
674 |
|
{ |
675 |
|
return arith().soiApproxMajorFailure; |
676 |
|
} |
677 |
|
template <> const options::soiApproxMajorFailure__option_t::type& Options::operator[]( |
678 |
|
options::soiApproxMajorFailure__option_t) const |
679 |
|
{ |
680 |
|
return arith().soiApproxMajorFailure; |
681 |
|
} |
682 |
|
template <> bool Options::wasSetByUser(options::soiApproxMajorFailure__option_t) const |
683 |
|
{ |
684 |
|
return arith().soiApproxMajorFailure__setByUser__; |
685 |
|
} |
686 |
|
template <> options::soiApproxMinorFailurePen__option_t::type& Options::ref( |
687 |
|
options::soiApproxMinorFailurePen__option_t) |
688 |
|
{ |
689 |
|
return arith().soiApproxMinorFailurePen; |
690 |
|
} |
691 |
|
template <> const options::soiApproxMinorFailurePen__option_t::type& Options::operator[]( |
692 |
|
options::soiApproxMinorFailurePen__option_t) const |
693 |
|
{ |
694 |
|
return arith().soiApproxMinorFailurePen; |
695 |
|
} |
696 |
|
template <> bool Options::wasSetByUser(options::soiApproxMinorFailurePen__option_t) const |
697 |
|
{ |
698 |
|
return arith().soiApproxMinorFailurePen__setByUser__; |
699 |
|
} |
700 |
|
template <> options::soiApproxMinorFailure__option_t::type& Options::ref( |
701 |
|
options::soiApproxMinorFailure__option_t) |
702 |
|
{ |
703 |
|
return arith().soiApproxMinorFailure; |
704 |
|
} |
705 |
|
template <> const options::soiApproxMinorFailure__option_t::type& Options::operator[]( |
706 |
|
options::soiApproxMinorFailure__option_t) const |
707 |
|
{ |
708 |
|
return arith().soiApproxMinorFailure; |
709 |
|
} |
710 |
|
template <> bool Options::wasSetByUser(options::soiApproxMinorFailure__option_t) const |
711 |
|
{ |
712 |
|
return arith().soiApproxMinorFailure__setByUser__; |
713 |
|
} |
714 |
|
template <> options::restrictedPivots__option_t::type& Options::ref( |
715 |
|
options::restrictedPivots__option_t) |
716 |
|
{ |
717 |
|
return arith().restrictedPivots; |
718 |
|
} |
719 |
1319444 |
template <> const options::restrictedPivots__option_t::type& Options::operator[]( |
720 |
|
options::restrictedPivots__option_t) const |
721 |
|
{ |
722 |
1319444 |
return arith().restrictedPivots; |
723 |
|
} |
724 |
|
template <> bool Options::wasSetByUser(options::restrictedPivots__option_t) const |
725 |
|
{ |
726 |
|
return arith().restrictedPivots__setByUser__; |
727 |
|
} |
728 |
|
template <> options::revertArithModels__option_t::type& Options::ref( |
729 |
|
options::revertArithModels__option_t) |
730 |
|
{ |
731 |
|
return arith().revertArithModels; |
732 |
|
} |
733 |
12920 |
template <> const options::revertArithModels__option_t::type& Options::operator[]( |
734 |
|
options::revertArithModels__option_t) const |
735 |
|
{ |
736 |
12920 |
return arith().revertArithModels; |
737 |
|
} |
738 |
|
template <> bool Options::wasSetByUser(options::revertArithModels__option_t) const |
739 |
|
{ |
740 |
|
return arith().revertArithModels__setByUser__; |
741 |
|
} |
742 |
|
template <> options::rrTurns__option_t::type& Options::ref( |
743 |
|
options::rrTurns__option_t) |
744 |
|
{ |
745 |
|
return arith().rrTurns; |
746 |
|
} |
747 |
123 |
template <> const options::rrTurns__option_t::type& Options::operator[]( |
748 |
|
options::rrTurns__option_t) const |
749 |
|
{ |
750 |
123 |
return arith().rrTurns; |
751 |
|
} |
752 |
|
template <> bool Options::wasSetByUser(options::rrTurns__option_t) const |
753 |
|
{ |
754 |
|
return arith().rrTurns__setByUser__; |
755 |
|
} |
756 |
|
template <> options::trySolveIntStandardEffort__option_t::type& Options::ref( |
757 |
|
options::trySolveIntStandardEffort__option_t) |
758 |
|
{ |
759 |
|
return arith().trySolveIntStandardEffort; |
760 |
|
} |
761 |
|
template <> const options::trySolveIntStandardEffort__option_t::type& Options::operator[]( |
762 |
|
options::trySolveIntStandardEffort__option_t) const |
763 |
|
{ |
764 |
|
return arith().trySolveIntStandardEffort; |
765 |
|
} |
766 |
|
template <> bool Options::wasSetByUser(options::trySolveIntStandardEffort__option_t) const |
767 |
|
{ |
768 |
|
return arith().trySolveIntStandardEffort__setByUser__; |
769 |
|
} |
770 |
|
template <> options::arithSimplexCheckPeriod__option_t::type& Options::ref( |
771 |
|
options::arithSimplexCheckPeriod__option_t) |
772 |
|
{ |
773 |
|
return arith().arithSimplexCheckPeriod; |
774 |
|
} |
775 |
85513 |
template <> const options::arithSimplexCheckPeriod__option_t::type& Options::operator[]( |
776 |
|
options::arithSimplexCheckPeriod__option_t) const |
777 |
|
{ |
778 |
85513 |
return arith().arithSimplexCheckPeriod; |
779 |
|
} |
780 |
|
template <> bool Options::wasSetByUser(options::arithSimplexCheckPeriod__option_t) const |
781 |
|
{ |
782 |
|
return arith().arithSimplexCheckPeriod__setByUser__; |
783 |
|
} |
784 |
|
template <> options::soiQuickExplain__option_t::type& Options::ref( |
785 |
|
options::soiQuickExplain__option_t) |
786 |
|
{ |
787 |
|
return arith().soiQuickExplain; |
788 |
|
} |
789 |
|
template <> const options::soiQuickExplain__option_t::type& Options::operator[]( |
790 |
|
options::soiQuickExplain__option_t) const |
791 |
|
{ |
792 |
|
return arith().soiQuickExplain; |
793 |
|
} |
794 |
|
template <> bool Options::wasSetByUser(options::soiQuickExplain__option_t) const |
795 |
|
{ |
796 |
|
return arith().soiQuickExplain__setByUser__; |
797 |
|
} |
798 |
9460 |
template <> options::arithStandardCheckVarOrderPivots__option_t::type& Options::ref( |
799 |
|
options::arithStandardCheckVarOrderPivots__option_t) |
800 |
|
{ |
801 |
9460 |
return arith().arithStandardCheckVarOrderPivots; |
802 |
|
} |
803 |
112339 |
template <> const options::arithStandardCheckVarOrderPivots__option_t::type& Options::operator[]( |
804 |
|
options::arithStandardCheckVarOrderPivots__option_t) const |
805 |
|
{ |
806 |
112339 |
return arith().arithStandardCheckVarOrderPivots; |
807 |
|
} |
808 |
9460 |
template <> bool Options::wasSetByUser(options::arithStandardCheckVarOrderPivots__option_t) const |
809 |
|
{ |
810 |
9460 |
return arith().arithStandardCheckVarOrderPivots__setByUser__; |
811 |
|
} |
812 |
|
template <> options::arithUnateLemmaMode__option_t::type& Options::ref( |
813 |
|
options::arithUnateLemmaMode__option_t) |
814 |
|
{ |
815 |
|
return arith().arithUnateLemmaMode; |
816 |
|
} |
817 |
7362 |
template <> const options::arithUnateLemmaMode__option_t::type& Options::operator[]( |
818 |
|
options::arithUnateLemmaMode__option_t) const |
819 |
|
{ |
820 |
7362 |
return arith().arithUnateLemmaMode; |
821 |
|
} |
822 |
|
template <> bool Options::wasSetByUser(options::arithUnateLemmaMode__option_t) const |
823 |
|
{ |
824 |
|
return arith().arithUnateLemmaMode__setByUser__; |
825 |
|
} |
826 |
|
template <> options::useApprox__option_t::type& Options::ref( |
827 |
|
options::useApprox__option_t) |
828 |
|
{ |
829 |
|
return arith().useApprox; |
830 |
|
} |
831 |
3988800 |
template <> const options::useApprox__option_t::type& Options::operator[]( |
832 |
|
options::useApprox__option_t) const |
833 |
|
{ |
834 |
3988800 |
return arith().useApprox; |
835 |
|
} |
836 |
|
template <> bool Options::wasSetByUser(options::useApprox__option_t) const |
837 |
|
{ |
838 |
|
return arith().useApprox__setByUser__; |
839 |
|
} |
840 |
|
template <> options::useFC__option_t::type& Options::ref( |
841 |
|
options::useFC__option_t) |
842 |
|
{ |
843 |
|
return arith().useFC; |
844 |
|
} |
845 |
1380024 |
template <> const options::useFC__option_t::type& Options::operator[]( |
846 |
|
options::useFC__option_t) const |
847 |
|
{ |
848 |
1380024 |
return arith().useFC; |
849 |
|
} |
850 |
|
template <> bool Options::wasSetByUser(options::useFC__option_t) const |
851 |
|
{ |
852 |
|
return arith().useFC__setByUser__; |
853 |
|
} |
854 |
|
template <> options::useSOI__option_t::type& Options::ref( |
855 |
|
options::useSOI__option_t) |
856 |
|
{ |
857 |
|
return arith().useSOI; |
858 |
|
} |
859 |
6054 |
template <> const options::useSOI__option_t::type& Options::operator[]( |
860 |
|
options::useSOI__option_t) const |
861 |
|
{ |
862 |
6054 |
return arith().useSOI; |
863 |
|
} |
864 |
|
template <> bool Options::wasSetByUser(options::useSOI__option_t) const |
865 |
|
{ |
866 |
|
return arith().useSOI__setByUser__; |
867 |
|
} |
868 |
|
|
869 |
|
namespace options { |
870 |
|
|
871 |
|
thread_local struct maxApproxDepth__option_t maxApproxDepth; |
872 |
|
thread_local struct brabTest__option_t brabTest; |
873 |
|
thread_local struct arithNoPartialFun__option_t arithNoPartialFun; |
874 |
|
thread_local struct arithPropAsLemmaLength__option_t arithPropAsLemmaLength; |
875 |
|
thread_local struct arithPropagationMode__option_t arithPropagationMode; |
876 |
|
thread_local struct arithRewriteEq__option_t arithRewriteEq; |
877 |
|
thread_local struct collectPivots__option_t collectPivots; |
878 |
|
thread_local struct doCutAllBounded__option_t doCutAllBounded; |
879 |
|
thread_local struct exportDioDecompositions__option_t exportDioDecompositions; |
880 |
|
thread_local struct dioRepeat__option_t dioRepeat; |
881 |
|
thread_local struct arithDioSolver__option_t arithDioSolver; |
882 |
|
thread_local struct dioSolverTurns__option_t dioSolverTurns; |
883 |
|
thread_local struct arithErrorSelectionRule__option_t arithErrorSelectionRule; |
884 |
|
thread_local struct havePenalties__option_t havePenalties; |
885 |
|
thread_local struct arithHeuristicPivots__option_t arithHeuristicPivots; |
886 |
|
thread_local struct replayFailureLemma__option_t replayFailureLemma; |
887 |
|
thread_local struct maxCutsInContext__option_t maxCutsInContext; |
888 |
|
thread_local struct arithMLTrick__option_t arithMLTrick; |
889 |
|
thread_local struct arithMLTrickSubstitutions__option_t arithMLTrickSubstitutions; |
890 |
|
thread_local struct newProp__option_t newProp; |
891 |
|
thread_local struct nlCad__option_t nlCad; |
892 |
|
thread_local struct nlCadUseInitial__option_t nlCadUseInitial; |
893 |
|
thread_local struct nlExtEntailConflicts__option_t nlExtEntailConflicts; |
894 |
|
thread_local struct nlExtFactor__option_t nlExtFactor; |
895 |
|
thread_local struct nlExtIncPrecision__option_t nlExtIncPrecision; |
896 |
|
thread_local struct nlExtPurify__option_t nlExtPurify; |
897 |
|
thread_local struct nlExtResBound__option_t nlExtResBound; |
898 |
|
thread_local struct nlExtRewrites__option_t nlExtRewrites; |
899 |
|
thread_local struct nlExtSplitZero__option_t nlExtSplitZero; |
900 |
|
thread_local struct nlExtTfTaylorDegree__option_t nlExtTfTaylorDegree; |
901 |
|
thread_local struct nlExtTfTangentPlanes__option_t nlExtTfTangentPlanes; |
902 |
|
thread_local struct nlExtTangentPlanes__option_t nlExtTangentPlanes; |
903 |
|
thread_local struct nlExtTangentPlanesInterleave__option_t nlExtTangentPlanesInterleave; |
904 |
|
thread_local struct nlExt__option_t nlExt; |
905 |
|
thread_local struct nlICP__option_t nlICP; |
906 |
|
thread_local struct nlRlvMode__option_t nlRlvMode; |
907 |
|
thread_local struct pbRewrites__option_t pbRewrites; |
908 |
|
thread_local struct arithPivotThreshold__option_t arithPivotThreshold; |
909 |
|
thread_local struct ppAssertMaxSubSize__option_t ppAssertMaxSubSize; |
910 |
|
thread_local struct arithPropagateMaxLength__option_t arithPropagateMaxLength; |
911 |
|
thread_local struct replayEarlyCloseDepths__option_t replayEarlyCloseDepths; |
912 |
|
thread_local struct replayFailurePenalty__option_t replayFailurePenalty; |
913 |
|
thread_local struct lemmaRejectCutSize__option_t lemmaRejectCutSize; |
914 |
|
thread_local struct replayNumericFailurePenalty__option_t replayNumericFailurePenalty; |
915 |
|
thread_local struct replayRejectCutSize__option_t replayRejectCutSize; |
916 |
|
thread_local struct soiApproxMajorFailurePen__option_t soiApproxMajorFailurePen; |
917 |
|
thread_local struct soiApproxMajorFailure__option_t soiApproxMajorFailure; |
918 |
|
thread_local struct soiApproxMinorFailurePen__option_t soiApproxMinorFailurePen; |
919 |
|
thread_local struct soiApproxMinorFailure__option_t soiApproxMinorFailure; |
920 |
|
thread_local struct restrictedPivots__option_t restrictedPivots; |
921 |
|
thread_local struct revertArithModels__option_t revertArithModels; |
922 |
|
thread_local struct rrTurns__option_t rrTurns; |
923 |
|
thread_local struct trySolveIntStandardEffort__option_t trySolveIntStandardEffort; |
924 |
|
thread_local struct arithSimplexCheckPeriod__option_t arithSimplexCheckPeriod; |
925 |
|
thread_local struct soiQuickExplain__option_t soiQuickExplain; |
926 |
|
thread_local struct arithStandardCheckVarOrderPivots__option_t arithStandardCheckVarOrderPivots; |
927 |
|
thread_local struct arithUnateLemmaMode__option_t arithUnateLemmaMode; |
928 |
|
thread_local struct useApprox__option_t useApprox; |
929 |
|
thread_local struct useFC__option_t useFC; |
930 |
|
thread_local struct useSOI__option_t useSOI; |
931 |
|
|
932 |
|
|
933 |
|
std::ostream& operator<<(std::ostream& os, ArithPropagationMode mode) |
934 |
|
{ |
935 |
|
switch(mode) { |
936 |
|
case ArithPropagationMode::BOTH_PROP: |
937 |
|
return os << "ArithPropagationMode::BOTH_PROP"; |
938 |
|
case ArithPropagationMode::NO_PROP: |
939 |
|
return os << "ArithPropagationMode::NO_PROP"; |
940 |
|
case ArithPropagationMode::UNATE_PROP: |
941 |
|
return os << "ArithPropagationMode::UNATE_PROP"; |
942 |
|
case ArithPropagationMode::BOUND_INFERENCE_PROP: |
943 |
|
return os << "ArithPropagationMode::BOUND_INFERENCE_PROP"; |
944 |
|
default: |
945 |
|
Unreachable(); |
946 |
|
} |
947 |
|
return os; |
948 |
|
} |
949 |
|
|
950 |
|
ArithPropagationMode stringToArithPropagationMode(const std::string& optarg) |
951 |
|
{ |
952 |
|
if (optarg == "both") |
953 |
|
{ |
954 |
|
return ArithPropagationMode::BOTH_PROP; |
955 |
|
} |
956 |
|
else if (optarg == "none") |
957 |
|
{ |
958 |
|
return ArithPropagationMode::NO_PROP; |
959 |
|
} |
960 |
|
else if (optarg == "unate") |
961 |
|
{ |
962 |
|
return ArithPropagationMode::UNATE_PROP; |
963 |
|
} |
964 |
|
else if (optarg == "bi") |
965 |
|
{ |
966 |
|
return ArithPropagationMode::BOUND_INFERENCE_PROP; |
967 |
|
} |
968 |
|
else if (optarg == "help") |
969 |
|
{ |
970 |
|
std::cerr << "This decides on kind of propagation arithmetic attempts to do during the\n" |
971 |
|
"search.\n" |
972 |
|
"Available modes for --arith-prop are:\n" |
973 |
|
"+ both (default)\n" |
974 |
|
" Use bounds inference and unate.\n" |
975 |
|
"+ none\n" |
976 |
|
"+ unate\n" |
977 |
|
" Use constraints to do unate propagation.\n" |
978 |
|
"+ bi\n" |
979 |
|
" (Bounds Inference) infers bounds on basic variables using the upper and lower\n" |
980 |
|
" bounds of the non-basic variables in the tableau.\n"; |
981 |
|
std::exit(1); |
982 |
|
} |
983 |
|
throw OptionException(std::string("unknown option for --arith-prop: `") + |
984 |
|
optarg + "'. Try --arith-prop=help."); |
985 |
|
} |
986 |
|
|
987 |
|
std::ostream& operator<<(std::ostream& os, ErrorSelectionRule mode) |
988 |
|
{ |
989 |
|
switch(mode) { |
990 |
|
case ErrorSelectionRule::VAR_ORDER: |
991 |
|
return os << "ErrorSelectionRule::VAR_ORDER"; |
992 |
|
case ErrorSelectionRule::MAXIMUM_AMOUNT: |
993 |
|
return os << "ErrorSelectionRule::MAXIMUM_AMOUNT"; |
994 |
|
case ErrorSelectionRule::MINIMUM_AMOUNT: |
995 |
|
return os << "ErrorSelectionRule::MINIMUM_AMOUNT"; |
996 |
|
case ErrorSelectionRule::SUM_METRIC: |
997 |
|
return os << "ErrorSelectionRule::SUM_METRIC"; |
998 |
|
default: |
999 |
|
Unreachable(); |
1000 |
|
} |
1001 |
|
return os; |
1002 |
|
} |
1003 |
|
|
1004 |
|
ErrorSelectionRule stringToErrorSelectionRule(const std::string& optarg) |
1005 |
|
{ |
1006 |
|
if (optarg == "varord") |
1007 |
|
{ |
1008 |
|
return ErrorSelectionRule::VAR_ORDER; |
1009 |
|
} |
1010 |
|
else if (optarg == "max") |
1011 |
|
{ |
1012 |
|
return ErrorSelectionRule::MAXIMUM_AMOUNT; |
1013 |
|
} |
1014 |
|
else if (optarg == "min") |
1015 |
|
{ |
1016 |
|
return ErrorSelectionRule::MINIMUM_AMOUNT; |
1017 |
|
} |
1018 |
|
else if (optarg == "sum") |
1019 |
|
{ |
1020 |
|
return ErrorSelectionRule::SUM_METRIC; |
1021 |
|
} |
1022 |
|
else if (optarg == "help") |
1023 |
|
{ |
1024 |
|
std::cerr << "This decides on the rule used by simplex during heuristic rounds for deciding\n" |
1025 |
|
"the next basic variable to select.\n" |
1026 |
|
"Available modes for --error-selection-rule are:\n" |
1027 |
|
"+ varord\n" |
1028 |
|
" The variable order.\n" |
1029 |
|
"+ max\n" |
1030 |
|
" The maximum violation the bound.\n" |
1031 |
|
"+ min (default)\n" |
1032 |
|
" The minimum abs() value of the variable's violation of its bound.\n" |
1033 |
|
"+ sum\n"; |
1034 |
|
std::exit(1); |
1035 |
|
} |
1036 |
|
throw OptionException(std::string("unknown option for --error-selection-rule: `") + |
1037 |
|
optarg + "'. Try --error-selection-rule=help."); |
1038 |
|
} |
1039 |
|
|
1040 |
|
std::ostream& operator<<(std::ostream& os, NlExtMode mode) |
1041 |
|
{ |
1042 |
|
switch(mode) { |
1043 |
|
case NlExtMode::NONE: |
1044 |
|
return os << "NlExtMode::NONE"; |
1045 |
|
case NlExtMode::LIGHT: |
1046 |
|
return os << "NlExtMode::LIGHT"; |
1047 |
|
case NlExtMode::FULL: |
1048 |
|
return os << "NlExtMode::FULL"; |
1049 |
|
default: |
1050 |
|
Unreachable(); |
1051 |
|
} |
1052 |
|
return os; |
1053 |
|
} |
1054 |
|
|
1055 |
128 |
NlExtMode stringToNlExtMode(const std::string& optarg) |
1056 |
|
{ |
1057 |
128 |
if (optarg == "none") |
1058 |
|
{ |
1059 |
7 |
return NlExtMode::NONE; |
1060 |
|
} |
1061 |
121 |
else if (optarg == "light") |
1062 |
|
{ |
1063 |
|
return NlExtMode::LIGHT; |
1064 |
|
} |
1065 |
121 |
else if (optarg == "full") |
1066 |
|
{ |
1067 |
121 |
return NlExtMode::FULL; |
1068 |
|
} |
1069 |
|
else if (optarg == "help") |
1070 |
|
{ |
1071 |
|
std::cerr << "Modes for the non-linear linearization\n" |
1072 |
|
"Available modes for --nl-ext are:\n" |
1073 |
|
"+ none\n" |
1074 |
|
" Disable linearization approach\n" |
1075 |
|
"+ light\n" |
1076 |
|
" Only use a few light-weight lemma schemes\n" |
1077 |
|
"+ full (default)\n" |
1078 |
|
" Use all lemma schemes\n"; |
1079 |
|
std::exit(1); |
1080 |
|
} |
1081 |
|
throw OptionException(std::string("unknown option for --nl-ext: `") + |
1082 |
|
optarg + "'. Try --nl-ext=help."); |
1083 |
|
} |
1084 |
|
|
1085 |
|
std::ostream& operator<<(std::ostream& os, NlRlvMode mode) |
1086 |
|
{ |
1087 |
|
switch(mode) { |
1088 |
|
case NlRlvMode::NONE: |
1089 |
|
return os << "NlRlvMode::NONE"; |
1090 |
|
case NlRlvMode::ALWAYS: |
1091 |
|
return os << "NlRlvMode::ALWAYS"; |
1092 |
|
case NlRlvMode::INTERLEAVE: |
1093 |
|
return os << "NlRlvMode::INTERLEAVE"; |
1094 |
|
default: |
1095 |
|
Unreachable(); |
1096 |
|
} |
1097 |
|
return os; |
1098 |
|
} |
1099 |
|
|
1100 |
10 |
NlRlvMode stringToNlRlvMode(const std::string& optarg) |
1101 |
|
{ |
1102 |
10 |
if (optarg == "none") |
1103 |
|
{ |
1104 |
3 |
return NlRlvMode::NONE; |
1105 |
|
} |
1106 |
7 |
else if (optarg == "always") |
1107 |
|
{ |
1108 |
7 |
return NlRlvMode::ALWAYS; |
1109 |
|
} |
1110 |
|
else if (optarg == "interleave") |
1111 |
|
{ |
1112 |
|
return NlRlvMode::INTERLEAVE; |
1113 |
|
} |
1114 |
|
else if (optarg == "help") |
1115 |
|
{ |
1116 |
|
std::cerr << "Modes for using relevance of assertoins in non-linear arithmetic.\n" |
1117 |
|
"Available modes for --nl-rlv are:\n" |
1118 |
|
"+ none (default)\n" |
1119 |
|
" Do not use relevance.\n" |
1120 |
|
"+ always\n" |
1121 |
|
" Always use relevance.\n" |
1122 |
|
"+ interleave\n" |
1123 |
|
" Alternate rounds using relevance.\n"; |
1124 |
|
std::exit(1); |
1125 |
|
} |
1126 |
|
throw OptionException(std::string("unknown option for --nl-rlv: `") + |
1127 |
|
optarg + "'. Try --nl-rlv=help."); |
1128 |
|
} |
1129 |
|
|
1130 |
|
std::ostream& operator<<(std::ostream& os, ArithUnateLemmaMode mode) |
1131 |
|
{ |
1132 |
|
switch(mode) { |
1133 |
|
case ArithUnateLemmaMode::ALL: |
1134 |
|
return os << "ArithUnateLemmaMode::ALL"; |
1135 |
|
case ArithUnateLemmaMode::NO: |
1136 |
|
return os << "ArithUnateLemmaMode::NO"; |
1137 |
|
case ArithUnateLemmaMode::EQUALITY: |
1138 |
|
return os << "ArithUnateLemmaMode::EQUALITY"; |
1139 |
|
case ArithUnateLemmaMode::INEQUALITY: |
1140 |
|
return os << "ArithUnateLemmaMode::INEQUALITY"; |
1141 |
|
default: |
1142 |
|
Unreachable(); |
1143 |
|
} |
1144 |
|
return os; |
1145 |
|
} |
1146 |
|
|
1147 |
|
ArithUnateLemmaMode stringToArithUnateLemmaMode(const std::string& optarg) |
1148 |
|
{ |
1149 |
|
if (optarg == "all") |
1150 |
|
{ |
1151 |
|
return ArithUnateLemmaMode::ALL; |
1152 |
|
} |
1153 |
|
else if (optarg == "none") |
1154 |
|
{ |
1155 |
|
return ArithUnateLemmaMode::NO; |
1156 |
|
} |
1157 |
|
else if (optarg == "eqs") |
1158 |
|
{ |
1159 |
|
return ArithUnateLemmaMode::EQUALITY; |
1160 |
|
} |
1161 |
|
else if (optarg == "ineqs") |
1162 |
|
{ |
1163 |
|
return ArithUnateLemmaMode::INEQUALITY; |
1164 |
|
} |
1165 |
|
else if (optarg == "help") |
1166 |
|
{ |
1167 |
|
std::cerr << "Unate lemmas are generated before SAT search begins using the relationship of\n" |
1168 |
|
"constant terms and polynomials.\n" |
1169 |
|
"Available modes for --unate-lemmas are:\n" |
1170 |
|
"+ all (default)\n" |
1171 |
|
" A combination of inequalities and equalities.\n" |
1172 |
|
"+ none\n" |
1173 |
|
"+ eqs\n" |
1174 |
|
" Outputs lemmas of the general forms (= p c) implies (<= p d) for c < d, or (=\n" |
1175 |
|
" p c) implies (not (= p d)) for c != d.\n" |
1176 |
|
"+ ineqs\n" |
1177 |
|
" Outputs lemmas of the general form (<= p c) implies (<= p d) for c < d.\n"; |
1178 |
|
std::exit(1); |
1179 |
|
} |
1180 |
|
throw OptionException(std::string("unknown option for --unate-lemmas: `") + |
1181 |
|
optarg + "'. Try --unate-lemmas=help."); |
1182 |
|
} |
1183 |
|
|
1184 |
|
|
1185 |
|
} // namespace options |
1186 |
28194 |
} // namespace cvc5 |
1187 |
|
// clang-format on |