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 |
|
BOTH_PROP, |
39 |
|
NO_PROP, |
40 |
|
BOUND_INFERENCE_PROP |
41 |
|
}; |
42 |
|
|
43 |
|
static constexpr size_t ArithPropagationMode__numValues = 4; |
44 |
|
|
45 |
|
std::ostream& operator<<(std::ostream& os, ArithPropagationMode mode); |
46 |
|
ArithPropagationMode stringToArithPropagationMode(const std::string& optarg); |
47 |
|
enum class ErrorSelectionRule |
48 |
|
{ |
49 |
|
MAXIMUM_AMOUNT, |
50 |
|
SUM_METRIC, |
51 |
|
VAR_ORDER, |
52 |
|
MINIMUM_AMOUNT |
53 |
|
}; |
54 |
|
|
55 |
|
static constexpr size_t ErrorSelectionRule__numValues = 4; |
56 |
|
|
57 |
|
std::ostream& operator<<(std::ostream& os, ErrorSelectionRule mode); |
58 |
|
ErrorSelectionRule stringToErrorSelectionRule(const std::string& optarg); |
59 |
|
enum class NlCadLiftingMode |
60 |
|
{ |
61 |
|
REGULAR, |
62 |
|
LAZARD |
63 |
|
}; |
64 |
|
|
65 |
|
static constexpr size_t NlCadLiftingMode__numValues = 2; |
66 |
|
|
67 |
|
std::ostream& operator<<(std::ostream& os, NlCadLiftingMode mode); |
68 |
|
NlCadLiftingMode stringToNlCadLiftingMode(const std::string& optarg); |
69 |
|
enum class NlCadProjectionMode |
70 |
|
{ |
71 |
|
MCCALLUM, |
72 |
|
LAZARDMOD, |
73 |
|
LAZARD |
74 |
|
}; |
75 |
|
|
76 |
|
static constexpr size_t NlCadProjectionMode__numValues = 3; |
77 |
|
|
78 |
|
std::ostream& operator<<(std::ostream& os, NlCadProjectionMode mode); |
79 |
|
NlCadProjectionMode stringToNlCadProjectionMode(const std::string& optarg); |
80 |
|
enum class NlExtMode |
81 |
|
{ |
82 |
|
LIGHT, |
83 |
|
NONE, |
84 |
|
FULL |
85 |
|
}; |
86 |
|
|
87 |
|
static constexpr size_t NlExtMode__numValues = 3; |
88 |
|
|
89 |
|
std::ostream& operator<<(std::ostream& os, NlExtMode mode); |
90 |
|
NlExtMode stringToNlExtMode(const std::string& optarg); |
91 |
|
enum class NlRlvMode |
92 |
|
{ |
93 |
|
ALWAYS, |
94 |
|
NONE, |
95 |
|
INTERLEAVE |
96 |
|
}; |
97 |
|
|
98 |
|
static constexpr size_t NlRlvMode__numValues = 3; |
99 |
|
|
100 |
|
std::ostream& operator<<(std::ostream& os, NlRlvMode mode); |
101 |
|
NlRlvMode stringToNlRlvMode(const std::string& optarg); |
102 |
|
enum class ArithUnateLemmaMode |
103 |
|
{ |
104 |
|
NO, |
105 |
|
EQUALITY, |
106 |
|
ALL, |
107 |
|
INEQUALITY |
108 |
|
}; |
109 |
|
|
110 |
|
static constexpr size_t ArithUnateLemmaMode__numValues = 4; |
111 |
|
|
112 |
|
std::ostream& operator<<(std::ostream& os, ArithUnateLemmaMode mode); |
113 |
|
ArithUnateLemmaMode stringToArithUnateLemmaMode(const std::string& optarg); |
114 |
|
// clang-format on |
115 |
|
|
116 |
|
#if defined(CVC5_MUZZLED) || defined(CVC5_COMPETITION_MODE) |
117 |
|
# define DO_SEMANTIC_CHECKS_BY_DEFAULT false |
118 |
|
#else /* CVC5_MUZZLED || CVC5_COMPETITION_MODE */ |
119 |
|
# define DO_SEMANTIC_CHECKS_BY_DEFAULT true |
120 |
|
#endif /* CVC5_MUZZLED || CVC5_COMPETITION_MODE */ |
121 |
|
|
122 |
27397 |
struct HolderARITH |
123 |
|
{ |
124 |
|
// clang-format off |
125 |
|
int16_t maxApproxDepth = 200; |
126 |
|
bool maxApproxDepthWasSetByUser = false; |
127 |
|
bool brabTest = true; |
128 |
|
bool brabTestWasSetByUser = false; |
129 |
|
bool arithCongMan = true; |
130 |
|
bool arithCongManWasSetByUser = false; |
131 |
|
bool arithEqSolver = false; |
132 |
|
bool arithEqSolverWasSetByUser = false; |
133 |
|
bool arithNoPartialFun = false; |
134 |
|
bool arithNoPartialFunWasSetByUser = false; |
135 |
|
uint16_t arithPropAsLemmaLength = 8; |
136 |
|
bool arithPropAsLemmaLengthWasSetByUser = false; |
137 |
|
ArithPropagationMode arithPropagationMode = ArithPropagationMode::BOTH_PROP; |
138 |
|
bool arithPropagationModeWasSetByUser = false; |
139 |
|
bool arithRewriteEq = false; |
140 |
|
bool arithRewriteEqWasSetByUser = false; |
141 |
|
bool collectPivots = false; |
142 |
|
bool collectPivotsWasSetByUser = false; |
143 |
|
bool doCutAllBounded = false; |
144 |
|
bool doCutAllBoundedWasSetByUser = false; |
145 |
|
bool exportDioDecompositions = false; |
146 |
|
bool exportDioDecompositionsWasSetByUser = false; |
147 |
|
bool dioRepeat = false; |
148 |
|
bool dioRepeatWasSetByUser = false; |
149 |
|
bool arithDioSolver = true; |
150 |
|
bool arithDioSolverWasSetByUser = false; |
151 |
|
int dioSolverTurns = 10; |
152 |
|
bool dioSolverTurnsWasSetByUser = false; |
153 |
|
ErrorSelectionRule arithErrorSelectionRule = ErrorSelectionRule::MINIMUM_AMOUNT; |
154 |
|
bool arithErrorSelectionRuleWasSetByUser = false; |
155 |
|
bool havePenalties = false; |
156 |
|
bool havePenaltiesWasSetByUser = false; |
157 |
|
int16_t arithHeuristicPivots = 0; |
158 |
|
bool arithHeuristicPivotsWasSetByUser = false; |
159 |
|
bool replayFailureLemma = false; |
160 |
|
bool replayFailureLemmaWasSetByUser = false; |
161 |
|
unsigned maxCutsInContext = 65535; |
162 |
|
bool maxCutsInContextWasSetByUser = false; |
163 |
|
bool arithMLTrick = false; |
164 |
|
bool arithMLTrickWasSetByUser = false; |
165 |
|
unsigned arithMLTrickSubstitutions = 1; |
166 |
|
bool arithMLTrickSubstitutionsWasSetByUser = false; |
167 |
|
bool newProp = true; |
168 |
|
bool newPropWasSetByUser = false; |
169 |
|
bool nlCad = false; |
170 |
|
bool nlCadWasSetByUser = false; |
171 |
|
bool nlCadUseInitial = false; |
172 |
|
bool nlCadUseInitialWasSetByUser = false; |
173 |
|
NlCadLiftingMode nlCadLifting = NlCadLiftingMode::REGULAR; |
174 |
|
bool nlCadLiftingWasSetByUser = false; |
175 |
|
NlCadProjectionMode nlCadProjection = NlCadProjectionMode::MCCALLUM; |
176 |
|
bool nlCadProjectionWasSetByUser = false; |
177 |
|
bool nlExtEntailConflicts = false; |
178 |
|
bool nlExtEntailConflictsWasSetByUser = false; |
179 |
|
bool nlExtFactor = true; |
180 |
|
bool nlExtFactorWasSetByUser = false; |
181 |
|
bool nlExtIncPrecision = true; |
182 |
|
bool nlExtIncPrecisionWasSetByUser = false; |
183 |
|
bool nlExtPurify = false; |
184 |
|
bool nlExtPurifyWasSetByUser = false; |
185 |
|
bool nlExtResBound = false; |
186 |
|
bool nlExtResBoundWasSetByUser = false; |
187 |
|
bool nlExtRewrites = true; |
188 |
|
bool nlExtRewritesWasSetByUser = false; |
189 |
|
bool nlExtSplitZero = false; |
190 |
|
bool nlExtSplitZeroWasSetByUser = false; |
191 |
|
int16_t nlExtTfTaylorDegree = 4; |
192 |
|
bool nlExtTfTaylorDegreeWasSetByUser = false; |
193 |
|
bool nlExtTfTangentPlanes = true; |
194 |
|
bool nlExtTfTangentPlanesWasSetByUser = false; |
195 |
|
bool nlExtTangentPlanes = false; |
196 |
|
bool nlExtTangentPlanesWasSetByUser = false; |
197 |
|
bool nlExtTangentPlanesInterleave = false; |
198 |
|
bool nlExtTangentPlanesInterleaveWasSetByUser = false; |
199 |
|
NlExtMode nlExt = NlExtMode::FULL; |
200 |
|
bool nlExtWasSetByUser = false; |
201 |
|
bool nlICP = false; |
202 |
|
bool nlICPWasSetByUser = false; |
203 |
|
NlRlvMode nlRlvMode = NlRlvMode::NONE; |
204 |
|
bool nlRlvModeWasSetByUser = false; |
205 |
|
bool pbRewrites = false; |
206 |
|
bool pbRewritesWasSetByUser = false; |
207 |
|
uint16_t arithPivotThreshold = 2; |
208 |
|
bool arithPivotThresholdWasSetByUser = false; |
209 |
|
unsigned ppAssertMaxSubSize = 2; |
210 |
|
bool ppAssertMaxSubSizeWasSetByUser = false; |
211 |
|
uint16_t arithPropagateMaxLength = 16; |
212 |
|
bool arithPropagateMaxLengthWasSetByUser = false; |
213 |
|
int replayEarlyCloseDepths = 1; |
214 |
|
bool replayEarlyCloseDepthsWasSetByUser = false; |
215 |
|
int replayFailurePenalty = 100; |
216 |
|
bool replayFailurePenaltyWasSetByUser = false; |
217 |
|
unsigned lemmaRejectCutSize = 25500; |
218 |
|
bool lemmaRejectCutSizeWasSetByUser = false; |
219 |
|
int replayNumericFailurePenalty = 4194304; |
220 |
|
bool replayNumericFailurePenaltyWasSetByUser = false; |
221 |
|
unsigned replayRejectCutSize = 25500; |
222 |
|
bool replayRejectCutSizeWasSetByUser = false; |
223 |
|
int soiApproxMajorFailurePen = 50; |
224 |
|
bool soiApproxMajorFailurePenWasSetByUser = false; |
225 |
|
double soiApproxMajorFailure = .01; |
226 |
|
bool soiApproxMajorFailureWasSetByUser = false; |
227 |
|
int soiApproxMinorFailurePen = 10; |
228 |
|
bool soiApproxMinorFailurePenWasSetByUser = false; |
229 |
|
double soiApproxMinorFailure = .0001; |
230 |
|
bool soiApproxMinorFailureWasSetByUser = false; |
231 |
|
bool restrictedPivots = true; |
232 |
|
bool restrictedPivotsWasSetByUser = false; |
233 |
|
bool revertArithModels = false; |
234 |
|
bool revertArithModelsWasSetByUser = false; |
235 |
|
int rrTurns = 3; |
236 |
|
bool rrTurnsWasSetByUser = false; |
237 |
|
bool trySolveIntStandardEffort = false; |
238 |
|
bool trySolveIntStandardEffortWasSetByUser = false; |
239 |
|
uint16_t arithSimplexCheckPeriod = 200; |
240 |
|
bool arithSimplexCheckPeriodWasSetByUser = false; |
241 |
|
bool soiQuickExplain = false; |
242 |
|
bool soiQuickExplainWasSetByUser = false; |
243 |
|
int16_t arithStandardCheckVarOrderPivots = -1; |
244 |
|
bool arithStandardCheckVarOrderPivotsWasSetByUser = false; |
245 |
|
ArithUnateLemmaMode arithUnateLemmaMode = ArithUnateLemmaMode::ALL; |
246 |
|
bool arithUnateLemmaModeWasSetByUser = false; |
247 |
|
bool useApprox = false; |
248 |
|
bool useApproxWasSetByUser = false; |
249 |
|
bool useFC = false; |
250 |
|
bool useFCWasSetByUser = false; |
251 |
|
bool useSOI = false; |
252 |
|
bool useSOIWasSetByUser = false; |
253 |
|
// clang-format on |
254 |
|
}; |
255 |
|
|
256 |
|
#undef DO_SEMANTIC_CHECKS_BY_DEFAULT |
257 |
|
|
258 |
|
// clang-format off |
259 |
|
extern struct maxApproxDepth__option_t |
260 |
|
{ |
261 |
|
typedef int16_t type; |
262 |
|
type operator()() const; |
263 |
|
} thread_local maxApproxDepth; |
264 |
|
extern struct brabTest__option_t |
265 |
|
{ |
266 |
|
typedef bool type; |
267 |
|
type operator()() const; |
268 |
|
} thread_local brabTest; |
269 |
|
extern struct arithCongMan__option_t |
270 |
|
{ |
271 |
|
typedef bool type; |
272 |
|
type operator()() const; |
273 |
|
} thread_local arithCongMan; |
274 |
|
extern struct arithEqSolver__option_t |
275 |
|
{ |
276 |
|
typedef bool type; |
277 |
|
type operator()() const; |
278 |
|
} thread_local arithEqSolver; |
279 |
|
extern struct arithNoPartialFun__option_t |
280 |
|
{ |
281 |
|
typedef bool type; |
282 |
|
type operator()() const; |
283 |
|
} thread_local arithNoPartialFun; |
284 |
|
extern struct arithPropAsLemmaLength__option_t |
285 |
|
{ |
286 |
|
typedef uint16_t type; |
287 |
|
type operator()() const; |
288 |
|
} thread_local arithPropAsLemmaLength; |
289 |
|
extern struct arithPropagationMode__option_t |
290 |
|
{ |
291 |
|
typedef ArithPropagationMode type; |
292 |
|
type operator()() const; |
293 |
|
} thread_local arithPropagationMode; |
294 |
|
extern struct arithRewriteEq__option_t |
295 |
|
{ |
296 |
|
typedef bool type; |
297 |
|
type operator()() const; |
298 |
|
} thread_local arithRewriteEq; |
299 |
|
extern struct collectPivots__option_t |
300 |
|
{ |
301 |
|
typedef bool type; |
302 |
|
type operator()() const; |
303 |
|
} thread_local collectPivots; |
304 |
|
extern struct doCutAllBounded__option_t |
305 |
|
{ |
306 |
|
typedef bool type; |
307 |
|
type operator()() const; |
308 |
|
} thread_local doCutAllBounded; |
309 |
|
extern struct exportDioDecompositions__option_t |
310 |
|
{ |
311 |
|
typedef bool type; |
312 |
|
type operator()() const; |
313 |
|
} thread_local exportDioDecompositions; |
314 |
|
extern struct dioRepeat__option_t |
315 |
|
{ |
316 |
|
typedef bool type; |
317 |
|
type operator()() const; |
318 |
|
} thread_local dioRepeat; |
319 |
|
extern struct arithDioSolver__option_t |
320 |
|
{ |
321 |
|
typedef bool type; |
322 |
|
type operator()() const; |
323 |
|
} thread_local arithDioSolver; |
324 |
|
extern struct dioSolverTurns__option_t |
325 |
|
{ |
326 |
|
typedef int type; |
327 |
|
type operator()() const; |
328 |
|
} thread_local dioSolverTurns; |
329 |
|
extern struct arithErrorSelectionRule__option_t |
330 |
|
{ |
331 |
|
typedef ErrorSelectionRule type; |
332 |
|
type operator()() const; |
333 |
|
} thread_local arithErrorSelectionRule; |
334 |
|
extern struct havePenalties__option_t |
335 |
|
{ |
336 |
|
typedef bool type; |
337 |
|
type operator()() const; |
338 |
|
} thread_local havePenalties; |
339 |
|
extern struct arithHeuristicPivots__option_t |
340 |
|
{ |
341 |
|
typedef int16_t type; |
342 |
|
type operator()() const; |
343 |
|
} thread_local arithHeuristicPivots; |
344 |
|
extern struct replayFailureLemma__option_t |
345 |
|
{ |
346 |
|
typedef bool type; |
347 |
|
type operator()() const; |
348 |
|
} thread_local replayFailureLemma; |
349 |
|
extern struct maxCutsInContext__option_t |
350 |
|
{ |
351 |
|
typedef unsigned type; |
352 |
|
type operator()() const; |
353 |
|
} thread_local maxCutsInContext; |
354 |
|
extern struct arithMLTrick__option_t |
355 |
|
{ |
356 |
|
typedef bool type; |
357 |
|
type operator()() const; |
358 |
|
} thread_local arithMLTrick; |
359 |
|
extern struct arithMLTrickSubstitutions__option_t |
360 |
|
{ |
361 |
|
typedef unsigned type; |
362 |
|
type operator()() const; |
363 |
|
} thread_local arithMLTrickSubstitutions; |
364 |
|
extern struct newProp__option_t |
365 |
|
{ |
366 |
|
typedef bool type; |
367 |
|
type operator()() const; |
368 |
|
} thread_local newProp; |
369 |
|
extern struct nlCad__option_t |
370 |
|
{ |
371 |
|
typedef bool type; |
372 |
|
type operator()() const; |
373 |
|
} thread_local nlCad; |
374 |
|
extern struct nlCadUseInitial__option_t |
375 |
|
{ |
376 |
|
typedef bool type; |
377 |
|
type operator()() const; |
378 |
|
} thread_local nlCadUseInitial; |
379 |
|
extern struct nlCadLifting__option_t |
380 |
|
{ |
381 |
|
typedef NlCadLiftingMode type; |
382 |
|
type operator()() const; |
383 |
|
} thread_local nlCadLifting; |
384 |
|
extern struct nlCadProjection__option_t |
385 |
|
{ |
386 |
|
typedef NlCadProjectionMode type; |
387 |
|
type operator()() const; |
388 |
|
} thread_local nlCadProjection; |
389 |
|
extern struct nlExtEntailConflicts__option_t |
390 |
|
{ |
391 |
|
typedef bool type; |
392 |
|
type operator()() const; |
393 |
|
} thread_local nlExtEntailConflicts; |
394 |
|
extern struct nlExtFactor__option_t |
395 |
|
{ |
396 |
|
typedef bool type; |
397 |
|
type operator()() const; |
398 |
|
} thread_local nlExtFactor; |
399 |
|
extern struct nlExtIncPrecision__option_t |
400 |
|
{ |
401 |
|
typedef bool type; |
402 |
|
type operator()() const; |
403 |
|
} thread_local nlExtIncPrecision; |
404 |
|
extern struct nlExtPurify__option_t |
405 |
|
{ |
406 |
|
typedef bool type; |
407 |
|
type operator()() const; |
408 |
|
} thread_local nlExtPurify; |
409 |
|
extern struct nlExtResBound__option_t |
410 |
|
{ |
411 |
|
typedef bool type; |
412 |
|
type operator()() const; |
413 |
|
} thread_local nlExtResBound; |
414 |
|
extern struct nlExtRewrites__option_t |
415 |
|
{ |
416 |
|
typedef bool type; |
417 |
|
type operator()() const; |
418 |
|
} thread_local nlExtRewrites; |
419 |
|
extern struct nlExtSplitZero__option_t |
420 |
|
{ |
421 |
|
typedef bool type; |
422 |
|
type operator()() const; |
423 |
|
} thread_local nlExtSplitZero; |
424 |
|
extern struct nlExtTfTaylorDegree__option_t |
425 |
|
{ |
426 |
|
typedef int16_t type; |
427 |
|
type operator()() const; |
428 |
|
} thread_local nlExtTfTaylorDegree; |
429 |
|
extern struct nlExtTfTangentPlanes__option_t |
430 |
|
{ |
431 |
|
typedef bool type; |
432 |
|
type operator()() const; |
433 |
|
} thread_local nlExtTfTangentPlanes; |
434 |
|
extern struct nlExtTangentPlanes__option_t |
435 |
|
{ |
436 |
|
typedef bool type; |
437 |
|
type operator()() const; |
438 |
|
} thread_local nlExtTangentPlanes; |
439 |
|
extern struct nlExtTangentPlanesInterleave__option_t |
440 |
|
{ |
441 |
|
typedef bool type; |
442 |
|
type operator()() const; |
443 |
|
} thread_local nlExtTangentPlanesInterleave; |
444 |
|
extern struct nlExt__option_t |
445 |
|
{ |
446 |
|
typedef NlExtMode type; |
447 |
|
type operator()() const; |
448 |
|
} thread_local nlExt; |
449 |
|
extern struct nlICP__option_t |
450 |
|
{ |
451 |
|
typedef bool type; |
452 |
|
type operator()() const; |
453 |
|
} thread_local nlICP; |
454 |
|
extern struct nlRlvMode__option_t |
455 |
|
{ |
456 |
|
typedef NlRlvMode type; |
457 |
|
type operator()() const; |
458 |
|
} thread_local nlRlvMode; |
459 |
|
extern struct pbRewrites__option_t |
460 |
|
{ |
461 |
|
typedef bool type; |
462 |
|
type operator()() const; |
463 |
|
} thread_local pbRewrites; |
464 |
|
extern struct arithPivotThreshold__option_t |
465 |
|
{ |
466 |
|
typedef uint16_t type; |
467 |
|
type operator()() const; |
468 |
|
} thread_local arithPivotThreshold; |
469 |
|
extern struct ppAssertMaxSubSize__option_t |
470 |
|
{ |
471 |
|
typedef unsigned type; |
472 |
|
type operator()() const; |
473 |
|
} thread_local ppAssertMaxSubSize; |
474 |
|
extern struct arithPropagateMaxLength__option_t |
475 |
|
{ |
476 |
|
typedef uint16_t type; |
477 |
|
type operator()() const; |
478 |
|
} thread_local arithPropagateMaxLength; |
479 |
|
extern struct replayEarlyCloseDepths__option_t |
480 |
|
{ |
481 |
|
typedef int type; |
482 |
|
type operator()() const; |
483 |
|
} thread_local replayEarlyCloseDepths; |
484 |
|
extern struct replayFailurePenalty__option_t |
485 |
|
{ |
486 |
|
typedef int type; |
487 |
|
type operator()() const; |
488 |
|
} thread_local replayFailurePenalty; |
489 |
|
extern struct lemmaRejectCutSize__option_t |
490 |
|
{ |
491 |
|
typedef unsigned type; |
492 |
|
type operator()() const; |
493 |
|
} thread_local lemmaRejectCutSize; |
494 |
|
extern struct replayNumericFailurePenalty__option_t |
495 |
|
{ |
496 |
|
typedef int type; |
497 |
|
type operator()() const; |
498 |
|
} thread_local replayNumericFailurePenalty; |
499 |
|
extern struct replayRejectCutSize__option_t |
500 |
|
{ |
501 |
|
typedef unsigned type; |
502 |
|
type operator()() const; |
503 |
|
} thread_local replayRejectCutSize; |
504 |
|
extern struct soiApproxMajorFailurePen__option_t |
505 |
|
{ |
506 |
|
typedef int type; |
507 |
|
type operator()() const; |
508 |
|
} thread_local soiApproxMajorFailurePen; |
509 |
|
extern struct soiApproxMajorFailure__option_t |
510 |
|
{ |
511 |
|
typedef double type; |
512 |
|
type operator()() const; |
513 |
|
} thread_local soiApproxMajorFailure; |
514 |
|
extern struct soiApproxMinorFailurePen__option_t |
515 |
|
{ |
516 |
|
typedef int type; |
517 |
|
type operator()() const; |
518 |
|
} thread_local soiApproxMinorFailurePen; |
519 |
|
extern struct soiApproxMinorFailure__option_t |
520 |
|
{ |
521 |
|
typedef double type; |
522 |
|
type operator()() const; |
523 |
|
} thread_local soiApproxMinorFailure; |
524 |
|
extern struct restrictedPivots__option_t |
525 |
|
{ |
526 |
|
typedef bool type; |
527 |
|
type operator()() const; |
528 |
|
} thread_local restrictedPivots; |
529 |
|
extern struct revertArithModels__option_t |
530 |
|
{ |
531 |
|
typedef bool type; |
532 |
|
type operator()() const; |
533 |
|
} thread_local revertArithModels; |
534 |
|
extern struct rrTurns__option_t |
535 |
|
{ |
536 |
|
typedef int type; |
537 |
|
type operator()() const; |
538 |
|
} thread_local rrTurns; |
539 |
|
extern struct trySolveIntStandardEffort__option_t |
540 |
|
{ |
541 |
|
typedef bool type; |
542 |
|
type operator()() const; |
543 |
|
} thread_local trySolveIntStandardEffort; |
544 |
|
extern struct arithSimplexCheckPeriod__option_t |
545 |
|
{ |
546 |
|
typedef uint16_t type; |
547 |
|
type operator()() const; |
548 |
|
} thread_local arithSimplexCheckPeriod; |
549 |
|
extern struct soiQuickExplain__option_t |
550 |
|
{ |
551 |
|
typedef bool type; |
552 |
|
type operator()() const; |
553 |
|
} thread_local soiQuickExplain; |
554 |
|
extern struct arithStandardCheckVarOrderPivots__option_t |
555 |
|
{ |
556 |
|
typedef int16_t type; |
557 |
|
type operator()() const; |
558 |
|
} thread_local arithStandardCheckVarOrderPivots; |
559 |
|
extern struct arithUnateLemmaMode__option_t |
560 |
|
{ |
561 |
|
typedef ArithUnateLemmaMode type; |
562 |
|
type operator()() const; |
563 |
|
} thread_local arithUnateLemmaMode; |
564 |
|
extern struct useApprox__option_t |
565 |
|
{ |
566 |
|
typedef bool type; |
567 |
|
type operator()() const; |
568 |
|
} thread_local useApprox; |
569 |
|
extern struct useFC__option_t |
570 |
|
{ |
571 |
|
typedef bool type; |
572 |
|
type operator()() const; |
573 |
|
} thread_local useFC; |
574 |
|
extern struct useSOI__option_t |
575 |
|
{ |
576 |
|
typedef bool type; |
577 |
|
type operator()() const; |
578 |
|
} thread_local useSOI; |
579 |
|
// clang-format on |
580 |
|
|
581 |
|
namespace arith |
582 |
|
{ |
583 |
|
// clang-format off |
584 |
|
static constexpr const char* maxApproxDepth__name = "approx-branch-depth"; |
585 |
|
static constexpr const char* brabTest__name = "arith-brab"; |
586 |
|
static constexpr const char* arithCongMan__name = "arith-cong-man"; |
587 |
|
static constexpr const char* arithEqSolver__name = "arith-eq-solver"; |
588 |
|
static constexpr const char* arithNoPartialFun__name = "arith-no-partial-fun"; |
589 |
|
static constexpr const char* arithPropAsLemmaLength__name = "arith-prop-clauses"; |
590 |
|
static constexpr const char* arithPropagationMode__name = "arith-prop"; |
591 |
|
static constexpr const char* arithRewriteEq__name = "arith-rewrite-equalities"; |
592 |
|
static constexpr const char* collectPivots__name = "collect-pivot-stats"; |
593 |
|
static constexpr const char* doCutAllBounded__name = "cut-all-bounded"; |
594 |
|
static constexpr const char* exportDioDecompositions__name = "dio-decomps"; |
595 |
|
static constexpr const char* dioRepeat__name = "dio-repeat"; |
596 |
|
static constexpr const char* arithDioSolver__name = "dio-solver"; |
597 |
|
static constexpr const char* dioSolverTurns__name = "dio-turns"; |
598 |
|
static constexpr const char* arithErrorSelectionRule__name = "error-selection-rule"; |
599 |
|
static constexpr const char* havePenalties__name = "fc-penalties"; |
600 |
|
static constexpr const char* arithHeuristicPivots__name = "heuristic-pivots"; |
601 |
|
static constexpr const char* replayFailureLemma__name = "lemmas-on-replay-failure"; |
602 |
|
static constexpr const char* maxCutsInContext__name = "maxCutsInContext"; |
603 |
|
static constexpr const char* arithMLTrick__name = "miplib-trick"; |
604 |
|
static constexpr const char* arithMLTrickSubstitutions__name = "miplib-trick-subs"; |
605 |
|
static constexpr const char* newProp__name = "new-prop"; |
606 |
|
static constexpr const char* nlCad__name = "nl-cad"; |
607 |
|
static constexpr const char* nlCadUseInitial__name = "nl-cad-initial"; |
608 |
|
static constexpr const char* nlCadLifting__name = "nl-cad-lift"; |
609 |
|
static constexpr const char* nlCadProjection__name = "nl-cad-proj"; |
610 |
|
static constexpr const char* nlExtEntailConflicts__name = "nl-ext-ent-conf"; |
611 |
|
static constexpr const char* nlExtFactor__name = "nl-ext-factor"; |
612 |
|
static constexpr const char* nlExtIncPrecision__name = "nl-ext-inc-prec"; |
613 |
|
static constexpr const char* nlExtPurify__name = "nl-ext-purify"; |
614 |
|
static constexpr const char* nlExtResBound__name = "nl-ext-rbound"; |
615 |
|
static constexpr const char* nlExtRewrites__name = "nl-ext-rewrite"; |
616 |
|
static constexpr const char* nlExtSplitZero__name = "nl-ext-split-zero"; |
617 |
|
static constexpr const char* nlExtTfTaylorDegree__name = "nl-ext-tf-taylor-deg"; |
618 |
|
static constexpr const char* nlExtTfTangentPlanes__name = "nl-ext-tf-tplanes"; |
619 |
|
static constexpr const char* nlExtTangentPlanes__name = "nl-ext-tplanes"; |
620 |
|
static constexpr const char* nlExtTangentPlanesInterleave__name = "nl-ext-tplanes-interleave"; |
621 |
|
static constexpr const char* nlExt__name = "nl-ext"; |
622 |
|
static constexpr const char* nlICP__name = "nl-icp"; |
623 |
|
static constexpr const char* nlRlvMode__name = "nl-rlv"; |
624 |
|
static constexpr const char* pbRewrites__name = "pb-rewrites"; |
625 |
|
static constexpr const char* arithPivotThreshold__name = "pivot-threshold"; |
626 |
|
static constexpr const char* ppAssertMaxSubSize__name = "pp-assert-max-sub-size"; |
627 |
|
static constexpr const char* arithPropagateMaxLength__name = "prop-row-length"; |
628 |
|
static constexpr const char* replayEarlyCloseDepths__name = "replay-early-close-depth"; |
629 |
|
static constexpr const char* replayFailurePenalty__name = "replay-failure-penalty"; |
630 |
|
static constexpr const char* lemmaRejectCutSize__name = "replay-lemma-reject-cut"; |
631 |
|
static constexpr const char* replayNumericFailurePenalty__name = "replay-num-err-penalty"; |
632 |
|
static constexpr const char* replayRejectCutSize__name = "replay-reject-cut"; |
633 |
|
static constexpr const char* soiApproxMajorFailurePen__name = "replay-soi-major-threshold-pen"; |
634 |
|
static constexpr const char* soiApproxMajorFailure__name = "replay-soi-major-threshold"; |
635 |
|
static constexpr const char* soiApproxMinorFailurePen__name = "replay-soi-minor-threshold-pen"; |
636 |
|
static constexpr const char* soiApproxMinorFailure__name = "replay-soi-minor-threshold"; |
637 |
|
static constexpr const char* restrictedPivots__name = "restrict-pivots"; |
638 |
|
static constexpr const char* revertArithModels__name = "revert-arith-models-on-unsat"; |
639 |
|
static constexpr const char* rrTurns__name = "rr-turns"; |
640 |
|
static constexpr const char* trySolveIntStandardEffort__name = "se-solve-int"; |
641 |
|
static constexpr const char* arithSimplexCheckPeriod__name = "simplex-check-period"; |
642 |
|
static constexpr const char* soiQuickExplain__name = "soi-qe"; |
643 |
|
static constexpr const char* arithStandardCheckVarOrderPivots__name = "standard-effort-variable-order-pivots"; |
644 |
|
static constexpr const char* arithUnateLemmaMode__name = "unate-lemmas"; |
645 |
|
static constexpr const char* useApprox__name = "use-approx"; |
646 |
|
static constexpr const char* useFC__name = "use-fcsimplex"; |
647 |
|
static constexpr const char* useSOI__name = "use-soi"; |
648 |
|
// clang-format on |
649 |
|
} |
650 |
|
|
651 |
|
} // namespace options |
652 |
|
|
653 |
|
// clang-format off |
654 |
|
|
655 |
|
// clang-format on |
656 |
|
|
657 |
|
namespace options { |
658 |
|
// clang-format off |
659 |
|
inline int16_t maxApproxDepth__option_t::operator()() const |
660 |
|
{ return Options::current().arith.maxApproxDepth; } |
661 |
1099 |
inline bool brabTest__option_t::operator()() const |
662 |
1099 |
{ return Options::current().arith.brabTest; } |
663 |
9841 |
inline bool arithCongMan__option_t::operator()() const |
664 |
9841 |
{ return Options::current().arith.arithCongMan; } |
665 |
39356 |
inline bool arithEqSolver__option_t::operator()() const |
666 |
39356 |
{ return Options::current().arith.arithEqSolver; } |
667 |
695 |
inline bool arithNoPartialFun__option_t::operator()() const |
668 |
695 |
{ return Options::current().arith.arithNoPartialFun; } |
669 |
124332 |
inline uint16_t arithPropAsLemmaLength__option_t::operator()() const |
670 |
124332 |
{ return Options::current().arith.arithPropAsLemmaLength; } |
671 |
7920642 |
inline ArithPropagationMode arithPropagationMode__option_t::operator()() const |
672 |
7920642 |
{ return Options::current().arith.arithPropagationMode; } |
673 |
31263 |
inline bool arithRewriteEq__option_t::operator()() const |
674 |
31263 |
{ return Options::current().arith.arithRewriteEq; } |
675 |
1484856 |
inline bool collectPivots__option_t::operator()() const |
676 |
1484856 |
{ return Options::current().arith.collectPivots; } |
677 |
|
inline bool doCutAllBounded__option_t::operator()() const |
678 |
|
{ return Options::current().arith.doCutAllBounded; } |
679 |
334 |
inline bool exportDioDecompositions__option_t::operator()() const |
680 |
334 |
{ return Options::current().arith.exportDioDecompositions; } |
681 |
|
inline bool dioRepeat__option_t::operator()() const |
682 |
|
{ return Options::current().arith.dioRepeat; } |
683 |
5228 |
inline bool arithDioSolver__option_t::operator()() const |
684 |
5228 |
{ return Options::current().arith.arithDioSolver; } |
685 |
402 |
inline int dioSolverTurns__option_t::operator()() const |
686 |
402 |
{ return Options::current().arith.dioSolverTurns; } |
687 |
39364 |
inline ErrorSelectionRule arithErrorSelectionRule__option_t::operator()() const |
688 |
39364 |
{ return Options::current().arith.arithErrorSelectionRule; } |
689 |
|
inline bool havePenalties__option_t::operator()() const |
690 |
|
{ return Options::current().arith.havePenalties; } |
691 |
160562 |
inline int16_t arithHeuristicPivots__option_t::operator()() const |
692 |
160562 |
{ return Options::current().arith.arithHeuristicPivots; } |
693 |
|
inline bool replayFailureLemma__option_t::operator()() const |
694 |
|
{ return Options::current().arith.replayFailureLemma; } |
695 |
2691 |
inline unsigned maxCutsInContext__option_t::operator()() const |
696 |
2691 |
{ return Options::current().arith.maxCutsInContext; } |
697 |
19303 |
inline bool arithMLTrick__option_t::operator()() const |
698 |
19303 |
{ return Options::current().arith.arithMLTrick; } |
699 |
|
inline unsigned arithMLTrickSubstitutions__option_t::operator()() const |
700 |
|
{ return Options::current().arith.arithMLTrickSubstitutions; } |
701 |
962791 |
inline bool newProp__option_t::operator()() const |
702 |
962791 |
{ return Options::current().arith.newProp; } |
703 |
1299 |
inline bool nlCad__option_t::operator()() const |
704 |
1299 |
{ return Options::current().arith.nlCad; } |
705 |
345 |
inline bool nlCadUseInitial__option_t::operator()() const |
706 |
345 |
{ return Options::current().arith.nlCadUseInitial; } |
707 |
1191 |
inline NlCadLiftingMode nlCadLifting__option_t::operator()() const |
708 |
1191 |
{ return Options::current().arith.nlCadLifting; } |
709 |
172 |
inline NlCadProjectionMode nlCadProjection__option_t::operator()() const |
710 |
172 |
{ return Options::current().arith.nlCadProjection; } |
711 |
8643 |
inline bool nlExtEntailConflicts__option_t::operator()() const |
712 |
8643 |
{ return Options::current().arith.nlExtEntailConflicts; } |
713 |
425 |
inline bool nlExtFactor__option_t::operator()() const |
714 |
425 |
{ return Options::current().arith.nlExtFactor; } |
715 |
18 |
inline bool nlExtIncPrecision__option_t::operator()() const |
716 |
18 |
{ return Options::current().arith.nlExtIncPrecision; } |
717 |
13736 |
inline bool nlExtPurify__option_t::operator()() const |
718 |
13736 |
{ return Options::current().arith.nlExtPurify; } |
719 |
425 |
inline bool nlExtResBound__option_t::operator()() const |
720 |
425 |
{ return Options::current().arith.nlExtResBound; } |
721 |
31878 |
inline bool nlExtRewrites__option_t::operator()() const |
722 |
31878 |
{ return Options::current().arith.nlExtRewrites; } |
723 |
425 |
inline bool nlExtSplitZero__option_t::operator()() const |
724 |
425 |
{ return Options::current().arith.nlExtSplitZero; } |
725 |
5134 |
inline int16_t nlExtTfTaylorDegree__option_t::operator()() const |
726 |
5134 |
{ return Options::current().arith.nlExtTfTaylorDegree; } |
727 |
425 |
inline bool nlExtTfTangentPlanes__option_t::operator()() const |
728 |
425 |
{ return Options::current().arith.nlExtTfTangentPlanes; } |
729 |
57191 |
inline bool nlExtTangentPlanes__option_t::operator()() const |
730 |
57191 |
{ return Options::current().arith.nlExtTangentPlanes; } |
731 |
142 |
inline bool nlExtTangentPlanesInterleave__option_t::operator()() const |
732 |
142 |
{ return Options::current().arith.nlExtTangentPlanesInterleave; } |
733 |
2183 |
inline NlExtMode nlExt__option_t::operator()() const |
734 |
2183 |
{ return Options::current().arith.nlExt; } |
735 |
458 |
inline bool nlICP__option_t::operator()() const |
736 |
458 |
{ return Options::current().arith.nlICP; } |
737 |
10663 |
inline NlRlvMode nlRlvMode__option_t::operator()() const |
738 |
10663 |
{ return Options::current().arith.nlRlvMode; } |
739 |
16256 |
inline bool pbRewrites__option_t::operator()() const |
740 |
16256 |
{ return Options::current().arith.pbRewrites; } |
741 |
390348 |
inline uint16_t arithPivotThreshold__option_t::operator()() const |
742 |
390348 |
{ return Options::current().arith.arithPivotThreshold; } |
743 |
1399 |
inline unsigned ppAssertMaxSubSize__option_t::operator()() const |
744 |
1399 |
{ return Options::current().arith.ppAssertMaxSubSize; } |
745 |
10285605 |
inline uint16_t arithPropagateMaxLength__option_t::operator()() const |
746 |
10285605 |
{ return Options::current().arith.arithPropagateMaxLength; } |
747 |
|
inline int replayEarlyCloseDepths__option_t::operator()() const |
748 |
|
{ return Options::current().arith.replayEarlyCloseDepths; } |
749 |
|
inline int replayFailurePenalty__option_t::operator()() const |
750 |
|
{ return Options::current().arith.replayFailurePenalty; } |
751 |
|
inline unsigned lemmaRejectCutSize__option_t::operator()() const |
752 |
|
{ return Options::current().arith.lemmaRejectCutSize; } |
753 |
|
inline int replayNumericFailurePenalty__option_t::operator()() const |
754 |
|
{ return Options::current().arith.replayNumericFailurePenalty; } |
755 |
|
inline unsigned replayRejectCutSize__option_t::operator()() const |
756 |
|
{ return Options::current().arith.replayRejectCutSize; } |
757 |
|
inline int soiApproxMajorFailurePen__option_t::operator()() const |
758 |
|
{ return Options::current().arith.soiApproxMajorFailurePen; } |
759 |
|
inline double soiApproxMajorFailure__option_t::operator()() const |
760 |
|
{ return Options::current().arith.soiApproxMajorFailure; } |
761 |
|
inline int soiApproxMinorFailurePen__option_t::operator()() const |
762 |
|
{ return Options::current().arith.soiApproxMinorFailurePen; } |
763 |
|
inline double soiApproxMinorFailure__option_t::operator()() const |
764 |
|
{ return Options::current().arith.soiApproxMinorFailure; } |
765 |
1474385 |
inline bool restrictedPivots__option_t::operator()() const |
766 |
1474385 |
{ return Options::current().arith.restrictedPivots; } |
767 |
12029 |
inline bool revertArithModels__option_t::operator()() const |
768 |
12029 |
{ return Options::current().arith.revertArithModels; } |
769 |
131 |
inline int rrTurns__option_t::operator()() const |
770 |
131 |
{ return Options::current().arith.rrTurns; } |
771 |
|
inline bool trySolveIntStandardEffort__option_t::operator()() const |
772 |
|
{ return Options::current().arith.trySolveIntStandardEffort; } |
773 |
87785 |
inline uint16_t arithSimplexCheckPeriod__option_t::operator()() const |
774 |
87785 |
{ return Options::current().arith.arithSimplexCheckPeriod; } |
775 |
|
inline bool soiQuickExplain__option_t::operator()() const |
776 |
|
{ return Options::current().arith.soiQuickExplain; } |
777 |
114203 |
inline int16_t arithStandardCheckVarOrderPivots__option_t::operator()() const |
778 |
114203 |
{ return Options::current().arith.arithStandardCheckVarOrderPivots; } |
779 |
7622 |
inline ArithUnateLemmaMode arithUnateLemmaMode__option_t::operator()() const |
780 |
7622 |
{ return Options::current().arith.arithUnateLemmaMode; } |
781 |
4472342 |
inline bool useApprox__option_t::operator()() const |
782 |
4472342 |
{ return Options::current().arith.useApprox; } |
783 |
1546812 |
inline bool useFC__option_t::operator()() const |
784 |
1546812 |
{ return Options::current().arith.useFC; } |
785 |
6336 |
inline bool useSOI__option_t::operator()() const |
786 |
6336 |
{ return Options::current().arith.useSOI; } |
787 |
|
// clang-format on |
788 |
|
|
789 |
|
namespace arith |
790 |
|
{ |
791 |
|
// clang-format off |
792 |
|
void setDefaultMaxApproxDepth(Options& opts, int16_t value); |
793 |
|
void setDefaultBrabTest(Options& opts, bool value); |
794 |
|
void setDefaultArithCongMan(Options& opts, bool value); |
795 |
|
void setDefaultArithEqSolver(Options& opts, bool value); |
796 |
|
void setDefaultArithNoPartialFun(Options& opts, bool value); |
797 |
|
void setDefaultArithPropAsLemmaLength(Options& opts, uint16_t value); |
798 |
|
void setDefaultArithPropagationMode(Options& opts, ArithPropagationMode value); |
799 |
|
void setDefaultArithRewriteEq(Options& opts, bool value); |
800 |
|
void setDefaultCollectPivots(Options& opts, bool value); |
801 |
|
void setDefaultDoCutAllBounded(Options& opts, bool value); |
802 |
|
void setDefaultExportDioDecompositions(Options& opts, bool value); |
803 |
|
void setDefaultDioRepeat(Options& opts, bool value); |
804 |
|
void setDefaultArithDioSolver(Options& opts, bool value); |
805 |
|
void setDefaultDioSolverTurns(Options& opts, int value); |
806 |
|
void setDefaultArithErrorSelectionRule(Options& opts, ErrorSelectionRule value); |
807 |
|
void setDefaultHavePenalties(Options& opts, bool value); |
808 |
|
void setDefaultArithHeuristicPivots(Options& opts, int16_t value); |
809 |
|
void setDefaultReplayFailureLemma(Options& opts, bool value); |
810 |
|
void setDefaultMaxCutsInContext(Options& opts, unsigned value); |
811 |
|
void setDefaultArithMLTrick(Options& opts, bool value); |
812 |
|
void setDefaultArithMLTrickSubstitutions(Options& opts, unsigned value); |
813 |
|
void setDefaultNewProp(Options& opts, bool value); |
814 |
|
void setDefaultNlCad(Options& opts, bool value); |
815 |
|
void setDefaultNlCadUseInitial(Options& opts, bool value); |
816 |
|
void setDefaultNlCadLifting(Options& opts, NlCadLiftingMode value); |
817 |
|
void setDefaultNlCadProjection(Options& opts, NlCadProjectionMode value); |
818 |
|
void setDefaultNlExtEntailConflicts(Options& opts, bool value); |
819 |
|
void setDefaultNlExtFactor(Options& opts, bool value); |
820 |
|
void setDefaultNlExtIncPrecision(Options& opts, bool value); |
821 |
|
void setDefaultNlExtPurify(Options& opts, bool value); |
822 |
|
void setDefaultNlExtResBound(Options& opts, bool value); |
823 |
|
void setDefaultNlExtRewrites(Options& opts, bool value); |
824 |
|
void setDefaultNlExtSplitZero(Options& opts, bool value); |
825 |
|
void setDefaultNlExtTfTaylorDegree(Options& opts, int16_t value); |
826 |
|
void setDefaultNlExtTfTangentPlanes(Options& opts, bool value); |
827 |
|
void setDefaultNlExtTangentPlanes(Options& opts, bool value); |
828 |
|
void setDefaultNlExtTangentPlanesInterleave(Options& opts, bool value); |
829 |
|
void setDefaultNlExt(Options& opts, NlExtMode value); |
830 |
|
void setDefaultNlICP(Options& opts, bool value); |
831 |
|
void setDefaultNlRlvMode(Options& opts, NlRlvMode value); |
832 |
|
void setDefaultPbRewrites(Options& opts, bool value); |
833 |
|
void setDefaultArithPivotThreshold(Options& opts, uint16_t value); |
834 |
|
void setDefaultPpAssertMaxSubSize(Options& opts, unsigned value); |
835 |
|
void setDefaultArithPropagateMaxLength(Options& opts, uint16_t value); |
836 |
|
void setDefaultReplayEarlyCloseDepths(Options& opts, int value); |
837 |
|
void setDefaultReplayFailurePenalty(Options& opts, int value); |
838 |
|
void setDefaultLemmaRejectCutSize(Options& opts, unsigned value); |
839 |
|
void setDefaultReplayNumericFailurePenalty(Options& opts, int value); |
840 |
|
void setDefaultReplayRejectCutSize(Options& opts, unsigned value); |
841 |
|
void setDefaultSoiApproxMajorFailurePen(Options& opts, int value); |
842 |
|
void setDefaultSoiApproxMajorFailure(Options& opts, double value); |
843 |
|
void setDefaultSoiApproxMinorFailurePen(Options& opts, int value); |
844 |
|
void setDefaultSoiApproxMinorFailure(Options& opts, double value); |
845 |
|
void setDefaultRestrictedPivots(Options& opts, bool value); |
846 |
|
void setDefaultRevertArithModels(Options& opts, bool value); |
847 |
|
void setDefaultRrTurns(Options& opts, int value); |
848 |
|
void setDefaultTrySolveIntStandardEffort(Options& opts, bool value); |
849 |
|
void setDefaultArithSimplexCheckPeriod(Options& opts, uint16_t value); |
850 |
|
void setDefaultSoiQuickExplain(Options& opts, bool value); |
851 |
|
void setDefaultArithStandardCheckVarOrderPivots(Options& opts, int16_t value); |
852 |
|
void setDefaultArithUnateLemmaMode(Options& opts, ArithUnateLemmaMode value); |
853 |
|
void setDefaultUseApprox(Options& opts, bool value); |
854 |
|
void setDefaultUseFC(Options& opts, bool value); |
855 |
|
void setDefaultUseSOI(Options& opts, bool value); |
856 |
|
// clang-format on |
857 |
|
} |
858 |
|
|
859 |
|
} // namespace options |
860 |
|
} // namespace cvc5 |
861 |
|
|
862 |
|
#endif /* CVC5__OPTIONS__ARITH_H */ |