1 |
|
/****************************************************************************** |
2 |
|
* Top contributors (to current version): |
3 |
|
* Mathias Preiner, Aina Niemetz |
4 |
|
* |
5 |
|
* This file is part of the cvc5 project. |
6 |
|
* |
7 |
|
* Copyright (c) 2009-2021 by the authors listed in the file AUTHORS |
8 |
|
* in the top-level source directory and their institutional affiliations. |
9 |
|
* All rights reserved. See the file COPYING in the top-level source |
10 |
|
* directory for licensing information. |
11 |
|
* **************************************************************************** |
12 |
|
* |
13 |
|
* Option template for option modules. |
14 |
|
* |
15 |
|
* For each <module>_options.toml configuration file, mkoptions.py |
16 |
|
* expands this template and generates a <module>_options.cpp file. |
17 |
|
*/ |
18 |
|
#include "options/arith_options.h" |
19 |
|
|
20 |
|
#include <iostream> |
21 |
|
|
22 |
|
#include "base/check.h" |
23 |
|
#include "options/option_exception.h" |
24 |
|
|
25 |
|
// clang-format off |
26 |
|
namespace cvc5::options { |
27 |
|
|
28 |
|
std::ostream& operator<<(std::ostream& os, ArithPropagationMode mode) |
29 |
|
{ |
30 |
|
switch(mode) { |
31 |
|
case ArithPropagationMode::BOUND_INFERENCE_PROP: |
32 |
|
return os << "ArithPropagationMode::BOUND_INFERENCE_PROP"; |
33 |
|
case ArithPropagationMode::NO_PROP: |
34 |
|
return os << "ArithPropagationMode::NO_PROP"; |
35 |
|
case ArithPropagationMode::BOTH_PROP: |
36 |
|
return os << "ArithPropagationMode::BOTH_PROP"; |
37 |
|
case ArithPropagationMode::UNATE_PROP: |
38 |
|
return os << "ArithPropagationMode::UNATE_PROP"; |
39 |
|
default: |
40 |
|
Unreachable(); |
41 |
|
} |
42 |
|
return os; |
43 |
|
} |
44 |
|
ArithPropagationMode stringToArithPropagationMode(const std::string& optarg) |
45 |
|
{ |
46 |
|
if (optarg == "bi") |
47 |
|
{ |
48 |
|
return ArithPropagationMode::BOUND_INFERENCE_PROP; |
49 |
|
} |
50 |
|
else if (optarg == "none") |
51 |
|
{ |
52 |
|
return ArithPropagationMode::NO_PROP; |
53 |
|
} |
54 |
|
else if (optarg == "both") |
55 |
|
{ |
56 |
|
return ArithPropagationMode::BOTH_PROP; |
57 |
|
} |
58 |
|
else if (optarg == "unate") |
59 |
|
{ |
60 |
|
return ArithPropagationMode::UNATE_PROP; |
61 |
|
} |
62 |
|
else if (optarg == "help") |
63 |
|
{ |
64 |
|
std::cerr << "This decides on kind of propagation arithmetic attempts to do during the\n" |
65 |
|
"search.\n" |
66 |
|
"Available modes for --arith-prop are:\n" |
67 |
|
"+ bi\n" |
68 |
|
" (Bounds Inference) infers bounds on basic variables using the upper and lower\n" |
69 |
|
" bounds of the non-basic variables in the tableau.\n" |
70 |
|
"+ both (default)\n" |
71 |
|
" Use bounds inference and unate.\n" |
72 |
|
"+ unate\n" |
73 |
|
" Use constraints to do unate propagation.\n"; |
74 |
|
std::exit(1); |
75 |
|
} |
76 |
|
throw OptionException(std::string("unknown option for --arith-prop: `") + |
77 |
|
optarg + "'. Try --arith-prop=help."); |
78 |
|
} |
79 |
|
std::ostream& operator<<(std::ostream& os, ErrorSelectionRule mode) |
80 |
|
{ |
81 |
|
switch(mode) { |
82 |
|
case ErrorSelectionRule::VAR_ORDER: |
83 |
|
return os << "ErrorSelectionRule::VAR_ORDER"; |
84 |
|
case ErrorSelectionRule::SUM_METRIC: |
85 |
|
return os << "ErrorSelectionRule::SUM_METRIC"; |
86 |
|
case ErrorSelectionRule::MINIMUM_AMOUNT: |
87 |
|
return os << "ErrorSelectionRule::MINIMUM_AMOUNT"; |
88 |
|
case ErrorSelectionRule::MAXIMUM_AMOUNT: |
89 |
|
return os << "ErrorSelectionRule::MAXIMUM_AMOUNT"; |
90 |
|
default: |
91 |
|
Unreachable(); |
92 |
|
} |
93 |
|
return os; |
94 |
|
} |
95 |
|
ErrorSelectionRule stringToErrorSelectionRule(const std::string& optarg) |
96 |
|
{ |
97 |
|
if (optarg == "varord") |
98 |
|
{ |
99 |
|
return ErrorSelectionRule::VAR_ORDER; |
100 |
|
} |
101 |
|
else if (optarg == "sum") |
102 |
|
{ |
103 |
|
return ErrorSelectionRule::SUM_METRIC; |
104 |
|
} |
105 |
|
else if (optarg == "min") |
106 |
|
{ |
107 |
|
return ErrorSelectionRule::MINIMUM_AMOUNT; |
108 |
|
} |
109 |
|
else if (optarg == "max") |
110 |
|
{ |
111 |
|
return ErrorSelectionRule::MAXIMUM_AMOUNT; |
112 |
|
} |
113 |
|
else if (optarg == "help") |
114 |
|
{ |
115 |
|
std::cerr << "This decides on the rule used by simplex during heuristic rounds for deciding\n" |
116 |
|
"the next basic variable to select.\n" |
117 |
|
"Available rules for --error-selection-rule are:\n" |
118 |
|
"+ varord\n" |
119 |
|
" The variable order.\n" |
120 |
|
"+ min (default)\n" |
121 |
|
" The minimum abs() value of the variable's violation of its bound.\n" |
122 |
|
"+ max\n" |
123 |
|
" The maximum violation the bound.\n"; |
124 |
|
std::exit(1); |
125 |
|
} |
126 |
|
throw OptionException(std::string("unknown option for --error-selection-rule: `") + |
127 |
|
optarg + "'. Try --error-selection-rule=help."); |
128 |
|
} |
129 |
|
std::ostream& operator<<(std::ostream& os, NlCadLiftingMode mode) |
130 |
|
{ |
131 |
|
switch(mode) { |
132 |
|
case NlCadLiftingMode::LAZARD: |
133 |
|
return os << "NlCadLiftingMode::LAZARD"; |
134 |
|
case NlCadLiftingMode::REGULAR: |
135 |
|
return os << "NlCadLiftingMode::REGULAR"; |
136 |
|
default: |
137 |
|
Unreachable(); |
138 |
|
} |
139 |
|
return os; |
140 |
|
} |
141 |
|
NlCadLiftingMode stringToNlCadLiftingMode(const std::string& optarg) |
142 |
|
{ |
143 |
|
if (optarg == "lazard") |
144 |
|
{ |
145 |
|
return NlCadLiftingMode::LAZARD; |
146 |
|
} |
147 |
|
else if (optarg == "regular") |
148 |
|
{ |
149 |
|
return NlCadLiftingMode::REGULAR; |
150 |
|
} |
151 |
|
else if (optarg == "help") |
152 |
|
{ |
153 |
|
std::cerr << "Modes for the CAD lifting in non-linear arithmetic.\n" |
154 |
|
"Available modes for --nl-cad-lift are:\n" |
155 |
|
"+ lazard\n" |
156 |
|
" Lazard's lifting scheme.\n" |
157 |
|
"+ regular (default)\n" |
158 |
|
" Regular lifting.\n"; |
159 |
|
std::exit(1); |
160 |
|
} |
161 |
|
throw OptionException(std::string("unknown option for --nl-cad-lift: `") + |
162 |
|
optarg + "'. Try --nl-cad-lift=help."); |
163 |
|
} |
164 |
|
std::ostream& operator<<(std::ostream& os, NlCadProjectionMode mode) |
165 |
|
{ |
166 |
|
switch(mode) { |
167 |
|
case NlCadProjectionMode::LAZARD: |
168 |
|
return os << "NlCadProjectionMode::LAZARD"; |
169 |
|
case NlCadProjectionMode::MCCALLUM: |
170 |
|
return os << "NlCadProjectionMode::MCCALLUM"; |
171 |
|
case NlCadProjectionMode::LAZARDMOD: |
172 |
|
return os << "NlCadProjectionMode::LAZARDMOD"; |
173 |
|
default: |
174 |
|
Unreachable(); |
175 |
|
} |
176 |
|
return os; |
177 |
|
} |
178 |
|
NlCadProjectionMode stringToNlCadProjectionMode(const std::string& optarg) |
179 |
|
{ |
180 |
|
if (optarg == "lazard") |
181 |
|
{ |
182 |
|
return NlCadProjectionMode::LAZARD; |
183 |
|
} |
184 |
|
else if (optarg == "mccallum") |
185 |
|
{ |
186 |
|
return NlCadProjectionMode::MCCALLUM; |
187 |
|
} |
188 |
|
else if (optarg == "lazard-mod") |
189 |
|
{ |
190 |
|
return NlCadProjectionMode::LAZARDMOD; |
191 |
|
} |
192 |
|
else if (optarg == "help") |
193 |
|
{ |
194 |
|
std::cerr << "Modes for the CAD projection operator in non-linear arithmetic.\n" |
195 |
|
"Available modes for --nl-cad-proj are:\n" |
196 |
|
"+ lazard\n" |
197 |
|
" Lazard's projection operator.\n" |
198 |
|
"+ mccallum (default)\n" |
199 |
|
" McCallum's projection operator.\n" |
200 |
|
"+ lazard-mod\n" |
201 |
|
" A modification of Lazard's projection operator.\n"; |
202 |
|
std::exit(1); |
203 |
|
} |
204 |
|
throw OptionException(std::string("unknown option for --nl-cad-proj: `") + |
205 |
|
optarg + "'. Try --nl-cad-proj=help."); |
206 |
|
} |
207 |
|
std::ostream& operator<<(std::ostream& os, NlExtMode mode) |
208 |
|
{ |
209 |
|
switch(mode) { |
210 |
|
case NlExtMode::NONE: |
211 |
|
return os << "NlExtMode::NONE"; |
212 |
|
case NlExtMode::FULL: |
213 |
|
return os << "NlExtMode::FULL"; |
214 |
|
case NlExtMode::LIGHT: |
215 |
|
return os << "NlExtMode::LIGHT"; |
216 |
|
default: |
217 |
|
Unreachable(); |
218 |
|
} |
219 |
|
return os; |
220 |
|
} |
221 |
126 |
NlExtMode stringToNlExtMode(const std::string& optarg) |
222 |
|
{ |
223 |
126 |
if (optarg == "none") |
224 |
|
{ |
225 |
6 |
return NlExtMode::NONE; |
226 |
|
} |
227 |
120 |
else if (optarg == "full") |
228 |
|
{ |
229 |
120 |
return NlExtMode::FULL; |
230 |
|
} |
231 |
|
else if (optarg == "light") |
232 |
|
{ |
233 |
|
return NlExtMode::LIGHT; |
234 |
|
} |
235 |
|
else if (optarg == "help") |
236 |
|
{ |
237 |
|
std::cerr << "Modes for the non-linear linearization\n" |
238 |
|
"Available modes for --nl-ext are:\n" |
239 |
|
"+ none\n" |
240 |
|
" Disable linearization approach\n" |
241 |
|
"+ full (default)\n" |
242 |
|
" Use all lemma schemes\n" |
243 |
|
"+ light\n" |
244 |
|
" Only use a few light-weight lemma schemes\n"; |
245 |
|
std::exit(1); |
246 |
|
} |
247 |
|
throw OptionException(std::string("unknown option for --nl-ext: `") + |
248 |
|
optarg + "'. Try --nl-ext=help."); |
249 |
|
} |
250 |
|
std::ostream& operator<<(std::ostream& os, NlRlvMode mode) |
251 |
|
{ |
252 |
|
switch(mode) { |
253 |
|
case NlRlvMode::NONE: |
254 |
|
return os << "NlRlvMode::NONE"; |
255 |
|
case NlRlvMode::ALWAYS: |
256 |
|
return os << "NlRlvMode::ALWAYS"; |
257 |
|
case NlRlvMode::INTERLEAVE: |
258 |
|
return os << "NlRlvMode::INTERLEAVE"; |
259 |
|
default: |
260 |
|
Unreachable(); |
261 |
|
} |
262 |
|
return os; |
263 |
|
} |
264 |
6 |
NlRlvMode stringToNlRlvMode(const std::string& optarg) |
265 |
|
{ |
266 |
6 |
if (optarg == "none") |
267 |
|
{ |
268 |
3 |
return NlRlvMode::NONE; |
269 |
|
} |
270 |
3 |
else if (optarg == "always") |
271 |
|
{ |
272 |
3 |
return NlRlvMode::ALWAYS; |
273 |
|
} |
274 |
|
else if (optarg == "interleave") |
275 |
|
{ |
276 |
|
return NlRlvMode::INTERLEAVE; |
277 |
|
} |
278 |
|
else if (optarg == "help") |
279 |
|
{ |
280 |
|
std::cerr << "Modes for using relevance of assertions in non-linear arithmetic.\n" |
281 |
|
"Available modes for --nl-rlv are:\n" |
282 |
|
"+ none (default)\n" |
283 |
|
" Do not use relevance.\n" |
284 |
|
"+ always\n" |
285 |
|
" Always use relevance.\n" |
286 |
|
"+ interleave\n" |
287 |
|
" Alternate rounds using relevance.\n"; |
288 |
|
std::exit(1); |
289 |
|
} |
290 |
|
throw OptionException(std::string("unknown option for --nl-rlv: `") + |
291 |
|
optarg + "'. Try --nl-rlv=help."); |
292 |
|
} |
293 |
|
std::ostream& operator<<(std::ostream& os, ArithUnateLemmaMode mode) |
294 |
|
{ |
295 |
|
switch(mode) { |
296 |
|
case ArithUnateLemmaMode::INEQUALITY: |
297 |
|
return os << "ArithUnateLemmaMode::INEQUALITY"; |
298 |
|
case ArithUnateLemmaMode::ALL: |
299 |
|
return os << "ArithUnateLemmaMode::ALL"; |
300 |
|
case ArithUnateLemmaMode::EQUALITY: |
301 |
|
return os << "ArithUnateLemmaMode::EQUALITY"; |
302 |
|
case ArithUnateLemmaMode::NO: |
303 |
|
return os << "ArithUnateLemmaMode::NO"; |
304 |
|
default: |
305 |
|
Unreachable(); |
306 |
|
} |
307 |
|
return os; |
308 |
|
} |
309 |
|
ArithUnateLemmaMode stringToArithUnateLemmaMode(const std::string& optarg) |
310 |
|
{ |
311 |
|
if (optarg == "ineqs") |
312 |
|
{ |
313 |
|
return ArithUnateLemmaMode::INEQUALITY; |
314 |
|
} |
315 |
|
else if (optarg == "all") |
316 |
|
{ |
317 |
|
return ArithUnateLemmaMode::ALL; |
318 |
|
} |
319 |
|
else if (optarg == "eqs") |
320 |
|
{ |
321 |
|
return ArithUnateLemmaMode::EQUALITY; |
322 |
|
} |
323 |
|
else if (optarg == "none") |
324 |
|
{ |
325 |
|
return ArithUnateLemmaMode::NO; |
326 |
|
} |
327 |
|
else if (optarg == "help") |
328 |
|
{ |
329 |
|
std::cerr << "Unate lemmas are generated before SAT search begins using the relationship of\n" |
330 |
|
"constant terms and polynomials.\n" |
331 |
|
"Available modes for --unate-lemmas are:\n" |
332 |
|
"+ ineqs\n" |
333 |
|
" Outputs lemmas of the general form (<= p c) implies (<= p d) for c < d.\n" |
334 |
|
"+ all (default)\n" |
335 |
|
" A combination of inequalities and equalities.\n" |
336 |
|
"+ eqs\n" |
337 |
|
" Outputs lemmas of the general forms (= p c) implies (<= p d) for c < d, or (=\n" |
338 |
|
" p c) implies (not (= p d)) for c != d.\n"; |
339 |
|
std::exit(1); |
340 |
|
} |
341 |
|
throw OptionException(std::string("unknown option for --unate-lemmas: `") + |
342 |
|
optarg + "'. Try --unate-lemmas=help."); |
343 |
|
} |
344 |
|
|
345 |
|
namespace arith |
346 |
|
{ |
347 |
|
// clang-format off |
348 |
|
void setDefaultMaxApproxDepth(Options& opts, int64_t value) |
349 |
|
{ |
350 |
|
if (!opts.arith.maxApproxDepthWasSetByUser) { |
351 |
|
opts.arith.maxApproxDepth = value; |
352 |
|
} |
353 |
|
} |
354 |
|
void setDefaultBrabTest(Options& opts, bool value) |
355 |
|
{ |
356 |
|
if (!opts.arith.brabTestWasSetByUser) { |
357 |
|
opts.arith.brabTest = value; |
358 |
|
} |
359 |
|
} |
360 |
|
void setDefaultArithCongMan(Options& opts, bool value) |
361 |
|
{ |
362 |
|
if (!opts.arith.arithCongManWasSetByUser) { |
363 |
|
opts.arith.arithCongMan = value; |
364 |
|
} |
365 |
|
} |
366 |
|
void setDefaultArithEqSolver(Options& opts, bool value) |
367 |
|
{ |
368 |
|
if (!opts.arith.arithEqSolverWasSetByUser) { |
369 |
|
opts.arith.arithEqSolver = value; |
370 |
|
} |
371 |
|
} |
372 |
|
void setDefaultArithNoPartialFun(Options& opts, bool value) |
373 |
|
{ |
374 |
|
if (!opts.arith.arithNoPartialFunWasSetByUser) { |
375 |
|
opts.arith.arithNoPartialFun = value; |
376 |
|
} |
377 |
|
} |
378 |
|
void setDefaultArithPropAsLemmaLength(Options& opts, uint64_t value) |
379 |
|
{ |
380 |
|
if (!opts.arith.arithPropAsLemmaLengthWasSetByUser) { |
381 |
|
opts.arith.arithPropAsLemmaLength = value; |
382 |
|
} |
383 |
|
} |
384 |
|
void setDefaultArithPropagationMode(Options& opts, ArithPropagationMode value) |
385 |
|
{ |
386 |
|
if (!opts.arith.arithPropagationModeWasSetByUser) { |
387 |
|
opts.arith.arithPropagationMode = value; |
388 |
|
} |
389 |
|
} |
390 |
|
void setDefaultArithRewriteEq(Options& opts, bool value) |
391 |
|
{ |
392 |
|
if (!opts.arith.arithRewriteEqWasSetByUser) { |
393 |
|
opts.arith.arithRewriteEq = value; |
394 |
|
} |
395 |
|
} |
396 |
|
void setDefaultCollectPivots(Options& opts, bool value) |
397 |
|
{ |
398 |
|
if (!opts.arith.collectPivotsWasSetByUser) { |
399 |
|
opts.arith.collectPivots = value; |
400 |
|
} |
401 |
|
} |
402 |
|
void setDefaultDoCutAllBounded(Options& opts, bool value) |
403 |
|
{ |
404 |
|
if (!opts.arith.doCutAllBoundedWasSetByUser) { |
405 |
|
opts.arith.doCutAllBounded = value; |
406 |
|
} |
407 |
|
} |
408 |
|
void setDefaultExportDioDecompositions(Options& opts, bool value) |
409 |
|
{ |
410 |
|
if (!opts.arith.exportDioDecompositionsWasSetByUser) { |
411 |
|
opts.arith.exportDioDecompositions = value; |
412 |
|
} |
413 |
|
} |
414 |
|
void setDefaultDioRepeat(Options& opts, bool value) |
415 |
|
{ |
416 |
|
if (!opts.arith.dioRepeatWasSetByUser) { |
417 |
|
opts.arith.dioRepeat = value; |
418 |
|
} |
419 |
|
} |
420 |
|
void setDefaultArithDioSolver(Options& opts, bool value) |
421 |
|
{ |
422 |
|
if (!opts.arith.arithDioSolverWasSetByUser) { |
423 |
|
opts.arith.arithDioSolver = value; |
424 |
|
} |
425 |
|
} |
426 |
|
void setDefaultDioSolverTurns(Options& opts, int64_t value) |
427 |
|
{ |
428 |
|
if (!opts.arith.dioSolverTurnsWasSetByUser) { |
429 |
|
opts.arith.dioSolverTurns = value; |
430 |
|
} |
431 |
|
} |
432 |
|
void setDefaultArithErrorSelectionRule(Options& opts, ErrorSelectionRule value) |
433 |
|
{ |
434 |
|
if (!opts.arith.arithErrorSelectionRuleWasSetByUser) { |
435 |
|
opts.arith.arithErrorSelectionRule = value; |
436 |
|
} |
437 |
|
} |
438 |
|
void setDefaultHavePenalties(Options& opts, bool value) |
439 |
|
{ |
440 |
|
if (!opts.arith.havePenaltiesWasSetByUser) { |
441 |
|
opts.arith.havePenalties = value; |
442 |
|
} |
443 |
|
} |
444 |
|
void setDefaultArithHeuristicPivots(Options& opts, int64_t value) |
445 |
|
{ |
446 |
|
if (!opts.arith.arithHeuristicPivotsWasSetByUser) { |
447 |
|
opts.arith.arithHeuristicPivots = value; |
448 |
|
} |
449 |
|
} |
450 |
|
void setDefaultReplayFailureLemma(Options& opts, bool value) |
451 |
|
{ |
452 |
|
if (!opts.arith.replayFailureLemmaWasSetByUser) { |
453 |
|
opts.arith.replayFailureLemma = value; |
454 |
|
} |
455 |
|
} |
456 |
|
void setDefaultMaxCutsInContext(Options& opts, uint64_t value) |
457 |
|
{ |
458 |
|
if (!opts.arith.maxCutsInContextWasSetByUser) { |
459 |
|
opts.arith.maxCutsInContext = value; |
460 |
|
} |
461 |
|
} |
462 |
|
void setDefaultArithMLTrick(Options& opts, bool value) |
463 |
|
{ |
464 |
|
if (!opts.arith.arithMLTrickWasSetByUser) { |
465 |
|
opts.arith.arithMLTrick = value; |
466 |
|
} |
467 |
|
} |
468 |
|
void setDefaultArithMLTrickSubstitutions(Options& opts, uint64_t value) |
469 |
|
{ |
470 |
|
if (!opts.arith.arithMLTrickSubstitutionsWasSetByUser) { |
471 |
|
opts.arith.arithMLTrickSubstitutions = value; |
472 |
|
} |
473 |
|
} |
474 |
|
void setDefaultNewProp(Options& opts, bool value) |
475 |
|
{ |
476 |
|
if (!opts.arith.newPropWasSetByUser) { |
477 |
|
opts.arith.newProp = value; |
478 |
|
} |
479 |
|
} |
480 |
|
void setDefaultNlCad(Options& opts, bool value) |
481 |
|
{ |
482 |
|
if (!opts.arith.nlCadWasSetByUser) { |
483 |
|
opts.arith.nlCad = value; |
484 |
|
} |
485 |
|
} |
486 |
|
void setDefaultNlCadUseInitial(Options& opts, bool value) |
487 |
|
{ |
488 |
|
if (!opts.arith.nlCadUseInitialWasSetByUser) { |
489 |
|
opts.arith.nlCadUseInitial = value; |
490 |
|
} |
491 |
|
} |
492 |
|
void setDefaultNlCadLifting(Options& opts, NlCadLiftingMode value) |
493 |
|
{ |
494 |
|
if (!opts.arith.nlCadLiftingWasSetByUser) { |
495 |
|
opts.arith.nlCadLifting = value; |
496 |
|
} |
497 |
|
} |
498 |
|
void setDefaultNlCadProjection(Options& opts, NlCadProjectionMode value) |
499 |
|
{ |
500 |
|
if (!opts.arith.nlCadProjectionWasSetByUser) { |
501 |
|
opts.arith.nlCadProjection = value; |
502 |
|
} |
503 |
|
} |
504 |
|
void setDefaultNlExtEntailConflicts(Options& opts, bool value) |
505 |
|
{ |
506 |
|
if (!opts.arith.nlExtEntailConflictsWasSetByUser) { |
507 |
|
opts.arith.nlExtEntailConflicts = value; |
508 |
|
} |
509 |
|
} |
510 |
|
void setDefaultNlExtFactor(Options& opts, bool value) |
511 |
|
{ |
512 |
|
if (!opts.arith.nlExtFactorWasSetByUser) { |
513 |
|
opts.arith.nlExtFactor = value; |
514 |
|
} |
515 |
|
} |
516 |
|
void setDefaultNlExtIncPrecision(Options& opts, bool value) |
517 |
|
{ |
518 |
|
if (!opts.arith.nlExtIncPrecisionWasSetByUser) { |
519 |
|
opts.arith.nlExtIncPrecision = value; |
520 |
|
} |
521 |
|
} |
522 |
|
void setDefaultNlExtPurify(Options& opts, bool value) |
523 |
|
{ |
524 |
|
if (!opts.arith.nlExtPurifyWasSetByUser) { |
525 |
|
opts.arith.nlExtPurify = value; |
526 |
|
} |
527 |
|
} |
528 |
|
void setDefaultNlExtResBound(Options& opts, bool value) |
529 |
|
{ |
530 |
|
if (!opts.arith.nlExtResBoundWasSetByUser) { |
531 |
|
opts.arith.nlExtResBound = value; |
532 |
|
} |
533 |
|
} |
534 |
|
void setDefaultNlExtRewrites(Options& opts, bool value) |
535 |
|
{ |
536 |
|
if (!opts.arith.nlExtRewritesWasSetByUser) { |
537 |
|
opts.arith.nlExtRewrites = value; |
538 |
|
} |
539 |
|
} |
540 |
|
void setDefaultNlExtSplitZero(Options& opts, bool value) |
541 |
|
{ |
542 |
|
if (!opts.arith.nlExtSplitZeroWasSetByUser) { |
543 |
|
opts.arith.nlExtSplitZero = value; |
544 |
|
} |
545 |
|
} |
546 |
|
void setDefaultNlExtTfTaylorDegree(Options& opts, int64_t value) |
547 |
|
{ |
548 |
|
if (!opts.arith.nlExtTfTaylorDegreeWasSetByUser) { |
549 |
|
opts.arith.nlExtTfTaylorDegree = value; |
550 |
|
} |
551 |
|
} |
552 |
|
void setDefaultNlExtTfTangentPlanes(Options& opts, bool value) |
553 |
|
{ |
554 |
|
if (!opts.arith.nlExtTfTangentPlanesWasSetByUser) { |
555 |
|
opts.arith.nlExtTfTangentPlanes = value; |
556 |
|
} |
557 |
|
} |
558 |
|
void setDefaultNlExtTangentPlanes(Options& opts, bool value) |
559 |
|
{ |
560 |
|
if (!opts.arith.nlExtTangentPlanesWasSetByUser) { |
561 |
|
opts.arith.nlExtTangentPlanes = value; |
562 |
|
} |
563 |
|
} |
564 |
|
void setDefaultNlExtTangentPlanesInterleave(Options& opts, bool value) |
565 |
|
{ |
566 |
|
if (!opts.arith.nlExtTangentPlanesInterleaveWasSetByUser) { |
567 |
|
opts.arith.nlExtTangentPlanesInterleave = value; |
568 |
|
} |
569 |
|
} |
570 |
|
void setDefaultNlExt(Options& opts, NlExtMode value) |
571 |
|
{ |
572 |
|
if (!opts.arith.nlExtWasSetByUser) { |
573 |
|
opts.arith.nlExt = value; |
574 |
|
} |
575 |
|
} |
576 |
|
void setDefaultNlICP(Options& opts, bool value) |
577 |
|
{ |
578 |
|
if (!opts.arith.nlICPWasSetByUser) { |
579 |
|
opts.arith.nlICP = value; |
580 |
|
} |
581 |
|
} |
582 |
|
void setDefaultNlRlvAssertBounds(Options& opts, bool value) |
583 |
|
{ |
584 |
|
if (!opts.arith.nlRlvAssertBoundsWasSetByUser) { |
585 |
|
opts.arith.nlRlvAssertBounds = value; |
586 |
|
} |
587 |
|
} |
588 |
|
void setDefaultNlRlvMode(Options& opts, NlRlvMode value) |
589 |
|
{ |
590 |
|
if (!opts.arith.nlRlvModeWasSetByUser) { |
591 |
|
opts.arith.nlRlvMode = value; |
592 |
|
} |
593 |
|
} |
594 |
|
void setDefaultPbRewrites(Options& opts, bool value) |
595 |
|
{ |
596 |
|
if (!opts.arith.pbRewritesWasSetByUser) { |
597 |
|
opts.arith.pbRewrites = value; |
598 |
|
} |
599 |
|
} |
600 |
|
void setDefaultArithPivotThreshold(Options& opts, uint64_t value) |
601 |
|
{ |
602 |
|
if (!opts.arith.arithPivotThresholdWasSetByUser) { |
603 |
|
opts.arith.arithPivotThreshold = value; |
604 |
|
} |
605 |
|
} |
606 |
|
void setDefaultPpAssertMaxSubSize(Options& opts, uint64_t value) |
607 |
|
{ |
608 |
|
if (!opts.arith.ppAssertMaxSubSizeWasSetByUser) { |
609 |
|
opts.arith.ppAssertMaxSubSize = value; |
610 |
|
} |
611 |
|
} |
612 |
|
void setDefaultArithPropagateMaxLength(Options& opts, uint64_t value) |
613 |
|
{ |
614 |
|
if (!opts.arith.arithPropagateMaxLengthWasSetByUser) { |
615 |
|
opts.arith.arithPropagateMaxLength = value; |
616 |
|
} |
617 |
|
} |
618 |
|
void setDefaultReplayEarlyCloseDepths(Options& opts, int64_t value) |
619 |
|
{ |
620 |
|
if (!opts.arith.replayEarlyCloseDepthsWasSetByUser) { |
621 |
|
opts.arith.replayEarlyCloseDepths = value; |
622 |
|
} |
623 |
|
} |
624 |
|
void setDefaultReplayFailurePenalty(Options& opts, int64_t value) |
625 |
|
{ |
626 |
|
if (!opts.arith.replayFailurePenaltyWasSetByUser) { |
627 |
|
opts.arith.replayFailurePenalty = value; |
628 |
|
} |
629 |
|
} |
630 |
|
void setDefaultLemmaRejectCutSize(Options& opts, uint64_t value) |
631 |
|
{ |
632 |
|
if (!opts.arith.lemmaRejectCutSizeWasSetByUser) { |
633 |
|
opts.arith.lemmaRejectCutSize = value; |
634 |
|
} |
635 |
|
} |
636 |
|
void setDefaultReplayNumericFailurePenalty(Options& opts, int64_t value) |
637 |
|
{ |
638 |
|
if (!opts.arith.replayNumericFailurePenaltyWasSetByUser) { |
639 |
|
opts.arith.replayNumericFailurePenalty = value; |
640 |
|
} |
641 |
|
} |
642 |
|
void setDefaultReplayRejectCutSize(Options& opts, uint64_t value) |
643 |
|
{ |
644 |
|
if (!opts.arith.replayRejectCutSizeWasSetByUser) { |
645 |
|
opts.arith.replayRejectCutSize = value; |
646 |
|
} |
647 |
|
} |
648 |
|
void setDefaultSoiApproxMajorFailurePen(Options& opts, int64_t value) |
649 |
|
{ |
650 |
|
if (!opts.arith.soiApproxMajorFailurePenWasSetByUser) { |
651 |
|
opts.arith.soiApproxMajorFailurePen = value; |
652 |
|
} |
653 |
|
} |
654 |
|
void setDefaultSoiApproxMajorFailure(Options& opts, double value) |
655 |
|
{ |
656 |
|
if (!opts.arith.soiApproxMajorFailureWasSetByUser) { |
657 |
|
opts.arith.soiApproxMajorFailure = value; |
658 |
|
} |
659 |
|
} |
660 |
|
void setDefaultSoiApproxMinorFailurePen(Options& opts, int64_t value) |
661 |
|
{ |
662 |
|
if (!opts.arith.soiApproxMinorFailurePenWasSetByUser) { |
663 |
|
opts.arith.soiApproxMinorFailurePen = value; |
664 |
|
} |
665 |
|
} |
666 |
|
void setDefaultSoiApproxMinorFailure(Options& opts, double value) |
667 |
|
{ |
668 |
|
if (!opts.arith.soiApproxMinorFailureWasSetByUser) { |
669 |
|
opts.arith.soiApproxMinorFailure = value; |
670 |
|
} |
671 |
|
} |
672 |
|
void setDefaultRestrictedPivots(Options& opts, bool value) |
673 |
|
{ |
674 |
|
if (!opts.arith.restrictedPivotsWasSetByUser) { |
675 |
|
opts.arith.restrictedPivots = value; |
676 |
|
} |
677 |
|
} |
678 |
|
void setDefaultRevertArithModels(Options& opts, bool value) |
679 |
|
{ |
680 |
|
if (!opts.arith.revertArithModelsWasSetByUser) { |
681 |
|
opts.arith.revertArithModels = value; |
682 |
|
} |
683 |
|
} |
684 |
|
void setDefaultRrTurns(Options& opts, int64_t value) |
685 |
|
{ |
686 |
|
if (!opts.arith.rrTurnsWasSetByUser) { |
687 |
|
opts.arith.rrTurns = value; |
688 |
|
} |
689 |
|
} |
690 |
|
void setDefaultTrySolveIntStandardEffort(Options& opts, bool value) |
691 |
|
{ |
692 |
|
if (!opts.arith.trySolveIntStandardEffortWasSetByUser) { |
693 |
|
opts.arith.trySolveIntStandardEffort = value; |
694 |
|
} |
695 |
|
} |
696 |
|
void setDefaultArithSimplexCheckPeriod(Options& opts, uint64_t value) |
697 |
|
{ |
698 |
|
if (!opts.arith.arithSimplexCheckPeriodWasSetByUser) { |
699 |
|
opts.arith.arithSimplexCheckPeriod = value; |
700 |
|
} |
701 |
|
} |
702 |
|
void setDefaultSoiQuickExplain(Options& opts, bool value) |
703 |
|
{ |
704 |
|
if (!opts.arith.soiQuickExplainWasSetByUser) { |
705 |
|
opts.arith.soiQuickExplain = value; |
706 |
|
} |
707 |
|
} |
708 |
|
void setDefaultArithStandardCheckVarOrderPivots(Options& opts, int64_t value) |
709 |
|
{ |
710 |
|
if (!opts.arith.arithStandardCheckVarOrderPivotsWasSetByUser) { |
711 |
|
opts.arith.arithStandardCheckVarOrderPivots = value; |
712 |
|
} |
713 |
|
} |
714 |
|
void setDefaultArithUnateLemmaMode(Options& opts, ArithUnateLemmaMode value) |
715 |
|
{ |
716 |
|
if (!opts.arith.arithUnateLemmaModeWasSetByUser) { |
717 |
|
opts.arith.arithUnateLemmaMode = value; |
718 |
|
} |
719 |
|
} |
720 |
|
void setDefaultUseApprox(Options& opts, bool value) |
721 |
|
{ |
722 |
|
if (!opts.arith.useApproxWasSetByUser) { |
723 |
|
opts.arith.useApprox = value; |
724 |
|
} |
725 |
|
} |
726 |
|
void setDefaultUseFC(Options& opts, bool value) |
727 |
|
{ |
728 |
|
if (!opts.arith.useFCWasSetByUser) { |
729 |
|
opts.arith.useFC = value; |
730 |
|
} |
731 |
|
} |
732 |
|
void setDefaultUseSOI(Options& opts, bool value) |
733 |
|
{ |
734 |
|
if (!opts.arith.useSOIWasSetByUser) { |
735 |
|
opts.arith.useSOI = value; |
736 |
|
} |
737 |
|
} |
738 |
|
// clang-format on |
739 |
|
} |
740 |
|
|
741 |
29517 |
} // namespace cvc5::options |
742 |
|
// clang-format on |