2 name = "Arithmetic theory"
3 header = "options/arith_options.h"
6 name = "arithUnateLemmaMode"
8 long = "unate-lemmas=MODE"
9 type = "ArithUnateLemmaMode"
10 default = "ALL_PRESOLVE_LEMMAS"
11 handler = "stringToArithUnateLemmaMode"
12 includes = ["options/arith_unate_lemma_mode.h"]
14 help = "determines which lemmas to add before solving (default is 'all', see --unate-lemmas=help)"
17 name = "arithPropagationMode"
19 long = "arith-prop=MODE"
20 type = "ArithPropagationMode"
22 handler = "stringToArithPropagationMode"
23 includes = ["options/arith_propagation_mode.h"]
25 help = "turns on arithmetic propagation (default is 'old', see --arith-prop=help)"
27 # The maximum number of difference pivots to do per invocation of simplex.
28 # If this is negative, the number of pivots done is the number of variables.
29 # If this is not set by the user, different logics are free to chose different
32 name = "arithHeuristicPivots"
34 long = "heuristic-pivots=N"
37 help = "the number of times to apply the heuristic pivot rule; if N < 0, this defaults to the number of variables; if this is unset, this is tuned by the logic selection"
40 # The maximum number of variable order pivots to do per invocation of simplex.
41 # If this is negative, the number of pivots done is unlimited.
42 # If this is not set by the user, different logics are free to chose different
45 name = "arithStandardCheckVarOrderPivots"
47 long = "standard-effort-variable-order-pivots=N"
50 help = "limits the number of pivots in a single invocation of check() at a non-full effort level using Bland's pivot rule"
53 name = "arithErrorSelectionRule"
55 long = "error-selection-rule=RULE"
56 type = "ErrorSelectionRule"
57 default = "MINIMUM_AMOUNT"
58 handler = "stringToErrorSelectionRule"
59 includes = ["options/arith_heuristic_pivot_rule.h"]
61 help = "change the pivot rule for the basic variable (default is 'min', see --pivot-rule help)"
63 # The number of pivots before simplex rechecks every basic variable for a conflict
65 name = "arithSimplexCheckPeriod"
67 long = "simplex-check-period=N"
71 help = "the number of pivots to do in simplex before rechecking for a conflict on all variables"
73 # This is the pivots per basic variable that can be done using heuristic choices
74 # before variable order must be used.
75 # If this is not set by the user, different logics are free to chose different
78 name = "arithPivotThreshold"
80 long = "pivot-threshold=N"
83 help = "sets the number of pivots using --pivot-rule per basic variable per simplex instance before using variable order"
86 name = "arithPropagateMaxLength"
88 long = "prop-row-length=N"
92 help = "sets the maximum row length to be used in propagation"
95 name = "arithDioSolver"
101 help = "turns on Linear Diophantine Equation solver (Griggio, JSAT 2012)"
103 # Whether to split (= x y) into (and (<= x y) (>= x y)) in
104 # arithmetic preprocessing.
106 name = "arithRewriteEq"
108 long = "arith-rewrite-equalities"
111 help = "turns on the preprocessing rewrite turning equalities into a conjunction of inequalities"
114 name = "arithMLTrick"
115 smt_name = "miplib-trick"
117 long = "miplib-trick"
121 help = "turns on the preprocessing step of attempting to infer bounds on miplib problems"
124 name = "arithMLTrickSubstitutions"
125 smt_name = "miplib-trick-subs"
127 long = "miplib-trick-subs=N"
131 help = "do substitution for miplib 'tmp' vars if defined in <= N eliminated vars"
134 name = "doCutAllBounded"
136 long = "cut-all-bounded"
139 help = "turns on the integer solving step of periodically cutting all integer variables that have both upper and lower bounds"
142 name = "maxCutsInContext"
144 long = "maxCutsInContext"
148 help = "maximum cuts in a given context before signalling a restart"
151 name = "revertArithModels"
153 long = "revert-arith-models-on-unsat"
157 help = "revert the arithmetic model to a known safe model on unsat if one is cached"
160 name = "havePenalties"
162 long = "fc-penalties"
165 help = "turns on degenerate pivot penalties"
170 long = "use-fcsimplex"
173 help = "use focusing and converging simplex (FMCAD 2013 submission)"
181 help = "use sum of infeasibility simplex (FMCAD 2013 submission)"
184 name = "restrictedPivots"
186 long = "restrict-pivots"
189 help = "have a pivot cap for simplex at effort levels below fullEffort"
192 name = "collectPivots"
194 long = "collect-pivot-stats"
197 help = "collect the pivot history"
205 help = "attempt to use an approximate solver"
208 name = "maxApproxDepth"
210 long = "approx-branch-depth"
213 help = "maximum branch depth the approximate solver is allowed to take"
216 name = "exportDioDecompositions"
221 help = "let skolem variables for integer divisibility constraints leak from the dio solver"
229 help = "use the new row propagation system"
232 name = "arithPropAsLemmaLength"
234 long = "arith-prop-clauses"
237 help = "rows shorter than this are propagated as clauses"
240 name = "soiQuickExplain"
245 help = "use quick explain to minimize the sum of infeasibility conflicts"
250 long = "rewrite-divk"
253 help = "rewrite division and mod when by a constant into linear terms"
256 name = "trySolveIntStandardEffort"
258 long = "se-solve-int"
262 help = "attempt to use the approximate solve integer method on standard effort"
265 name = "replayFailureLemma"
267 long = "lemmas-on-replay-failure"
271 help = "attempt to use external lemmas if approximate solve integer failed"
274 name = "dioSolverTurns"
280 help = "turns in a row dio solver cutting gets"
289 help = "round robin turn"
298 help = "handle dio solver constraints in mass or one at a time"
301 name = "replayEarlyCloseDepths"
303 long = "replay-early-close-depth"
307 help = "multiples of the depths to try to close the approx log eagerly"
310 name = "replayFailurePenalty"
312 long = "replay-failure-penalty"
316 help = "number of solve integer attempts to skips after a numeric failure"
319 name = "replayNumericFailurePenalty"
321 long = "replay-num-err-penalty"
325 help = "number of solve integer attempts to skips after a numeric failure"
328 name = "replayRejectCutSize"
330 long = "replay-reject-cut"
334 help = "maximum complexity of any coefficient while replaying cuts"
337 name = "lemmaRejectCutSize"
339 long = "replay-lemma-reject-cut"
343 help = "maximum complexity of any coefficient while outputting replaying cut lemmas"
346 name = "soiApproxMajorFailure"
348 long = "replay-soi-major-threshold"
352 help = "threshold for a major tolerance failure by the approximate solver"
355 name = "soiApproxMajorFailurePen"
357 long = "replay-soi-major-threshold-pen"
361 help = "threshold for a major tolerance failure by the approximate solver"
364 name = "soiApproxMinorFailure"
366 long = "replay-soi-minor-threshold"
370 help = "threshold for a minor tolerance failure by the approximate solver"
373 name = "soiApproxMinorFailurePen"
375 long = "replay-soi-minor-threshold-pen"
379 help = "threshold for a minor tolerance failure by the approximate solver"
382 name = "ppAssertMaxSubSize"
384 long = "pp-assert-max-sub-size"
388 help = "threshold for substituting an equality in ppAssert"
391 name = "arithNoPartialFun"
393 long = "arith-no-partial-fun"
397 help = "do not use partial function semantics for arithmetic (not SMT LIB compliant)"
406 help = "apply pseudo boolean rewrites"
409 name = "sNormInferEq"
411 long = "snorm-infer-eq"
415 help = "infer equalities based on Shostak normalization"
424 help = "extended approach to non-linear"
427 name = "nlExtResBound"
429 long = "nl-ext-rbound"
433 help = "use resolution-style inference for inferring new bounds"
438 long = "nl-ext-factor"
442 help = "use factoring inference in non-linear solver"
445 name = "nlExtTangentPlanes"
447 long = "nl-ext-tplanes"
451 help = "use non-terminating tangent plane strategy for non-linear"
454 name = "nlExtTfTangentPlanes"
456 long = "nl-ext-tf-tplanes"
460 help = "use non-terminating tangent plane strategy for transcendental functions for non-linear"
463 name = "nlExtEntailConflicts"
465 long = "nl-ext-ent-conf"
469 help = "check for entailed conflicts in non-linear solver"
472 name = "nlExtRewrites"
474 long = "nl-ext-rewrite"
478 help = "do rewrites in non-linear solver"
481 name = "nlExtSolveSubs"
483 long = "nl-ext-solve-subs"
487 help = "do solving for determining constant substitutions"
492 long = "nl-ext-purify"
496 help = "purify non-linear terms at preprocess"
499 name = "nlExtSplitZero"
501 long = "nl-ext-split-zero"
505 help = "intial splits on zero for all variables"
508 name = "nlExtTfTaylorDegree"
510 long = "nl-ext-tf-taylor-deg=N"
513 help = "initial degree of polynomials for Taylor approximation"
516 name = "nlExtTfIncPrecision"
518 long = "nl-ext-tf-inc-prec"
522 help = "whether to increment the precision for transcendental function constraints"