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 |
|
* Contains code for handling command-line options. |
14 |
|
* |
15 |
|
* For each <module>_options.toml configuration file, mkoptions.py |
16 |
|
* expands this template and generates a <module>_options.h file. |
17 |
|
*/ |
18 |
|
|
19 |
|
#include "cvc5_private.h" |
20 |
|
|
21 |
|
#ifndef CVC5__OPTIONS__ARITH_H |
22 |
|
#define CVC5__OPTIONS__ARITH_H |
23 |
|
|
24 |
|
#include "options/options.h" |
25 |
|
|
26 |
|
// clang-format off |
27 |
|
|
28 |
|
// clang-format on |
29 |
|
|
30 |
|
namespace cvc5 { |
31 |
|
namespace options { |
32 |
|
|
33 |
|
// clang-format off |
34 |
|
|
35 |
|
enum class ArithPropagationMode |
36 |
|
{ |
37 |
|
UNATE_PROP, |
38 |
|
BOUND_INFERENCE_PROP, |
39 |
|
NO_PROP, |
40 |
|
BOTH_PROP |
41 |
|
}; |
42 |
|
std::ostream& operator<<(std::ostream& os, ArithPropagationMode mode); |
43 |
|
ArithPropagationMode stringToArithPropagationMode(const std::string& optarg); |
44 |
|
enum class ErrorSelectionRule |
45 |
|
{ |
46 |
|
MINIMUM_AMOUNT, |
47 |
|
VAR_ORDER, |
48 |
|
SUM_METRIC, |
49 |
|
MAXIMUM_AMOUNT |
50 |
|
}; |
51 |
|
std::ostream& operator<<(std::ostream& os, ErrorSelectionRule mode); |
52 |
|
ErrorSelectionRule stringToErrorSelectionRule(const std::string& optarg); |
53 |
|
enum class NlExtMode |
54 |
|
{ |
55 |
|
NONE, |
56 |
|
FULL, |
57 |
|
LIGHT |
58 |
|
}; |
59 |
|
std::ostream& operator<<(std::ostream& os, NlExtMode mode); |
60 |
|
NlExtMode stringToNlExtMode(const std::string& optarg); |
61 |
|
enum class NlRlvMode |
62 |
|
{ |
63 |
|
NONE, |
64 |
|
ALWAYS, |
65 |
|
INTERLEAVE |
66 |
|
}; |
67 |
|
std::ostream& operator<<(std::ostream& os, NlRlvMode mode); |
68 |
|
NlRlvMode stringToNlRlvMode(const std::string& optarg); |
69 |
|
enum class ArithUnateLemmaMode |
70 |
|
{ |
71 |
|
NO, |
72 |
|
EQUALITY, |
73 |
|
INEQUALITY, |
74 |
|
ALL |
75 |
|
}; |
76 |
|
std::ostream& operator<<(std::ostream& os, ArithUnateLemmaMode mode); |
77 |
|
ArithUnateLemmaMode stringToArithUnateLemmaMode(const std::string& optarg); |
78 |
|
// clang-format on |
79 |
|
|
80 |
|
#if defined(CVC5_MUZZLED) || defined(CVC5_COMPETITION_MODE) |
81 |
|
# define DO_SEMANTIC_CHECKS_BY_DEFAULT false |
82 |
|
#else /* CVC5_MUZZLED || CVC5_COMPETITION_MODE */ |
83 |
|
# define DO_SEMANTIC_CHECKS_BY_DEFAULT true |
84 |
|
#endif /* CVC5_MUZZLED || CVC5_COMPETITION_MODE */ |
85 |
|
|
86 |
24449 |
struct HolderARITH |
87 |
|
{ |
88 |
|
// clang-format off |
89 |
|
int16_t maxApproxDepth = 200;\ |
90 |
|
bool maxApproxDepth__setByUser__ = false; |
91 |
|
bool brabTest = true;\ |
92 |
|
bool brabTest__setByUser__ = false; |
93 |
|
bool arithNoPartialFun = false;\ |
94 |
|
bool arithNoPartialFun__setByUser__ = false; |
95 |
|
uint16_t arithPropAsLemmaLength = 8;\ |
96 |
|
bool arithPropAsLemmaLength__setByUser__ = false; |
97 |
|
ArithPropagationMode arithPropagationMode = ArithPropagationMode::BOTH_PROP;\ |
98 |
|
bool arithPropagationMode__setByUser__ = false; |
99 |
|
bool arithRewriteEq = false;\ |
100 |
|
bool arithRewriteEq__setByUser__ = false; |
101 |
|
bool collectPivots = false;\ |
102 |
|
bool collectPivots__setByUser__ = false; |
103 |
|
bool doCutAllBounded = false;\ |
104 |
|
bool doCutAllBounded__setByUser__ = false; |
105 |
|
bool exportDioDecompositions = false;\ |
106 |
|
bool exportDioDecompositions__setByUser__ = false; |
107 |
|
bool dioRepeat = false;\ |
108 |
|
bool dioRepeat__setByUser__ = false; |
109 |
|
bool arithDioSolver = true;\ |
110 |
|
bool arithDioSolver__setByUser__ = false; |
111 |
|
int dioSolverTurns = 10;\ |
112 |
|
bool dioSolverTurns__setByUser__ = false; |
113 |
|
ErrorSelectionRule arithErrorSelectionRule = ErrorSelectionRule::MINIMUM_AMOUNT;\ |
114 |
|
bool arithErrorSelectionRule__setByUser__ = false; |
115 |
|
bool havePenalties = false;\ |
116 |
|
bool havePenalties__setByUser__ = false; |
117 |
|
int16_t arithHeuristicPivots = 0;\ |
118 |
|
bool arithHeuristicPivots__setByUser__ = false; |
119 |
|
bool replayFailureLemma = false;\ |
120 |
|
bool replayFailureLemma__setByUser__ = false; |
121 |
|
unsigned maxCutsInContext = 65535;\ |
122 |
|
bool maxCutsInContext__setByUser__ = false; |
123 |
|
bool arithMLTrick = false;\ |
124 |
|
bool arithMLTrick__setByUser__ = false; |
125 |
|
unsigned arithMLTrickSubstitutions = 1;\ |
126 |
|
bool arithMLTrickSubstitutions__setByUser__ = false; |
127 |
|
bool newProp = true;\ |
128 |
|
bool newProp__setByUser__ = false; |
129 |
|
bool nlCad = false;\ |
130 |
|
bool nlCad__setByUser__ = false; |
131 |
|
bool nlCadUseInitial = false;\ |
132 |
|
bool nlCadUseInitial__setByUser__ = false; |
133 |
|
bool nlExtEntailConflicts = false;\ |
134 |
|
bool nlExtEntailConflicts__setByUser__ = false; |
135 |
|
bool nlExtFactor = true;\ |
136 |
|
bool nlExtFactor__setByUser__ = false; |
137 |
|
bool nlExtIncPrecision = true;\ |
138 |
|
bool nlExtIncPrecision__setByUser__ = false; |
139 |
|
bool nlExtPurify = false;\ |
140 |
|
bool nlExtPurify__setByUser__ = false; |
141 |
|
bool nlExtResBound = false;\ |
142 |
|
bool nlExtResBound__setByUser__ = false; |
143 |
|
bool nlExtRewrites = true;\ |
144 |
|
bool nlExtRewrites__setByUser__ = false; |
145 |
|
bool nlExtSplitZero = false;\ |
146 |
|
bool nlExtSplitZero__setByUser__ = false; |
147 |
|
int16_t nlExtTfTaylorDegree = 4;\ |
148 |
|
bool nlExtTfTaylorDegree__setByUser__ = false; |
149 |
|
bool nlExtTfTangentPlanes = true;\ |
150 |
|
bool nlExtTfTangentPlanes__setByUser__ = false; |
151 |
|
bool nlExtTangentPlanes = false;\ |
152 |
|
bool nlExtTangentPlanes__setByUser__ = false; |
153 |
|
bool nlExtTangentPlanesInterleave = false;\ |
154 |
|
bool nlExtTangentPlanesInterleave__setByUser__ = false; |
155 |
|
NlExtMode nlExt = NlExtMode::FULL;\ |
156 |
|
bool nlExt__setByUser__ = false; |
157 |
|
bool nlICP = false;\ |
158 |
|
bool nlICP__setByUser__ = false; |
159 |
|
NlRlvMode nlRlvMode = NlRlvMode::NONE;\ |
160 |
|
bool nlRlvMode__setByUser__ = false; |
161 |
|
bool pbRewrites = false;\ |
162 |
|
bool pbRewrites__setByUser__ = false; |
163 |
|
uint16_t arithPivotThreshold = 2;\ |
164 |
|
bool arithPivotThreshold__setByUser__ = false; |
165 |
|
unsigned ppAssertMaxSubSize = 2;\ |
166 |
|
bool ppAssertMaxSubSize__setByUser__ = false; |
167 |
|
uint16_t arithPropagateMaxLength = 16;\ |
168 |
|
bool arithPropagateMaxLength__setByUser__ = false; |
169 |
|
int replayEarlyCloseDepths = 1;\ |
170 |
|
bool replayEarlyCloseDepths__setByUser__ = false; |
171 |
|
int replayFailurePenalty = 100;\ |
172 |
|
bool replayFailurePenalty__setByUser__ = false; |
173 |
|
unsigned lemmaRejectCutSize = 25500;\ |
174 |
|
bool lemmaRejectCutSize__setByUser__ = false; |
175 |
|
int replayNumericFailurePenalty = 4194304;\ |
176 |
|
bool replayNumericFailurePenalty__setByUser__ = false; |
177 |
|
unsigned replayRejectCutSize = 25500;\ |
178 |
|
bool replayRejectCutSize__setByUser__ = false; |
179 |
|
int soiApproxMajorFailurePen = 50;\ |
180 |
|
bool soiApproxMajorFailurePen__setByUser__ = false; |
181 |
|
double soiApproxMajorFailure = .01;\ |
182 |
|
bool soiApproxMajorFailure__setByUser__ = false; |
183 |
|
int soiApproxMinorFailurePen = 10;\ |
184 |
|
bool soiApproxMinorFailurePen__setByUser__ = false; |
185 |
|
double soiApproxMinorFailure = .0001;\ |
186 |
|
bool soiApproxMinorFailure__setByUser__ = false; |
187 |
|
bool restrictedPivots = true;\ |
188 |
|
bool restrictedPivots__setByUser__ = false; |
189 |
|
bool revertArithModels = false;\ |
190 |
|
bool revertArithModels__setByUser__ = false; |
191 |
|
int rrTurns = 3;\ |
192 |
|
bool rrTurns__setByUser__ = false; |
193 |
|
bool trySolveIntStandardEffort = false;\ |
194 |
|
bool trySolveIntStandardEffort__setByUser__ = false; |
195 |
|
uint16_t arithSimplexCheckPeriod = 200;\ |
196 |
|
bool arithSimplexCheckPeriod__setByUser__ = false; |
197 |
|
bool soiQuickExplain = false;\ |
198 |
|
bool soiQuickExplain__setByUser__ = false; |
199 |
|
int16_t arithStandardCheckVarOrderPivots = -1;\ |
200 |
|
bool arithStandardCheckVarOrderPivots__setByUser__ = false; |
201 |
|
ArithUnateLemmaMode arithUnateLemmaMode = ArithUnateLemmaMode::ALL;\ |
202 |
|
bool arithUnateLemmaMode__setByUser__ = false; |
203 |
|
bool useApprox = false;\ |
204 |
|
bool useApprox__setByUser__ = false; |
205 |
|
bool useFC = false;\ |
206 |
|
bool useFC__setByUser__ = false; |
207 |
|
bool useSOI = false;\ |
208 |
|
bool useSOI__setByUser__ = false; |
209 |
|
// clang-format on |
210 |
|
}; |
211 |
|
|
212 |
|
#undef DO_SEMANTIC_CHECKS_BY_DEFAULT |
213 |
|
|
214 |
|
// clang-format off |
215 |
|
extern struct maxApproxDepth__option_t |
216 |
|
{ |
217 |
|
typedef int16_t type; |
218 |
|
type operator()() const; |
219 |
|
} thread_local maxApproxDepth; |
220 |
|
extern struct brabTest__option_t |
221 |
|
{ |
222 |
|
typedef bool type; |
223 |
|
type operator()() const; |
224 |
|
} thread_local brabTest; |
225 |
|
extern struct arithNoPartialFun__option_t |
226 |
|
{ |
227 |
|
typedef bool type; |
228 |
|
type operator()() const; |
229 |
|
} thread_local arithNoPartialFun; |
230 |
|
extern struct arithPropAsLemmaLength__option_t |
231 |
|
{ |
232 |
|
typedef uint16_t type; |
233 |
|
type operator()() const; |
234 |
|
} thread_local arithPropAsLemmaLength; |
235 |
|
extern struct arithPropagationMode__option_t |
236 |
|
{ |
237 |
|
typedef ArithPropagationMode type; |
238 |
|
type operator()() const; |
239 |
|
} thread_local arithPropagationMode; |
240 |
|
extern struct arithRewriteEq__option_t |
241 |
|
{ |
242 |
|
typedef bool type; |
243 |
|
type operator()() const; |
244 |
|
} thread_local arithRewriteEq; |
245 |
|
extern struct collectPivots__option_t |
246 |
|
{ |
247 |
|
typedef bool type; |
248 |
|
type operator()() const; |
249 |
|
} thread_local collectPivots; |
250 |
|
extern struct doCutAllBounded__option_t |
251 |
|
{ |
252 |
|
typedef bool type; |
253 |
|
type operator()() const; |
254 |
|
} thread_local doCutAllBounded; |
255 |
|
extern struct exportDioDecompositions__option_t |
256 |
|
{ |
257 |
|
typedef bool type; |
258 |
|
type operator()() const; |
259 |
|
} thread_local exportDioDecompositions; |
260 |
|
extern struct dioRepeat__option_t |
261 |
|
{ |
262 |
|
typedef bool type; |
263 |
|
type operator()() const; |
264 |
|
} thread_local dioRepeat; |
265 |
|
extern struct arithDioSolver__option_t |
266 |
|
{ |
267 |
|
typedef bool type; |
268 |
|
type operator()() const; |
269 |
|
} thread_local arithDioSolver; |
270 |
|
extern struct dioSolverTurns__option_t |
271 |
|
{ |
272 |
|
typedef int type; |
273 |
|
type operator()() const; |
274 |
|
} thread_local dioSolverTurns; |
275 |
|
extern struct arithErrorSelectionRule__option_t |
276 |
|
{ |
277 |
|
typedef ErrorSelectionRule type; |
278 |
|
type operator()() const; |
279 |
|
} thread_local arithErrorSelectionRule; |
280 |
|
extern struct havePenalties__option_t |
281 |
|
{ |
282 |
|
typedef bool type; |
283 |
|
type operator()() const; |
284 |
|
} thread_local havePenalties; |
285 |
|
extern struct arithHeuristicPivots__option_t |
286 |
|
{ |
287 |
|
typedef int16_t type; |
288 |
|
type operator()() const; |
289 |
|
} thread_local arithHeuristicPivots; |
290 |
|
extern struct replayFailureLemma__option_t |
291 |
|
{ |
292 |
|
typedef bool type; |
293 |
|
type operator()() const; |
294 |
|
} thread_local replayFailureLemma; |
295 |
|
extern struct maxCutsInContext__option_t |
296 |
|
{ |
297 |
|
typedef unsigned type; |
298 |
|
type operator()() const; |
299 |
|
} thread_local maxCutsInContext; |
300 |
|
extern struct arithMLTrick__option_t |
301 |
|
{ |
302 |
|
typedef bool type; |
303 |
|
type operator()() const; |
304 |
|
} thread_local arithMLTrick; |
305 |
|
extern struct arithMLTrickSubstitutions__option_t |
306 |
|
{ |
307 |
|
typedef unsigned type; |
308 |
|
type operator()() const; |
309 |
|
} thread_local arithMLTrickSubstitutions; |
310 |
|
extern struct newProp__option_t |
311 |
|
{ |
312 |
|
typedef bool type; |
313 |
|
type operator()() const; |
314 |
|
} thread_local newProp; |
315 |
|
extern struct nlCad__option_t |
316 |
|
{ |
317 |
|
typedef bool type; |
318 |
|
type operator()() const; |
319 |
|
} thread_local nlCad; |
320 |
|
extern struct nlCadUseInitial__option_t |
321 |
|
{ |
322 |
|
typedef bool type; |
323 |
|
type operator()() const; |
324 |
|
} thread_local nlCadUseInitial; |
325 |
|
extern struct nlExtEntailConflicts__option_t |
326 |
|
{ |
327 |
|
typedef bool type; |
328 |
|
type operator()() const; |
329 |
|
} thread_local nlExtEntailConflicts; |
330 |
|
extern struct nlExtFactor__option_t |
331 |
|
{ |
332 |
|
typedef bool type; |
333 |
|
type operator()() const; |
334 |
|
} thread_local nlExtFactor; |
335 |
|
extern struct nlExtIncPrecision__option_t |
336 |
|
{ |
337 |
|
typedef bool type; |
338 |
|
type operator()() const; |
339 |
|
} thread_local nlExtIncPrecision; |
340 |
|
extern struct nlExtPurify__option_t |
341 |
|
{ |
342 |
|
typedef bool type; |
343 |
|
type operator()() const; |
344 |
|
} thread_local nlExtPurify; |
345 |
|
extern struct nlExtResBound__option_t |
346 |
|
{ |
347 |
|
typedef bool type; |
348 |
|
type operator()() const; |
349 |
|
} thread_local nlExtResBound; |
350 |
|
extern struct nlExtRewrites__option_t |
351 |
|
{ |
352 |
|
typedef bool type; |
353 |
|
type operator()() const; |
354 |
|
} thread_local nlExtRewrites; |
355 |
|
extern struct nlExtSplitZero__option_t |
356 |
|
{ |
357 |
|
typedef bool type; |
358 |
|
type operator()() const; |
359 |
|
} thread_local nlExtSplitZero; |
360 |
|
extern struct nlExtTfTaylorDegree__option_t |
361 |
|
{ |
362 |
|
typedef int16_t type; |
363 |
|
type operator()() const; |
364 |
|
} thread_local nlExtTfTaylorDegree; |
365 |
|
extern struct nlExtTfTangentPlanes__option_t |
366 |
|
{ |
367 |
|
typedef bool type; |
368 |
|
type operator()() const; |
369 |
|
} thread_local nlExtTfTangentPlanes; |
370 |
|
extern struct nlExtTangentPlanes__option_t |
371 |
|
{ |
372 |
|
typedef bool type; |
373 |
|
type operator()() const; |
374 |
|
} thread_local nlExtTangentPlanes; |
375 |
|
extern struct nlExtTangentPlanesInterleave__option_t |
376 |
|
{ |
377 |
|
typedef bool type; |
378 |
|
type operator()() const; |
379 |
|
} thread_local nlExtTangentPlanesInterleave; |
380 |
|
extern struct nlExt__option_t |
381 |
|
{ |
382 |
|
typedef NlExtMode type; |
383 |
|
type operator()() const; |
384 |
|
} thread_local nlExt; |
385 |
|
extern struct nlICP__option_t |
386 |
|
{ |
387 |
|
typedef bool type; |
388 |
|
type operator()() const; |
389 |
|
} thread_local nlICP; |
390 |
|
extern struct nlRlvMode__option_t |
391 |
|
{ |
392 |
|
typedef NlRlvMode type; |
393 |
|
type operator()() const; |
394 |
|
} thread_local nlRlvMode; |
395 |
|
extern struct pbRewrites__option_t |
396 |
|
{ |
397 |
|
typedef bool type; |
398 |
|
type operator()() const; |
399 |
|
} thread_local pbRewrites; |
400 |
|
extern struct arithPivotThreshold__option_t |
401 |
|
{ |
402 |
|
typedef uint16_t type; |
403 |
|
type operator()() const; |
404 |
|
} thread_local arithPivotThreshold; |
405 |
|
extern struct ppAssertMaxSubSize__option_t |
406 |
|
{ |
407 |
|
typedef unsigned type; |
408 |
|
type operator()() const; |
409 |
|
} thread_local ppAssertMaxSubSize; |
410 |
|
extern struct arithPropagateMaxLength__option_t |
411 |
|
{ |
412 |
|
typedef uint16_t type; |
413 |
|
type operator()() const; |
414 |
|
} thread_local arithPropagateMaxLength; |
415 |
|
extern struct replayEarlyCloseDepths__option_t |
416 |
|
{ |
417 |
|
typedef int type; |
418 |
|
type operator()() const; |
419 |
|
} thread_local replayEarlyCloseDepths; |
420 |
|
extern struct replayFailurePenalty__option_t |
421 |
|
{ |
422 |
|
typedef int type; |
423 |
|
type operator()() const; |
424 |
|
} thread_local replayFailurePenalty; |
425 |
|
extern struct lemmaRejectCutSize__option_t |
426 |
|
{ |
427 |
|
typedef unsigned type; |
428 |
|
type operator()() const; |
429 |
|
} thread_local lemmaRejectCutSize; |
430 |
|
extern struct replayNumericFailurePenalty__option_t |
431 |
|
{ |
432 |
|
typedef int type; |
433 |
|
type operator()() const; |
434 |
|
} thread_local replayNumericFailurePenalty; |
435 |
|
extern struct replayRejectCutSize__option_t |
436 |
|
{ |
437 |
|
typedef unsigned type; |
438 |
|
type operator()() const; |
439 |
|
} thread_local replayRejectCutSize; |
440 |
|
extern struct soiApproxMajorFailurePen__option_t |
441 |
|
{ |
442 |
|
typedef int type; |
443 |
|
type operator()() const; |
444 |
|
} thread_local soiApproxMajorFailurePen; |
445 |
|
extern struct soiApproxMajorFailure__option_t |
446 |
|
{ |
447 |
|
typedef double type; |
448 |
|
type operator()() const; |
449 |
|
} thread_local soiApproxMajorFailure; |
450 |
|
extern struct soiApproxMinorFailurePen__option_t |
451 |
|
{ |
452 |
|
typedef int type; |
453 |
|
type operator()() const; |
454 |
|
} thread_local soiApproxMinorFailurePen; |
455 |
|
extern struct soiApproxMinorFailure__option_t |
456 |
|
{ |
457 |
|
typedef double type; |
458 |
|
type operator()() const; |
459 |
|
} thread_local soiApproxMinorFailure; |
460 |
|
extern struct restrictedPivots__option_t |
461 |
|
{ |
462 |
|
typedef bool type; |
463 |
|
type operator()() const; |
464 |
|
} thread_local restrictedPivots; |
465 |
|
extern struct revertArithModels__option_t |
466 |
|
{ |
467 |
|
typedef bool type; |
468 |
|
type operator()() const; |
469 |
|
} thread_local revertArithModels; |
470 |
|
extern struct rrTurns__option_t |
471 |
|
{ |
472 |
|
typedef int type; |
473 |
|
type operator()() const; |
474 |
|
} thread_local rrTurns; |
475 |
|
extern struct trySolveIntStandardEffort__option_t |
476 |
|
{ |
477 |
|
typedef bool type; |
478 |
|
type operator()() const; |
479 |
|
} thread_local trySolveIntStandardEffort; |
480 |
|
extern struct arithSimplexCheckPeriod__option_t |
481 |
|
{ |
482 |
|
typedef uint16_t type; |
483 |
|
type operator()() const; |
484 |
|
} thread_local arithSimplexCheckPeriod; |
485 |
|
extern struct soiQuickExplain__option_t |
486 |
|
{ |
487 |
|
typedef bool type; |
488 |
|
type operator()() const; |
489 |
|
} thread_local soiQuickExplain; |
490 |
|
extern struct arithStandardCheckVarOrderPivots__option_t |
491 |
|
{ |
492 |
|
typedef int16_t type; |
493 |
|
type operator()() const; |
494 |
|
} thread_local arithStandardCheckVarOrderPivots; |
495 |
|
extern struct arithUnateLemmaMode__option_t |
496 |
|
{ |
497 |
|
typedef ArithUnateLemmaMode type; |
498 |
|
type operator()() const; |
499 |
|
} thread_local arithUnateLemmaMode; |
500 |
|
extern struct useApprox__option_t |
501 |
|
{ |
502 |
|
typedef bool type; |
503 |
|
type operator()() const; |
504 |
|
} thread_local useApprox; |
505 |
|
extern struct useFC__option_t |
506 |
|
{ |
507 |
|
typedef bool type; |
508 |
|
type operator()() const; |
509 |
|
} thread_local useFC; |
510 |
|
extern struct useSOI__option_t |
511 |
|
{ |
512 |
|
typedef bool type; |
513 |
|
type operator()() const; |
514 |
|
} thread_local useSOI; |
515 |
|
// clang-format on |
516 |
|
|
517 |
|
namespace arith |
518 |
|
{ |
519 |
|
// clang-format off |
520 |
|
static constexpr const char* maxApproxDepth__name = "approx-branch-depth"; |
521 |
|
static constexpr const char* brabTest__name = "arith-brab"; |
522 |
|
static constexpr const char* arithNoPartialFun__name = "arith-no-partial-fun"; |
523 |
|
static constexpr const char* arithPropAsLemmaLength__name = "arith-prop-clauses"; |
524 |
|
static constexpr const char* arithPropagationMode__name = "arith-prop"; |
525 |
|
static constexpr const char* arithRewriteEq__name = "arith-rewrite-equalities"; |
526 |
|
static constexpr const char* collectPivots__name = "collect-pivot-stats"; |
527 |
|
static constexpr const char* doCutAllBounded__name = "cut-all-bounded"; |
528 |
|
static constexpr const char* exportDioDecompositions__name = "dio-decomps"; |
529 |
|
static constexpr const char* dioRepeat__name = "dio-repeat"; |
530 |
|
static constexpr const char* arithDioSolver__name = "dio-solver"; |
531 |
|
static constexpr const char* dioSolverTurns__name = "dio-turns"; |
532 |
|
static constexpr const char* arithErrorSelectionRule__name = "error-selection-rule"; |
533 |
|
static constexpr const char* havePenalties__name = "fc-penalties"; |
534 |
|
static constexpr const char* arithHeuristicPivots__name = "heuristic-pivots"; |
535 |
|
static constexpr const char* replayFailureLemma__name = "lemmas-on-replay-failure"; |
536 |
|
static constexpr const char* maxCutsInContext__name = "maxCutsInContext"; |
537 |
|
static constexpr const char* arithMLTrick__name = "miplib-trick"; |
538 |
|
static constexpr const char* arithMLTrickSubstitutions__name = "miplib-trick-subs"; |
539 |
|
static constexpr const char* newProp__name = "new-prop"; |
540 |
|
static constexpr const char* nlCad__name = "nl-cad"; |
541 |
|
static constexpr const char* nlCadUseInitial__name = "nl-cad-initial"; |
542 |
|
static constexpr const char* nlExtEntailConflicts__name = "nl-ext-ent-conf"; |
543 |
|
static constexpr const char* nlExtFactor__name = "nl-ext-factor"; |
544 |
|
static constexpr const char* nlExtIncPrecision__name = "nl-ext-inc-prec"; |
545 |
|
static constexpr const char* nlExtPurify__name = "nl-ext-purify"; |
546 |
|
static constexpr const char* nlExtResBound__name = "nl-ext-rbound"; |
547 |
|
static constexpr const char* nlExtRewrites__name = "nl-ext-rewrite"; |
548 |
|
static constexpr const char* nlExtSplitZero__name = "nl-ext-split-zero"; |
549 |
|
static constexpr const char* nlExtTfTaylorDegree__name = "nl-ext-tf-taylor-deg"; |
550 |
|
static constexpr const char* nlExtTfTangentPlanes__name = "nl-ext-tf-tplanes"; |
551 |
|
static constexpr const char* nlExtTangentPlanes__name = "nl-ext-tplanes"; |
552 |
|
static constexpr const char* nlExtTangentPlanesInterleave__name = "nl-ext-tplanes-interleave"; |
553 |
|
static constexpr const char* nlExt__name = "nl-ext"; |
554 |
|
static constexpr const char* nlICP__name = "nl-icp"; |
555 |
|
static constexpr const char* nlRlvMode__name = "nl-rlv"; |
556 |
|
static constexpr const char* pbRewrites__name = "pb-rewrites"; |
557 |
|
static constexpr const char* arithPivotThreshold__name = "pivot-threshold"; |
558 |
|
static constexpr const char* ppAssertMaxSubSize__name = "pp-assert-max-sub-size"; |
559 |
|
static constexpr const char* arithPropagateMaxLength__name = "prop-row-length"; |
560 |
|
static constexpr const char* replayEarlyCloseDepths__name = "replay-early-close-depth"; |
561 |
|
static constexpr const char* replayFailurePenalty__name = "replay-failure-penalty"; |
562 |
|
static constexpr const char* lemmaRejectCutSize__name = "replay-lemma-reject-cut"; |
563 |
|
static constexpr const char* replayNumericFailurePenalty__name = "replay-num-err-penalty"; |
564 |
|
static constexpr const char* replayRejectCutSize__name = "replay-reject-cut"; |
565 |
|
static constexpr const char* soiApproxMajorFailurePen__name = "replay-soi-major-threshold-pen"; |
566 |
|
static constexpr const char* soiApproxMajorFailure__name = "replay-soi-major-threshold"; |
567 |
|
static constexpr const char* soiApproxMinorFailurePen__name = "replay-soi-minor-threshold-pen"; |
568 |
|
static constexpr const char* soiApproxMinorFailure__name = "replay-soi-minor-threshold"; |
569 |
|
static constexpr const char* restrictedPivots__name = "restrict-pivots"; |
570 |
|
static constexpr const char* revertArithModels__name = "revert-arith-models-on-unsat"; |
571 |
|
static constexpr const char* rrTurns__name = "rr-turns"; |
572 |
|
static constexpr const char* trySolveIntStandardEffort__name = "se-solve-int"; |
573 |
|
static constexpr const char* arithSimplexCheckPeriod__name = "simplex-check-period"; |
574 |
|
static constexpr const char* soiQuickExplain__name = "soi-qe"; |
575 |
|
static constexpr const char* arithStandardCheckVarOrderPivots__name = "standard-effort-variable-order-pivots"; |
576 |
|
static constexpr const char* arithUnateLemmaMode__name = "unate-lemmas"; |
577 |
|
static constexpr const char* useApprox__name = "use-approx"; |
578 |
|
static constexpr const char* useFC__name = "use-fcsimplex"; |
579 |
|
static constexpr const char* useSOI__name = "use-soi"; |
580 |
|
// clang-format on |
581 |
|
} |
582 |
|
|
583 |
|
} // namespace options |
584 |
|
|
585 |
|
// clang-format off |
586 |
|
template <> options::maxApproxDepth__option_t::type& Options::ref( |
587 |
|
options::maxApproxDepth__option_t); |
588 |
|
template <> const options::maxApproxDepth__option_t::type& Options::operator[]( |
589 |
|
options::maxApproxDepth__option_t) const; |
590 |
|
template <> bool Options::wasSetByUser(options::maxApproxDepth__option_t) const; |
591 |
|
template <> options::brabTest__option_t::type& Options::ref( |
592 |
|
options::brabTest__option_t); |
593 |
|
template <> const options::brabTest__option_t::type& Options::operator[]( |
594 |
|
options::brabTest__option_t) const; |
595 |
|
template <> bool Options::wasSetByUser(options::brabTest__option_t) const; |
596 |
|
template <> options::arithNoPartialFun__option_t::type& Options::ref( |
597 |
|
options::arithNoPartialFun__option_t); |
598 |
|
template <> const options::arithNoPartialFun__option_t::type& Options::operator[]( |
599 |
|
options::arithNoPartialFun__option_t) const; |
600 |
|
template <> bool Options::wasSetByUser(options::arithNoPartialFun__option_t) const; |
601 |
|
template <> options::arithPropAsLemmaLength__option_t::type& Options::ref( |
602 |
|
options::arithPropAsLemmaLength__option_t); |
603 |
|
template <> const options::arithPropAsLemmaLength__option_t::type& Options::operator[]( |
604 |
|
options::arithPropAsLemmaLength__option_t) const; |
605 |
|
template <> bool Options::wasSetByUser(options::arithPropAsLemmaLength__option_t) const; |
606 |
|
template <> options::arithPropagationMode__option_t::type& Options::ref( |
607 |
|
options::arithPropagationMode__option_t); |
608 |
|
template <> const options::arithPropagationMode__option_t::type& Options::operator[]( |
609 |
|
options::arithPropagationMode__option_t) const; |
610 |
|
template <> bool Options::wasSetByUser(options::arithPropagationMode__option_t) const; |
611 |
|
template <> options::arithRewriteEq__option_t::type& Options::ref( |
612 |
|
options::arithRewriteEq__option_t); |
613 |
|
template <> const options::arithRewriteEq__option_t::type& Options::operator[]( |
614 |
|
options::arithRewriteEq__option_t) const; |
615 |
|
template <> bool Options::wasSetByUser(options::arithRewriteEq__option_t) const; |
616 |
|
template <> options::collectPivots__option_t::type& Options::ref( |
617 |
|
options::collectPivots__option_t); |
618 |
|
template <> const options::collectPivots__option_t::type& Options::operator[]( |
619 |
|
options::collectPivots__option_t) const; |
620 |
|
template <> bool Options::wasSetByUser(options::collectPivots__option_t) const; |
621 |
|
template <> options::doCutAllBounded__option_t::type& Options::ref( |
622 |
|
options::doCutAllBounded__option_t); |
623 |
|
template <> const options::doCutAllBounded__option_t::type& Options::operator[]( |
624 |
|
options::doCutAllBounded__option_t) const; |
625 |
|
template <> bool Options::wasSetByUser(options::doCutAllBounded__option_t) const; |
626 |
|
template <> options::exportDioDecompositions__option_t::type& Options::ref( |
627 |
|
options::exportDioDecompositions__option_t); |
628 |
|
template <> const options::exportDioDecompositions__option_t::type& Options::operator[]( |
629 |
|
options::exportDioDecompositions__option_t) const; |
630 |
|
template <> bool Options::wasSetByUser(options::exportDioDecompositions__option_t) const; |
631 |
|
template <> options::dioRepeat__option_t::type& Options::ref( |
632 |
|
options::dioRepeat__option_t); |
633 |
|
template <> const options::dioRepeat__option_t::type& Options::operator[]( |
634 |
|
options::dioRepeat__option_t) const; |
635 |
|
template <> bool Options::wasSetByUser(options::dioRepeat__option_t) const; |
636 |
|
template <> options::arithDioSolver__option_t::type& Options::ref( |
637 |
|
options::arithDioSolver__option_t); |
638 |
|
template <> const options::arithDioSolver__option_t::type& Options::operator[]( |
639 |
|
options::arithDioSolver__option_t) const; |
640 |
|
template <> bool Options::wasSetByUser(options::arithDioSolver__option_t) const; |
641 |
|
template <> options::dioSolverTurns__option_t::type& Options::ref( |
642 |
|
options::dioSolverTurns__option_t); |
643 |
|
template <> const options::dioSolverTurns__option_t::type& Options::operator[]( |
644 |
|
options::dioSolverTurns__option_t) const; |
645 |
|
template <> bool Options::wasSetByUser(options::dioSolverTurns__option_t) const; |
646 |
|
template <> options::arithErrorSelectionRule__option_t::type& Options::ref( |
647 |
|
options::arithErrorSelectionRule__option_t); |
648 |
|
template <> const options::arithErrorSelectionRule__option_t::type& Options::operator[]( |
649 |
|
options::arithErrorSelectionRule__option_t) const; |
650 |
|
template <> bool Options::wasSetByUser(options::arithErrorSelectionRule__option_t) const; |
651 |
|
template <> options::havePenalties__option_t::type& Options::ref( |
652 |
|
options::havePenalties__option_t); |
653 |
|
template <> const options::havePenalties__option_t::type& Options::operator[]( |
654 |
|
options::havePenalties__option_t) const; |
655 |
|
template <> bool Options::wasSetByUser(options::havePenalties__option_t) const; |
656 |
|
template <> options::arithHeuristicPivots__option_t::type& Options::ref( |
657 |
|
options::arithHeuristicPivots__option_t); |
658 |
|
template <> const options::arithHeuristicPivots__option_t::type& Options::operator[]( |
659 |
|
options::arithHeuristicPivots__option_t) const; |
660 |
|
template <> bool Options::wasSetByUser(options::arithHeuristicPivots__option_t) const; |
661 |
|
template <> options::replayFailureLemma__option_t::type& Options::ref( |
662 |
|
options::replayFailureLemma__option_t); |
663 |
|
template <> const options::replayFailureLemma__option_t::type& Options::operator[]( |
664 |
|
options::replayFailureLemma__option_t) const; |
665 |
|
template <> bool Options::wasSetByUser(options::replayFailureLemma__option_t) const; |
666 |
|
template <> options::maxCutsInContext__option_t::type& Options::ref( |
667 |
|
options::maxCutsInContext__option_t); |
668 |
|
template <> const options::maxCutsInContext__option_t::type& Options::operator[]( |
669 |
|
options::maxCutsInContext__option_t) const; |
670 |
|
template <> bool Options::wasSetByUser(options::maxCutsInContext__option_t) const; |
671 |
|
template <> options::arithMLTrick__option_t::type& Options::ref( |
672 |
|
options::arithMLTrick__option_t); |
673 |
|
template <> const options::arithMLTrick__option_t::type& Options::operator[]( |
674 |
|
options::arithMLTrick__option_t) const; |
675 |
|
template <> bool Options::wasSetByUser(options::arithMLTrick__option_t) const; |
676 |
|
template <> options::arithMLTrickSubstitutions__option_t::type& Options::ref( |
677 |
|
options::arithMLTrickSubstitutions__option_t); |
678 |
|
template <> const options::arithMLTrickSubstitutions__option_t::type& Options::operator[]( |
679 |
|
options::arithMLTrickSubstitutions__option_t) const; |
680 |
|
template <> bool Options::wasSetByUser(options::arithMLTrickSubstitutions__option_t) const; |
681 |
|
template <> options::newProp__option_t::type& Options::ref( |
682 |
|
options::newProp__option_t); |
683 |
|
template <> const options::newProp__option_t::type& Options::operator[]( |
684 |
|
options::newProp__option_t) const; |
685 |
|
template <> bool Options::wasSetByUser(options::newProp__option_t) const; |
686 |
|
template <> options::nlCad__option_t::type& Options::ref( |
687 |
|
options::nlCad__option_t); |
688 |
|
template <> const options::nlCad__option_t::type& Options::operator[]( |
689 |
|
options::nlCad__option_t) const; |
690 |
|
template <> bool Options::wasSetByUser(options::nlCad__option_t) const; |
691 |
|
template <> options::nlCadUseInitial__option_t::type& Options::ref( |
692 |
|
options::nlCadUseInitial__option_t); |
693 |
|
template <> const options::nlCadUseInitial__option_t::type& Options::operator[]( |
694 |
|
options::nlCadUseInitial__option_t) const; |
695 |
|
template <> bool Options::wasSetByUser(options::nlCadUseInitial__option_t) const; |
696 |
|
template <> options::nlExtEntailConflicts__option_t::type& Options::ref( |
697 |
|
options::nlExtEntailConflicts__option_t); |
698 |
|
template <> const options::nlExtEntailConflicts__option_t::type& Options::operator[]( |
699 |
|
options::nlExtEntailConflicts__option_t) const; |
700 |
|
template <> bool Options::wasSetByUser(options::nlExtEntailConflicts__option_t) const; |
701 |
|
template <> options::nlExtFactor__option_t::type& Options::ref( |
702 |
|
options::nlExtFactor__option_t); |
703 |
|
template <> const options::nlExtFactor__option_t::type& Options::operator[]( |
704 |
|
options::nlExtFactor__option_t) const; |
705 |
|
template <> bool Options::wasSetByUser(options::nlExtFactor__option_t) const; |
706 |
|
template <> options::nlExtIncPrecision__option_t::type& Options::ref( |
707 |
|
options::nlExtIncPrecision__option_t); |
708 |
|
template <> const options::nlExtIncPrecision__option_t::type& Options::operator[]( |
709 |
|
options::nlExtIncPrecision__option_t) const; |
710 |
|
template <> bool Options::wasSetByUser(options::nlExtIncPrecision__option_t) const; |
711 |
|
template <> options::nlExtPurify__option_t::type& Options::ref( |
712 |
|
options::nlExtPurify__option_t); |
713 |
|
template <> const options::nlExtPurify__option_t::type& Options::operator[]( |
714 |
|
options::nlExtPurify__option_t) const; |
715 |
|
template <> bool Options::wasSetByUser(options::nlExtPurify__option_t) const; |
716 |
|
template <> options::nlExtResBound__option_t::type& Options::ref( |
717 |
|
options::nlExtResBound__option_t); |
718 |
|
template <> const options::nlExtResBound__option_t::type& Options::operator[]( |
719 |
|
options::nlExtResBound__option_t) const; |
720 |
|
template <> bool Options::wasSetByUser(options::nlExtResBound__option_t) const; |
721 |
|
template <> options::nlExtRewrites__option_t::type& Options::ref( |
722 |
|
options::nlExtRewrites__option_t); |
723 |
|
template <> const options::nlExtRewrites__option_t::type& Options::operator[]( |
724 |
|
options::nlExtRewrites__option_t) const; |
725 |
|
template <> bool Options::wasSetByUser(options::nlExtRewrites__option_t) const; |
726 |
|
template <> options::nlExtSplitZero__option_t::type& Options::ref( |
727 |
|
options::nlExtSplitZero__option_t); |
728 |
|
template <> const options::nlExtSplitZero__option_t::type& Options::operator[]( |
729 |
|
options::nlExtSplitZero__option_t) const; |
730 |
|
template <> bool Options::wasSetByUser(options::nlExtSplitZero__option_t) const; |
731 |
|
template <> options::nlExtTfTaylorDegree__option_t::type& Options::ref( |
732 |
|
options::nlExtTfTaylorDegree__option_t); |
733 |
|
template <> const options::nlExtTfTaylorDegree__option_t::type& Options::operator[]( |
734 |
|
options::nlExtTfTaylorDegree__option_t) const; |
735 |
|
template <> bool Options::wasSetByUser(options::nlExtTfTaylorDegree__option_t) const; |
736 |
|
template <> options::nlExtTfTangentPlanes__option_t::type& Options::ref( |
737 |
|
options::nlExtTfTangentPlanes__option_t); |
738 |
|
template <> const options::nlExtTfTangentPlanes__option_t::type& Options::operator[]( |
739 |
|
options::nlExtTfTangentPlanes__option_t) const; |
740 |
|
template <> bool Options::wasSetByUser(options::nlExtTfTangentPlanes__option_t) const; |
741 |
|
template <> options::nlExtTangentPlanes__option_t::type& Options::ref( |
742 |
|
options::nlExtTangentPlanes__option_t); |
743 |
|
template <> const options::nlExtTangentPlanes__option_t::type& Options::operator[]( |
744 |
|
options::nlExtTangentPlanes__option_t) const; |
745 |
|
template <> bool Options::wasSetByUser(options::nlExtTangentPlanes__option_t) const; |
746 |
|
template <> options::nlExtTangentPlanesInterleave__option_t::type& Options::ref( |
747 |
|
options::nlExtTangentPlanesInterleave__option_t); |
748 |
|
template <> const options::nlExtTangentPlanesInterleave__option_t::type& Options::operator[]( |
749 |
|
options::nlExtTangentPlanesInterleave__option_t) const; |
750 |
|
template <> bool Options::wasSetByUser(options::nlExtTangentPlanesInterleave__option_t) const; |
751 |
|
template <> options::nlExt__option_t::type& Options::ref( |
752 |
|
options::nlExt__option_t); |
753 |
|
template <> const options::nlExt__option_t::type& Options::operator[]( |
754 |
|
options::nlExt__option_t) const; |
755 |
|
template <> bool Options::wasSetByUser(options::nlExt__option_t) const; |
756 |
|
template <> options::nlICP__option_t::type& Options::ref( |
757 |
|
options::nlICP__option_t); |
758 |
|
template <> const options::nlICP__option_t::type& Options::operator[]( |
759 |
|
options::nlICP__option_t) const; |
760 |
|
template <> bool Options::wasSetByUser(options::nlICP__option_t) const; |
761 |
|
template <> options::nlRlvMode__option_t::type& Options::ref( |
762 |
|
options::nlRlvMode__option_t); |
763 |
|
template <> const options::nlRlvMode__option_t::type& Options::operator[]( |
764 |
|
options::nlRlvMode__option_t) const; |
765 |
|
template <> bool Options::wasSetByUser(options::nlRlvMode__option_t) const; |
766 |
|
template <> options::pbRewrites__option_t::type& Options::ref( |
767 |
|
options::pbRewrites__option_t); |
768 |
|
template <> const options::pbRewrites__option_t::type& Options::operator[]( |
769 |
|
options::pbRewrites__option_t) const; |
770 |
|
template <> bool Options::wasSetByUser(options::pbRewrites__option_t) const; |
771 |
|
template <> options::arithPivotThreshold__option_t::type& Options::ref( |
772 |
|
options::arithPivotThreshold__option_t); |
773 |
|
template <> const options::arithPivotThreshold__option_t::type& Options::operator[]( |
774 |
|
options::arithPivotThreshold__option_t) const; |
775 |
|
template <> bool Options::wasSetByUser(options::arithPivotThreshold__option_t) const; |
776 |
|
template <> options::ppAssertMaxSubSize__option_t::type& Options::ref( |
777 |
|
options::ppAssertMaxSubSize__option_t); |
778 |
|
template <> const options::ppAssertMaxSubSize__option_t::type& Options::operator[]( |
779 |
|
options::ppAssertMaxSubSize__option_t) const; |
780 |
|
template <> bool Options::wasSetByUser(options::ppAssertMaxSubSize__option_t) const; |
781 |
|
template <> options::arithPropagateMaxLength__option_t::type& Options::ref( |
782 |
|
options::arithPropagateMaxLength__option_t); |
783 |
|
template <> const options::arithPropagateMaxLength__option_t::type& Options::operator[]( |
784 |
|
options::arithPropagateMaxLength__option_t) const; |
785 |
|
template <> bool Options::wasSetByUser(options::arithPropagateMaxLength__option_t) const; |
786 |
|
template <> options::replayEarlyCloseDepths__option_t::type& Options::ref( |
787 |
|
options::replayEarlyCloseDepths__option_t); |
788 |
|
template <> const options::replayEarlyCloseDepths__option_t::type& Options::operator[]( |
789 |
|
options::replayEarlyCloseDepths__option_t) const; |
790 |
|
template <> bool Options::wasSetByUser(options::replayEarlyCloseDepths__option_t) const; |
791 |
|
template <> options::replayFailurePenalty__option_t::type& Options::ref( |
792 |
|
options::replayFailurePenalty__option_t); |
793 |
|
template <> const options::replayFailurePenalty__option_t::type& Options::operator[]( |
794 |
|
options::replayFailurePenalty__option_t) const; |
795 |
|
template <> bool Options::wasSetByUser(options::replayFailurePenalty__option_t) const; |
796 |
|
template <> options::lemmaRejectCutSize__option_t::type& Options::ref( |
797 |
|
options::lemmaRejectCutSize__option_t); |
798 |
|
template <> const options::lemmaRejectCutSize__option_t::type& Options::operator[]( |
799 |
|
options::lemmaRejectCutSize__option_t) const; |
800 |
|
template <> bool Options::wasSetByUser(options::lemmaRejectCutSize__option_t) const; |
801 |
|
template <> options::replayNumericFailurePenalty__option_t::type& Options::ref( |
802 |
|
options::replayNumericFailurePenalty__option_t); |
803 |
|
template <> const options::replayNumericFailurePenalty__option_t::type& Options::operator[]( |
804 |
|
options::replayNumericFailurePenalty__option_t) const; |
805 |
|
template <> bool Options::wasSetByUser(options::replayNumericFailurePenalty__option_t) const; |
806 |
|
template <> options::replayRejectCutSize__option_t::type& Options::ref( |
807 |
|
options::replayRejectCutSize__option_t); |
808 |
|
template <> const options::replayRejectCutSize__option_t::type& Options::operator[]( |
809 |
|
options::replayRejectCutSize__option_t) const; |
810 |
|
template <> bool Options::wasSetByUser(options::replayRejectCutSize__option_t) const; |
811 |
|
template <> options::soiApproxMajorFailurePen__option_t::type& Options::ref( |
812 |
|
options::soiApproxMajorFailurePen__option_t); |
813 |
|
template <> const options::soiApproxMajorFailurePen__option_t::type& Options::operator[]( |
814 |
|
options::soiApproxMajorFailurePen__option_t) const; |
815 |
|
template <> bool Options::wasSetByUser(options::soiApproxMajorFailurePen__option_t) const; |
816 |
|
template <> options::soiApproxMajorFailure__option_t::type& Options::ref( |
817 |
|
options::soiApproxMajorFailure__option_t); |
818 |
|
template <> const options::soiApproxMajorFailure__option_t::type& Options::operator[]( |
819 |
|
options::soiApproxMajorFailure__option_t) const; |
820 |
|
template <> bool Options::wasSetByUser(options::soiApproxMajorFailure__option_t) const; |
821 |
|
template <> options::soiApproxMinorFailurePen__option_t::type& Options::ref( |
822 |
|
options::soiApproxMinorFailurePen__option_t); |
823 |
|
template <> const options::soiApproxMinorFailurePen__option_t::type& Options::operator[]( |
824 |
|
options::soiApproxMinorFailurePen__option_t) const; |
825 |
|
template <> bool Options::wasSetByUser(options::soiApproxMinorFailurePen__option_t) const; |
826 |
|
template <> options::soiApproxMinorFailure__option_t::type& Options::ref( |
827 |
|
options::soiApproxMinorFailure__option_t); |
828 |
|
template <> const options::soiApproxMinorFailure__option_t::type& Options::operator[]( |
829 |
|
options::soiApproxMinorFailure__option_t) const; |
830 |
|
template <> bool Options::wasSetByUser(options::soiApproxMinorFailure__option_t) const; |
831 |
|
template <> options::restrictedPivots__option_t::type& Options::ref( |
832 |
|
options::restrictedPivots__option_t); |
833 |
|
template <> const options::restrictedPivots__option_t::type& Options::operator[]( |
834 |
|
options::restrictedPivots__option_t) const; |
835 |
|
template <> bool Options::wasSetByUser(options::restrictedPivots__option_t) const; |
836 |
|
template <> options::revertArithModels__option_t::type& Options::ref( |
837 |
|
options::revertArithModels__option_t); |
838 |
|
template <> const options::revertArithModels__option_t::type& Options::operator[]( |
839 |
|
options::revertArithModels__option_t) const; |
840 |
|
template <> bool Options::wasSetByUser(options::revertArithModels__option_t) const; |
841 |
|
template <> options::rrTurns__option_t::type& Options::ref( |
842 |
|
options::rrTurns__option_t); |
843 |
|
template <> const options::rrTurns__option_t::type& Options::operator[]( |
844 |
|
options::rrTurns__option_t) const; |
845 |
|
template <> bool Options::wasSetByUser(options::rrTurns__option_t) const; |
846 |
|
template <> options::trySolveIntStandardEffort__option_t::type& Options::ref( |
847 |
|
options::trySolveIntStandardEffort__option_t); |
848 |
|
template <> const options::trySolveIntStandardEffort__option_t::type& Options::operator[]( |
849 |
|
options::trySolveIntStandardEffort__option_t) const; |
850 |
|
template <> bool Options::wasSetByUser(options::trySolveIntStandardEffort__option_t) const; |
851 |
|
template <> options::arithSimplexCheckPeriod__option_t::type& Options::ref( |
852 |
|
options::arithSimplexCheckPeriod__option_t); |
853 |
|
template <> const options::arithSimplexCheckPeriod__option_t::type& Options::operator[]( |
854 |
|
options::arithSimplexCheckPeriod__option_t) const; |
855 |
|
template <> bool Options::wasSetByUser(options::arithSimplexCheckPeriod__option_t) const; |
856 |
|
template <> options::soiQuickExplain__option_t::type& Options::ref( |
857 |
|
options::soiQuickExplain__option_t); |
858 |
|
template <> const options::soiQuickExplain__option_t::type& Options::operator[]( |
859 |
|
options::soiQuickExplain__option_t) const; |
860 |
|
template <> bool Options::wasSetByUser(options::soiQuickExplain__option_t) const; |
861 |
|
template <> options::arithStandardCheckVarOrderPivots__option_t::type& Options::ref( |
862 |
|
options::arithStandardCheckVarOrderPivots__option_t); |
863 |
|
template <> const options::arithStandardCheckVarOrderPivots__option_t::type& Options::operator[]( |
864 |
|
options::arithStandardCheckVarOrderPivots__option_t) const; |
865 |
|
template <> bool Options::wasSetByUser(options::arithStandardCheckVarOrderPivots__option_t) const; |
866 |
|
template <> options::arithUnateLemmaMode__option_t::type& Options::ref( |
867 |
|
options::arithUnateLemmaMode__option_t); |
868 |
|
template <> const options::arithUnateLemmaMode__option_t::type& Options::operator[]( |
869 |
|
options::arithUnateLemmaMode__option_t) const; |
870 |
|
template <> bool Options::wasSetByUser(options::arithUnateLemmaMode__option_t) const; |
871 |
|
template <> options::useApprox__option_t::type& Options::ref( |
872 |
|
options::useApprox__option_t); |
873 |
|
template <> const options::useApprox__option_t::type& Options::operator[]( |
874 |
|
options::useApprox__option_t) const; |
875 |
|
template <> bool Options::wasSetByUser(options::useApprox__option_t) const; |
876 |
|
template <> options::useFC__option_t::type& Options::ref( |
877 |
|
options::useFC__option_t); |
878 |
|
template <> const options::useFC__option_t::type& Options::operator[]( |
879 |
|
options::useFC__option_t) const; |
880 |
|
template <> bool Options::wasSetByUser(options::useFC__option_t) const; |
881 |
|
template <> options::useSOI__option_t::type& Options::ref( |
882 |
|
options::useSOI__option_t); |
883 |
|
template <> const options::useSOI__option_t::type& Options::operator[]( |
884 |
|
options::useSOI__option_t) const; |
885 |
|
template <> bool Options::wasSetByUser(options::useSOI__option_t) const; |
886 |
|
// clang-format on |
887 |
|
|
888 |
|
namespace options { |
889 |
|
// clang-format off |
890 |
|
inline maxApproxDepth__option_t::type maxApproxDepth__option_t::operator()() const |
891 |
|
{ |
892 |
|
return Options::current()[*this]; |
893 |
|
} |
894 |
1035 |
inline brabTest__option_t::type brabTest__option_t::operator()() const |
895 |
|
{ |
896 |
1035 |
return Options::current()[*this]; |
897 |
|
} |
898 |
625 |
inline arithNoPartialFun__option_t::type arithNoPartialFun__option_t::operator()() const |
899 |
|
{ |
900 |
625 |
return Options::current()[*this]; |
901 |
|
} |
902 |
113650 |
inline arithPropAsLemmaLength__option_t::type arithPropAsLemmaLength__option_t::operator()() const |
903 |
|
{ |
904 |
113650 |
return Options::current()[*this]; |
905 |
|
} |
906 |
6735426 |
inline arithPropagationMode__option_t::type arithPropagationMode__option_t::operator()() const |
907 |
|
{ |
908 |
6735426 |
return Options::current()[*this]; |
909 |
|
} |
910 |
30059 |
inline arithRewriteEq__option_t::type arithRewriteEq__option_t::operator()() const |
911 |
|
{ |
912 |
30059 |
return Options::current()[*this]; |
913 |
|
} |
914 |
1245197 |
inline collectPivots__option_t::type collectPivots__option_t::operator()() const |
915 |
|
{ |
916 |
1245197 |
return Options::current()[*this]; |
917 |
|
} |
918 |
|
inline doCutAllBounded__option_t::type doCutAllBounded__option_t::operator()() const |
919 |
|
{ |
920 |
|
return Options::current()[*this]; |
921 |
|
} |
922 |
334 |
inline exportDioDecompositions__option_t::type exportDioDecompositions__option_t::operator()() const |
923 |
|
{ |
924 |
334 |
return Options::current()[*this]; |
925 |
|
} |
926 |
|
inline dioRepeat__option_t::type dioRepeat__option_t::operator()() const |
927 |
|
{ |
928 |
|
return Options::current()[*this]; |
929 |
|
} |
930 |
4585 |
inline arithDioSolver__option_t::type arithDioSolver__option_t::operator()() const |
931 |
|
{ |
932 |
4585 |
return Options::current()[*this]; |
933 |
|
} |
934 |
377 |
inline dioSolverTurns__option_t::type dioSolverTurns__option_t::operator()() const |
935 |
|
{ |
936 |
377 |
return Options::current()[*this]; |
937 |
|
} |
938 |
35816 |
inline arithErrorSelectionRule__option_t::type arithErrorSelectionRule__option_t::operator()() const |
939 |
|
{ |
940 |
35816 |
return Options::current()[*this]; |
941 |
|
} |
942 |
|
inline havePenalties__option_t::type havePenalties__option_t::operator()() const |
943 |
|
{ |
944 |
|
return Options::current()[*this]; |
945 |
|
} |
946 |
144230 |
inline arithHeuristicPivots__option_t::type arithHeuristicPivots__option_t::operator()() const |
947 |
|
{ |
948 |
144230 |
return Options::current()[*this]; |
949 |
|
} |
950 |
|
inline replayFailureLemma__option_t::type replayFailureLemma__option_t::operator()() const |
951 |
|
{ |
952 |
|
return Options::current()[*this]; |
953 |
|
} |
954 |
2336 |
inline maxCutsInContext__option_t::type maxCutsInContext__option_t::operator()() const |
955 |
|
{ |
956 |
2336 |
return Options::current()[*this]; |
957 |
|
} |
958 |
17717 |
inline arithMLTrick__option_t::type arithMLTrick__option_t::operator()() const |
959 |
|
{ |
960 |
17717 |
return Options::current()[*this]; |
961 |
|
} |
962 |
|
inline arithMLTrickSubstitutions__option_t::type arithMLTrickSubstitutions__option_t::operator()() const |
963 |
|
{ |
964 |
|
return Options::current()[*this]; |
965 |
|
} |
966 |
791966 |
inline newProp__option_t::type newProp__option_t::operator()() const |
967 |
|
{ |
968 |
791966 |
return Options::current()[*this]; |
969 |
|
} |
970 |
1215 |
inline nlCad__option_t::type nlCad__option_t::operator()() const |
971 |
|
{ |
972 |
1215 |
return Options::current()[*this]; |
973 |
|
} |
974 |
182 |
inline nlCadUseInitial__option_t::type nlCadUseInitial__option_t::operator()() const |
975 |
|
{ |
976 |
182 |
return Options::current()[*this]; |
977 |
|
} |
978 |
8870 |
inline nlExtEntailConflicts__option_t::type nlExtEntailConflicts__option_t::operator()() const |
979 |
|
{ |
980 |
8870 |
return Options::current()[*this]; |
981 |
|
} |
982 |
394 |
inline nlExtFactor__option_t::type nlExtFactor__option_t::operator()() const |
983 |
|
{ |
984 |
394 |
return Options::current()[*this]; |
985 |
|
} |
986 |
18 |
inline nlExtIncPrecision__option_t::type nlExtIncPrecision__option_t::operator()() const |
987 |
|
{ |
988 |
18 |
return Options::current()[*this]; |
989 |
|
} |
990 |
11638 |
inline nlExtPurify__option_t::type nlExtPurify__option_t::operator()() const |
991 |
|
{ |
992 |
11638 |
return Options::current()[*this]; |
993 |
|
} |
994 |
394 |
inline nlExtResBound__option_t::type nlExtResBound__option_t::operator()() const |
995 |
|
{ |
996 |
394 |
return Options::current()[*this]; |
997 |
|
} |
998 |
26139 |
inline nlExtRewrites__option_t::type nlExtRewrites__option_t::operator()() const |
999 |
|
{ |
1000 |
26139 |
return Options::current()[*this]; |
1001 |
|
} |
1002 |
394 |
inline nlExtSplitZero__option_t::type nlExtSplitZero__option_t::operator()() const |
1003 |
|
{ |
1004 |
394 |
return Options::current()[*this]; |
1005 |
|
} |
1006 |
4781 |
inline nlExtTfTaylorDegree__option_t::type nlExtTfTaylorDegree__option_t::operator()() const |
1007 |
|
{ |
1008 |
4781 |
return Options::current()[*this]; |
1009 |
|
} |
1010 |
394 |
inline nlExtTfTangentPlanes__option_t::type nlExtTfTangentPlanes__option_t::operator()() const |
1011 |
|
{ |
1012 |
394 |
return Options::current()[*this]; |
1013 |
|
} |
1014 |
61967 |
inline nlExtTangentPlanes__option_t::type nlExtTangentPlanes__option_t::operator()() const |
1015 |
|
{ |
1016 |
61967 |
return Options::current()[*this]; |
1017 |
|
} |
1018 |
144 |
inline nlExtTangentPlanesInterleave__option_t::type nlExtTangentPlanesInterleave__option_t::operator()() const |
1019 |
|
{ |
1020 |
144 |
return Options::current()[*this]; |
1021 |
|
} |
1022 |
2038 |
inline nlExt__option_t::type nlExt__option_t::operator()() const |
1023 |
|
{ |
1024 |
2038 |
return Options::current()[*this]; |
1025 |
|
} |
1026 |
427 |
inline nlICP__option_t::type nlICP__option_t::operator()() const |
1027 |
|
{ |
1028 |
427 |
return Options::current()[*this]; |
1029 |
|
} |
1030 |
10155 |
inline nlRlvMode__option_t::type nlRlvMode__option_t::operator()() const |
1031 |
|
{ |
1032 |
10155 |
return Options::current()[*this]; |
1033 |
|
} |
1034 |
13546 |
inline pbRewrites__option_t::type pbRewrites__option_t::operator()() const |
1035 |
|
{ |
1036 |
13546 |
return Options::current()[*this]; |
1037 |
|
} |
1038 |
369296 |
inline arithPivotThreshold__option_t::type arithPivotThreshold__option_t::operator()() const |
1039 |
|
{ |
1040 |
369296 |
return Options::current()[*this]; |
1041 |
|
} |
1042 |
1378 |
inline ppAssertMaxSubSize__option_t::type ppAssertMaxSubSize__option_t::operator()() const |
1043 |
|
{ |
1044 |
1378 |
return Options::current()[*this]; |
1045 |
|
} |
1046 |
9031766 |
inline arithPropagateMaxLength__option_t::type arithPropagateMaxLength__option_t::operator()() const |
1047 |
|
{ |
1048 |
9031766 |
return Options::current()[*this]; |
1049 |
|
} |
1050 |
|
inline replayEarlyCloseDepths__option_t::type replayEarlyCloseDepths__option_t::operator()() const |
1051 |
|
{ |
1052 |
|
return Options::current()[*this]; |
1053 |
|
} |
1054 |
|
inline replayFailurePenalty__option_t::type replayFailurePenalty__option_t::operator()() const |
1055 |
|
{ |
1056 |
|
return Options::current()[*this]; |
1057 |
|
} |
1058 |
|
inline lemmaRejectCutSize__option_t::type lemmaRejectCutSize__option_t::operator()() const |
1059 |
|
{ |
1060 |
|
return Options::current()[*this]; |
1061 |
|
} |
1062 |
|
inline replayNumericFailurePenalty__option_t::type replayNumericFailurePenalty__option_t::operator()() const |
1063 |
|
{ |
1064 |
|
return Options::current()[*this]; |
1065 |
|
} |
1066 |
|
inline replayRejectCutSize__option_t::type replayRejectCutSize__option_t::operator()() const |
1067 |
|
{ |
1068 |
|
return Options::current()[*this]; |
1069 |
|
} |
1070 |
|
inline soiApproxMajorFailurePen__option_t::type soiApproxMajorFailurePen__option_t::operator()() const |
1071 |
|
{ |
1072 |
|
return Options::current()[*this]; |
1073 |
|
} |
1074 |
|
inline soiApproxMajorFailure__option_t::type soiApproxMajorFailure__option_t::operator()() const |
1075 |
|
{ |
1076 |
|
return Options::current()[*this]; |
1077 |
|
} |
1078 |
|
inline soiApproxMinorFailurePen__option_t::type soiApproxMinorFailurePen__option_t::operator()() const |
1079 |
|
{ |
1080 |
|
return Options::current()[*this]; |
1081 |
|
} |
1082 |
|
inline soiApproxMinorFailure__option_t::type soiApproxMinorFailure__option_t::operator()() const |
1083 |
|
{ |
1084 |
|
return Options::current()[*this]; |
1085 |
|
} |
1086 |
1238839 |
inline restrictedPivots__option_t::type restrictedPivots__option_t::operator()() const |
1087 |
|
{ |
1088 |
1238839 |
return Options::current()[*this]; |
1089 |
|
} |
1090 |
12741 |
inline revertArithModels__option_t::type revertArithModels__option_t::operator()() const |
1091 |
|
{ |
1092 |
12741 |
return Options::current()[*this]; |
1093 |
|
} |
1094 |
112 |
inline rrTurns__option_t::type rrTurns__option_t::operator()() const |
1095 |
|
{ |
1096 |
112 |
return Options::current()[*this]; |
1097 |
|
} |
1098 |
|
inline trySolveIntStandardEffort__option_t::type trySolveIntStandardEffort__option_t::operator()() const |
1099 |
|
{ |
1100 |
|
return Options::current()[*this]; |
1101 |
|
} |
1102 |
79538 |
inline arithSimplexCheckPeriod__option_t::type arithSimplexCheckPeriod__option_t::operator()() const |
1103 |
|
{ |
1104 |
79538 |
return Options::current()[*this]; |
1105 |
|
} |
1106 |
|
inline soiQuickExplain__option_t::type soiQuickExplain__option_t::operator()() const |
1107 |
|
{ |
1108 |
|
return Options::current()[*this]; |
1109 |
|
} |
1110 |
103522 |
inline arithStandardCheckVarOrderPivots__option_t::type arithStandardCheckVarOrderPivots__option_t::operator()() const |
1111 |
|
{ |
1112 |
103522 |
return Options::current()[*this]; |
1113 |
|
} |
1114 |
7294 |
inline arithUnateLemmaMode__option_t::type arithUnateLemmaMode__option_t::operator()() const |
1115 |
|
{ |
1116 |
7294 |
return Options::current()[*this]; |
1117 |
|
} |
1118 |
3747720 |
inline useApprox__option_t::type useApprox__option_t::operator()() const |
1119 |
|
{ |
1120 |
3747720 |
return Options::current()[*this]; |
1121 |
|
} |
1122 |
1297389 |
inline useFC__option_t::type useFC__option_t::operator()() const |
1123 |
|
{ |
1124 |
1297389 |
return Options::current()[*this]; |
1125 |
|
} |
1126 |
5820 |
inline useSOI__option_t::type useSOI__option_t::operator()() const |
1127 |
|
{ |
1128 |
5820 |
return Options::current()[*this]; |
1129 |
|
} |
1130 |
|
// clang-format on |
1131 |
|
|
1132 |
|
} // namespace options |
1133 |
|
} // namespace cvc5 |
1134 |
|
|
1135 |
|
#endif /* CVC5__OPTIONS__ARITH_H */ |