2 name = "Arithmetic theory"
3 header = "options/arith_options.h"
6 name = "arithUnateLemmaMode"
8 long = "unate-lemmas=MODE"
9 type = "ArithUnateLemmaMode"
12 help = "determines which lemmas to add before solving (default is 'all', see --unate-lemmas=help)"
13 help_mode = "Unate lemmas are generated before SAT search begins using the relationship of constant terms and polynomials."
16 help = "A combination of inequalities and equalities."
17 [[option.mode.EQUALITY]]
19 help = "Outputs lemmas of the general forms (= p c) implies (<= p d) for c < d, or (= p c) implies (not (= p d)) for c != d."
20 [[option.mode.INEQUALITY]]
22 help = "Outputs lemmas of the general form (<= p c) implies (<= p d) for c < d."
27 name = "arithPropagationMode"
29 long = "arith-prop=MODE"
30 type = "ArithPropagationMode"
33 help = "turns on arithmetic propagation (default is 'old', see --arith-prop=help)"
34 help_mode = "This decides on kind of propagation arithmetic attempts to do during the search."
35 [[option.mode.NO_PROP]]
37 [[option.mode.UNATE_PROP]]
39 help = "Use constraints to do unate propagation."
40 [[option.mode.BOUND_INFERENCE_PROP]]
42 help = "(Bounds Inference) infers bounds on basic variables using the upper and lower bounds of the non-basic variables in the tableau."
43 [[option.mode.BOTH_PROP]]
45 help = "Use bounds inference and unate."
49 # The maximum number of difference pivots to do per invocation of simplex.
50 # If this is negative, the number of pivots done is the number of variables.
51 # If this is not set by the user, different logics are free to chose different
54 name = "arithHeuristicPivots"
56 long = "heuristic-pivots=N"
59 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"
62 # The maximum number of variable order pivots to do per invocation of simplex.
63 # If this is negative, the number of pivots done is unlimited.
64 # If this is not set by the user, different logics are free to chose different
67 name = "arithStandardCheckVarOrderPivots"
69 long = "standard-effort-variable-order-pivots=N"
72 help = "limits the number of pivots in a single invocation of check() at a non-full effort level using Bland's pivot rule"
75 name = "arithErrorSelectionRule"
77 long = "error-selection-rule=RULE"
78 type = "ErrorSelectionRule"
79 default = "MINIMUM_AMOUNT"
81 help = "change the pivot rule for the basic variable (default is 'min', see --pivot-rule help)"
82 help_mode = "This decides on the rule used by simplex during heuristic rounds for deciding the next basic variable to select."
83 [[option.mode.MINIMUM_AMOUNT]]
85 help = "The minimum abs() value of the variable's violation of its bound."
86 [[option.mode.VAR_ORDER]]
88 help = "The variable order."
89 [[option.mode.MAXIMUM_AMOUNT]]
91 help = "The maximum violation the bound."
92 [[option.mode.SUM_METRIC]]
95 # The number of pivots before simplex rechecks every basic variable for a conflict
97 name = "arithSimplexCheckPeriod"
99 long = "simplex-check-period=N"
103 help = "the number of pivots to do in simplex before rechecking for a conflict on all variables"
105 # This is the pivots per basic variable that can be done using heuristic choices
106 # before variable order must be used.
107 # If this is not set by the user, different logics are free to chose different
110 name = "arithPivotThreshold"
112 long = "pivot-threshold=N"
115 help = "sets the number of pivots using --pivot-rule per basic variable per simplex instance before using variable order"
118 name = "arithPropagateMaxLength"
120 long = "prop-row-length=N"
124 help = "sets the maximum row length to be used in propagation"
127 name = "arithDioSolver"
133 help = "turns on Linear Diophantine Equation solver (Griggio, JSAT 2012)"
135 # Whether to split (= x y) into (and (<= x y) (>= x y)) in
136 # arithmetic preprocessing.
138 name = "arithRewriteEq"
140 long = "arith-rewrite-equalities"
143 help = "turns on the preprocessing rewrite turning equalities into a conjunction of inequalities"
146 name = "arithMLTrick"
147 smt_name = "miplib-trick"
149 long = "miplib-trick"
152 help = "turns on the preprocessing step of attempting to infer bounds on miplib problems"
155 name = "arithMLTrickSubstitutions"
156 smt_name = "miplib-trick-subs"
158 long = "miplib-trick-subs=N"
162 help = "do substitution for miplib 'tmp' vars if defined in <= N eliminated vars"
165 name = "doCutAllBounded"
167 long = "cut-all-bounded"
170 help = "turns on the integer solving step of periodically cutting all integer variables that have both upper and lower bounds"
173 name = "maxCutsInContext"
175 long = "maxCutsInContext=N"
179 help = "maximum cuts in a given context before signalling a restart"
182 name = "revertArithModels"
184 long = "revert-arith-models-on-unsat"
188 help = "revert the arithmetic model to a known safe model on unsat if one is cached"
191 name = "havePenalties"
193 long = "fc-penalties"
196 help = "turns on degenerate pivot penalties"
201 long = "use-fcsimplex"
204 help = "use focusing and converging simplex (FMCAD 2013 submission)"
212 help = "use sum of infeasibility simplex (FMCAD 2013 submission)"
215 name = "restrictedPivots"
217 long = "restrict-pivots"
220 help = "have a pivot cap for simplex at effort levels below fullEffort"
223 name = "collectPivots"
225 long = "collect-pivot-stats"
228 help = "collect the pivot history"
236 help = "attempt to use an approximate solver"
239 name = "maxApproxDepth"
241 long = "approx-branch-depth=N"
244 help = "maximum branch depth the approximate solver is allowed to take"
247 name = "exportDioDecompositions"
252 help = "let skolem variables for integer divisibility constraints leak from the dio solver"
260 help = "use the new row propagation system"
263 name = "arithPropAsLemmaLength"
265 long = "arith-prop-clauses=N"
268 help = "rows shorter than this are propagated as clauses"
271 name = "soiQuickExplain"
276 help = "use quick explain to minimize the sum of infeasibility conflicts"
279 name = "trySolveIntStandardEffort"
281 long = "se-solve-int"
285 help = "attempt to use the approximate solve integer method on standard effort"
288 name = "replayFailureLemma"
290 long = "lemmas-on-replay-failure"
294 help = "attempt to use external lemmas if approximate solve integer failed"
297 name = "dioSolverTurns"
303 help = "turns in a row dio solver cutting gets"
312 help = "round robin turn"
321 help = "handle dio solver constraints in mass or one at a time"
324 name = "replayEarlyCloseDepths"
326 long = "replay-early-close-depth=N"
330 help = "multiples of the depths to try to close the approx log eagerly"
333 name = "replayFailurePenalty"
335 long = "replay-failure-penalty=N"
339 help = "number of solve integer attempts to skips after a numeric failure"
342 name = "replayNumericFailurePenalty"
344 long = "replay-num-err-penalty=N"
348 help = "number of solve integer attempts to skips after a numeric failure"
351 name = "replayRejectCutSize"
353 long = "replay-reject-cut=N"
357 help = "maximum complexity of any coefficient while replaying cuts"
360 name = "lemmaRejectCutSize"
362 long = "replay-lemma-reject-cut=N"
366 help = "maximum complexity of any coefficient while outputting replaying cut lemmas"
369 name = "soiApproxMajorFailure"
371 long = "replay-soi-major-threshold=T"
375 help = "threshold for a major tolerance failure by the approximate solver"
378 name = "soiApproxMajorFailurePen"
380 long = "replay-soi-major-threshold-pen=N"
384 help = "threshold for a major tolerance failure by the approximate solver"
387 name = "soiApproxMinorFailure"
389 long = "replay-soi-minor-threshold=T"
393 help = "threshold for a minor tolerance failure by the approximate solver"
396 name = "soiApproxMinorFailurePen"
398 long = "replay-soi-minor-threshold-pen=N"
402 help = "threshold for a minor tolerance failure by the approximate solver"
405 name = "ppAssertMaxSubSize"
407 long = "pp-assert-max-sub-size=N"
411 help = "threshold for substituting an equality in ppAssert"
414 name = "arithNoPartialFun"
416 long = "arith-no-partial-fun"
420 help = "do not use partial function semantics for arithmetic (not SMT LIB compliant)"
429 help = "apply pseudo boolean rewrites"
438 help = "incremental linearization approach to non-linear"
441 name = "nlExtResBound"
443 long = "nl-ext-rbound"
447 help = "use resolution-style inference for inferring new bounds in non-linear incremental linearization solver"
452 long = "nl-ext-factor"
456 help = "use factoring inference in non-linear incremental linearization solver"
459 name = "nlExtTangentPlanes"
461 long = "nl-ext-tplanes"
465 help = "use non-terminating tangent plane strategy for non-linear incremental linearization solver"
468 name = "nlExtTangentPlanesInterleave"
470 long = "nl-ext-tplanes-interleave"
473 help = "interleave tangent plane strategy for non-linear incremental linearization solver"
476 name = "nlExtTfTangentPlanes"
478 long = "nl-ext-tf-tplanes"
482 help = "use non-terminating tangent plane strategy for transcendental functions for non-linear incremental linearization solver"
485 name = "nlExtEntailConflicts"
487 long = "nl-ext-ent-conf"
491 help = "check for entailed conflicts in non-linear solver"
494 name = "nlExtRewrites"
496 long = "nl-ext-rewrite"
500 help = "do context-dependent simplification based on rewrites in non-linear solver"
505 long = "nl-ext-purify"
509 help = "purify non-linear terms at preprocess"
512 name = "nlExtSplitZero"
514 long = "nl-ext-split-zero"
518 help = "initial splits on zero for all variables"
521 name = "nlExtTfTaylorDegree"
523 long = "nl-ext-tf-taylor-deg=N"
526 help = "initial degree of polynomials for Taylor approximation"
529 name = "nlExtIncPrecision"
531 long = "nl-ext-inc-prec"
535 help = "whether to increment the precision for irrational function constraints"
544 help = "whether to use simple rounding, similar to a unit-cube test, for integers"