2 name = "Arithmetic Theory"
5 name = "arithUnateLemmaMode"
7 long = "unate-lemmas=MODE"
8 type = "ArithUnateLemmaMode"
10 help = "determines which lemmas to add before solving (default is 'all', see --unate-lemmas=help)"
11 help_mode = "Unate lemmas are generated before SAT search begins using the relationship of constant terms and polynomials."
14 help = "A combination of inequalities and equalities."
15 [[option.mode.EQUALITY]]
17 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."
18 [[option.mode.INEQUALITY]]
20 help = "Outputs lemmas of the general form (<= p c) implies (<= p d) for c < d."
25 name = "arithPropagationMode"
27 long = "arith-prop=MODE"
28 type = "ArithPropagationMode"
30 help = "turns on arithmetic propagation (default is 'old', see --arith-prop=help)"
31 help_mode = "This decides on kind of propagation arithmetic attempts to do during the search."
32 [[option.mode.NO_PROP]]
34 [[option.mode.UNATE_PROP]]
36 help = "Use constraints to do unate propagation."
37 [[option.mode.BOUND_INFERENCE_PROP]]
39 help = "(Bounds Inference) infers bounds on basic variables using the upper and lower bounds of the non-basic variables in the tableau."
40 [[option.mode.BOTH_PROP]]
42 help = "Use bounds inference and unate."
46 # The maximum number of difference pivots to do per invocation of simplex.
47 # If this is negative, the number of pivots done is the number of variables.
48 # If this is not set by the user, different logics are free to chose different
51 name = "arithHeuristicPivots"
53 long = "heuristic-pivots=N"
56 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"
59 # The maximum number of variable order pivots to do per invocation of simplex.
60 # If this is negative, the number of pivots done is unlimited.
61 # If this is not set by the user, different logics are free to chose different
64 name = "arithStandardCheckVarOrderPivots"
66 long = "standard-effort-variable-order-pivots=N"
69 help = "limits the number of pivots in a single invocation of check() at a non-full effort level using Bland's pivot rule"
72 name = "arithErrorSelectionRule"
74 long = "error-selection-rule=RULE"
75 type = "ErrorSelectionRule"
76 default = "MINIMUM_AMOUNT"
77 help = "change the pivot rule for the basic variable (default is 'min', see --pivot-rule help)"
78 help_mode = "This decides on the rule used by simplex during heuristic rounds for deciding the next basic variable to select."
79 [[option.mode.MINIMUM_AMOUNT]]
81 help = "The minimum abs() value of the variable's violation of its bound."
82 [[option.mode.VAR_ORDER]]
84 help = "The variable order."
85 [[option.mode.MAXIMUM_AMOUNT]]
87 help = "The maximum violation the bound."
88 [[option.mode.SUM_METRIC]]
91 # The number of pivots before simplex rechecks every basic variable for a conflict
93 name = "arithSimplexCheckPeriod"
95 long = "simplex-check-period=N"
98 help = "the number of pivots to do in simplex before rechecking for a conflict on all variables"
100 # This is the pivots per basic variable that can be done using heuristic choices
101 # before variable order must be used.
102 # If this is not set by the user, different logics are free to chose different
105 name = "arithPivotThreshold"
107 long = "pivot-threshold=N"
110 help = "sets the number of pivots using --pivot-rule per basic variable per simplex instance before using variable order"
113 name = "arithPropagateMaxLength"
115 long = "prop-row-length=N"
118 help = "sets the maximum row length to be used in propagation"
121 name = "arithDioSolver"
126 help = "turns on Linear Diophantine Equation solver (Griggio, JSAT 2012)"
128 # Whether to split (= x y) into (and (<= x y) (>= x y)) in
129 # arithmetic preprocessing.
131 name = "arithRewriteEq"
133 long = "arith-rewrite-equalities"
136 help = "turns on the preprocessing rewrite turning equalities into a conjunction of inequalities"
139 name = "arithMLTrick"
141 long = "miplib-trick"
144 help = "turns on the preprocessing step of attempting to infer bounds on miplib problems"
147 name = "arithMLTrickSubstitutions"
149 long = "miplib-trick-subs=N"
152 help = "do substitution for miplib 'tmp' vars if defined in <= N eliminated vars"
155 name = "doCutAllBounded"
157 long = "cut-all-bounded"
160 help = "turns on the integer solving step of periodically cutting all integer variables that have both upper and lower bounds"
163 name = "maxCutsInContext"
165 long = "maxCutsInContext=N"
168 help = "maximum cuts in a given context before signalling a restart"
171 name = "revertArithModels"
173 long = "revert-arith-models-on-unsat"
176 help = "revert the arithmetic model to a known safe model on unsat if one is cached"
179 name = "havePenalties"
181 long = "fc-penalties"
184 help = "turns on degenerate pivot penalties"
189 long = "use-fcsimplex"
192 help = "use focusing and converging simplex (FMCAD 2013 submission)"
200 help = "use sum of infeasibility simplex (FMCAD 2013 submission)"
203 name = "restrictedPivots"
205 long = "restrict-pivots"
208 help = "have a pivot cap for simplex at effort levels below fullEffort"
211 name = "collectPivots"
213 long = "collect-pivot-stats"
216 help = "collect the pivot history"
224 help = "attempt to use an approximate solver"
227 name = "maxApproxDepth"
229 long = "approx-branch-depth=N"
232 help = "maximum branch depth the approximate solver is allowed to take"
235 name = "exportDioDecompositions"
240 help = "let skolem variables for integer divisibility constraints leak from the dio solver"
248 help = "use the new row propagation system"
251 name = "arithPropAsLemmaLength"
253 long = "arith-prop-clauses=N"
256 help = "rows shorter than this are propagated as clauses"
259 name = "soiQuickExplain"
264 help = "use quick explain to minimize the sum of infeasibility conflicts"
267 name = "trySolveIntStandardEffort"
269 long = "se-solve-int"
272 help = "attempt to use the approximate solve integer method on standard effort"
275 name = "replayFailureLemma"
277 long = "lemmas-on-replay-failure"
280 help = "attempt to use external lemmas if approximate solve integer failed"
283 name = "dioSolverTurns"
288 help = "turns in a row dio solver cutting gets"
296 help = "round robin turn"
304 help = "handle dio solver constraints in mass or one at a time"
307 name = "replayEarlyCloseDepths"
309 long = "replay-early-close-depth=N"
312 help = "multiples of the depths to try to close the approx log eagerly"
315 name = "replayFailurePenalty"
317 long = "replay-failure-penalty=N"
320 help = "number of solve integer attempts to skips after a numeric failure"
323 name = "replayNumericFailurePenalty"
325 long = "replay-num-err-penalty=N"
328 help = "number of solve integer attempts to skips after a numeric failure"
331 name = "replayRejectCutSize"
333 long = "replay-reject-cut=N"
336 help = "maximum complexity of any coefficient while replaying cuts"
339 name = "lemmaRejectCutSize"
341 long = "replay-lemma-reject-cut=N"
344 help = "maximum complexity of any coefficient while outputting replaying cut lemmas"
347 name = "soiApproxMajorFailure"
349 long = "replay-soi-major-threshold=T"
352 help = "threshold for a major tolerance failure by the approximate solver"
355 name = "soiApproxMajorFailurePen"
357 long = "replay-soi-major-threshold-pen=N"
360 help = "threshold for a major tolerance failure by the approximate solver"
363 name = "soiApproxMinorFailure"
365 long = "replay-soi-minor-threshold=T"
368 help = "threshold for a minor tolerance failure by the approximate solver"
371 name = "soiApproxMinorFailurePen"
373 long = "replay-soi-minor-threshold-pen=N"
376 help = "threshold for a minor tolerance failure by the approximate solver"
379 name = "ppAssertMaxSubSize"
381 long = "pp-assert-max-sub-size=N"
384 help = "threshold for substituting an equality in ppAssert"
387 name = "arithNoPartialFun"
389 long = "arith-no-partial-fun"
392 help = "do not use partial function semantics for arithmetic (not SMT LIB compliant)"
400 help = "apply pseudo boolean rewrites"
408 help = "incremental linearization approach to non-linear"
409 help_mode = "Modes for the non-linear linearization"
412 help = "Disable linearization approach"
413 [[option.mode.LIGHT]]
415 help = "Only use a few light-weight lemma schemes"
418 help = "Use all lemma schemes"
421 name = "nlExtResBound"
423 long = "nl-ext-rbound"
426 help = "use resolution-style inference for inferring new bounds in non-linear incremental linearization solver"
431 long = "nl-ext-factor"
434 help = "use factoring inference in non-linear incremental linearization solver"
437 name = "nlExtTangentPlanes"
439 long = "nl-ext-tplanes"
442 help = "use non-terminating tangent plane strategy for non-linear incremental linearization solver"
445 name = "nlExtTangentPlanesInterleave"
447 long = "nl-ext-tplanes-interleave"
450 help = "interleave tangent plane strategy for non-linear incremental linearization solver"
453 name = "nlExtTfTangentPlanes"
455 long = "nl-ext-tf-tplanes"
458 help = "use non-terminating tangent plane strategy for transcendental functions for non-linear incremental linearization solver"
461 name = "nlExtEntailConflicts"
463 long = "nl-ext-ent-conf"
466 help = "check for entailed conflicts in non-linear solver"
469 name = "nlExtRewrites"
471 long = "nl-ext-rewrite"
474 help = "do context-dependent simplification based on rewrites in non-linear solver"
479 long = "nl-ext-purify"
482 help = "purify non-linear terms at preprocess"
485 name = "nlExtSplitZero"
487 long = "nl-ext-split-zero"
490 help = "initial splits on zero for all variables"
493 name = "nlExtTfTaylorDegree"
495 long = "nl-ext-tf-taylor-deg=N"
498 help = "initial degree of polynomials for Taylor approximation"
501 name = "nlExtIncPrecision"
503 long = "nl-ext-inc-prec"
506 help = "whether to increment the precision for irrational function constraints"
514 help = "choose mode for using relevance of assertions in non-linear arithmetic"
515 help_mode = "Modes for using relevance of assertions in non-linear arithmetic."
518 help = "Do not use relevance."
519 [[option.mode.INTERLEAVE]]
521 help = "Alternate rounds using relevance."
522 [[option.mode.ALWAYS]]
524 help = "Always use relevance."
532 help = "whether to use simple rounding, similar to a unit-cube test, for integers"
540 help = "whether to use the cylindrical algebraic decomposition solver for non-linear arithmetic"
543 name = "nlCadUseInitial"
545 long = "nl-cad-initial"
548 help = "whether to use the linear model as initial guess for the cylindrical algebraic decomposition solver"
551 name = "nlCadProjection"
553 long = "nl-cad-proj=MODE"
554 type = "NlCadProjectionMode"
556 help = "choose the CAD projection operator"
557 help_mode = "Modes for the CAD projection operator in non-linear arithmetic."
558 [[option.mode.MCCALLUM]]
560 help = "McCallum's projection operator."
561 [[option.mode.LAZARD]]
563 help = "Lazard's projection operator."
564 [[option.mode.LAZARDMOD]]
566 help = "A modification of Lazard's projection operator."
569 name = "nlCadLifting"
571 long = "nl-cad-lift=MODE"
572 type = "NlCadLiftingMode"
574 help = "choose the CAD lifting mode"
575 help_mode = "Modes for the CAD lifting in non-linear arithmetic."
576 [[option.mode.REGULAR]]
578 help = "Regular lifting."
579 [[option.mode.LAZARD]]
581 help = "Lazard's lifting scheme."
589 help = "whether to use ICP-style propagations for non-linear arithmetic"
592 name = "arithEqSolver"
594 long = "arith-eq-solver"
597 help = "whether to use the equality solver in the theory of arithmetic"
600 name = "arithCongMan"
602 long = "arith-cong-man"
605 help = "(experimental) whether to use the congruence manager when the equality solver is enabled"