diff options
Diffstat (limited to 'src/options/arith_options')
| -rw-r--r-- | src/options/arith_options | 164 |
1 files changed, 164 insertions, 0 deletions
diff --git a/src/options/arith_options b/src/options/arith_options new file mode 100644 index 000000000..9737d5382 --- /dev/null +++ b/src/options/arith_options @@ -0,0 +1,164 @@ +# +# Option specification file for CVC4 +# See src/options/base_options for a description of this file format +# + +module ARITH "options/arith_options.h" Arithmetic theory + +option arithUnateLemmaMode --unate-lemmas=MODE ArithUnateLemmaMode :handler CVC4::options::stringToArithUnateLemmaMode :default ALL_PRESOLVE_LEMMAS :handler-include "options/options_handler_interface.h" :include "options/arith_unate_lemma_mode.h" + determines which lemmas to add before solving (default is 'all', see --unate-lemmas=help) + +option arithPropagationMode --arith-prop=MODE ArithPropagationMode :handler CVC4::options::stringToArithPropagationMode :default BOTH_PROP :handler-include "options/options_handler_interface.h" :include "options/arith_propagation_mode.h" + turns on arithmetic propagation (default is 'old', see --arith-prop=help) + +# The maximum number of difference pivots to do per invocation of simplex. +# If this is negative, the number of pivots done is the number of variables. +# If this is not set by the user, different logics are free to chose different +# defaults. +option arithHeuristicPivots --heuristic-pivots=N int16_t :default 0 :read-write + 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 + +# The maximum number of variable order pivots to do per invocation of simplex. +# If this is negative, the number of pivots done is unlimited. +# If this is not set by the user, different logics are free to chose different +# defaults. +expert-option arithStandardCheckVarOrderPivots --standard-effort-variable-order-pivots=N int16_t :default -1 :read-write + limits the number of pivots in a single invocation of check() at a non-full effort level using Bland's pivot rule + +option arithErrorSelectionRule --error-selection-rule=RULE ErrorSelectionRule :handler CVC4::options::stringToErrorSelectionRule :default MINIMUM_AMOUNT :handler-include "options/options_handler_interface.h" :include "options/arith_heuristic_pivot_rule.h" + change the pivot rule for the basic variable (default is 'min', see --pivot-rule help) + +# The number of pivots before simplex rechecks every basic variable for a conflict +option arithSimplexCheckPeriod --simplex-check-period=N uint16_t :default 200 + the number of pivots to do in simplex before rechecking for a conflict on all variables + +# This is the pivots per basic variable that can be done using heuristic choices +# before variable order must be used. +# If this is not set by the user, different logics are free to chose different +# defaults. +option arithPivotThreshold --pivot-threshold=N uint16_t :default 2 :read-write + sets the number of pivots using --pivot-rule per basic variable per simplex instance before using variable order + +option arithPropagateMaxLength --prop-row-length=N uint16_t :default 16 + sets the maximum row length to be used in propagation + +option arithDioSolver /--disable-dio-solver bool :default true + turns off Linear Diophantine Equation solver (Griggio, JSAT 2012) + +# Whether to split (= x y) into (and (<= x y) (>= x y)) in +# arithmetic preprocessing. +option arithRewriteEq --enable-arith-rewrite-equalities/--disable-arith-rewrite-equalities bool :default false :read-write + turns on the preprocessing rewrite turning equalities into a conjunction of inequalities +/turns off the preprocessing rewrite turning equalities into a conjunction of inequalities + + +option arithMLTrick miplib-trick --enable-miplib-trick/--disable-miplib-trick bool :default false + turns on the preprocessing step of attempting to infer bounds on miplib problems +/turns off the preprocessing step of attempting to infer bounds on miplib problems + +option arithMLTrickSubstitutions miplib-trick-subs --miplib-trick-subs=N unsigned :default 1 + do substitution for miplib 'tmp' vars if defined in <= N eliminated vars + +option doCutAllBounded --cut-all-bounded bool :default false :read-write + turns on the integer solving step of periodically cutting all integer variables that have both upper and lower bounds +/turns off the integer solving step of periodically cutting all integer variables that have both upper and lower bounds + +option maxCutsInContext --maxCutsInContext unsigned :default 65535 + maximum cuts in a given context before signalling a restart + +option revertArithModels --revert-arith-models-on-unsat bool :default false + revert the arithmetic model to a known safe model on unsat if one is cached + +option havePenalties --fc-penalties bool :default false :read-write + turns on degenerate pivot penalties +/turns off degenerate pivot penalties + +option useFC --use-fcsimplex bool :default false :read-write + use focusing and converging simplex (FMCAD 2013 submission) + +option useSOI --use-soi bool :default false :read-write + use sum of infeasibility simplex (FMCAD 2013 submission) + +option restrictedPivots --restrict-pivots bool :default true :read-write + have a pivot cap for simplex at effort levels below fullEffort + +option collectPivots --collect-pivot-stats bool :default false :read-write + collect the pivot history + +option useApprox --use-approx bool :default false :read-write + attempt to use an approximate solver + +option maxApproxDepth --approx-branch-depth int16_t :default 200 :read-write + maximum branch depth the approximate solver is allowed to take + +option exportDioDecompositions --dio-decomps bool :default false :read-write + let skolem variables for integer divisibility constraints leak from the dio solver + +option newProp --new-prop bool :default false :read-write + use the new row propagation system + +option arithPropAsLemmaLength --arith-prop-clauses uint16_t :default 8 :read-write + rows shorter than this are propagated as clauses + +option soiQuickExplain --soi-qe bool :default false :read-write + use quick explain to minimize the sum of infeasibility conflicts + +option rewriteDivk rewrite-divk --rewrite-divk bool :default false :read-write + rewrite division and mod when by a constant into linear terms + +option trySolveIntStandardEffort --se-solve-int bool :default false + attempt to use the approximate solve integer method on standard effort + +option replayFailureLemma --lemmas-on-replay-failure bool :default false + attempt to use external lemmas if approximate solve integer failed + +option dioSolverTurns --dio-turns int :default 10 + turns in a row dio solver cutting gets + +option rrTurns --rr-turns int :default 3 + round robin turn + +option dioRepeat --dio-repeat bool :default false + handle dio solver constraints in mass or one at a time + +option replayEarlyCloseDepths --replay-early-close-depth int :default 1 + multiples of the depths to try to close the approx log eagerly + +option replayFailurePenalty --replay-failure-penalty int :default 100 + number of solve integer attempts to skips after a numeric failure + +option replayNumericFailurePenalty --replay-num-err-penalty int :default 4194304 + number of solve integer attempts to skips after a numeric failure + +option replayRejectCutSize --replay-reject-cut unsigned :default 25500 + maximum complexity of any coefficient while replaying cuts + +option lemmaRejectCutSize --replay-lemma-reject-cut unsigned :default 25500 + maximum complexity of any coefficient while outputing replaying cut lemmas + +option soiApproxMajorFailure --replay-soi-major-threshold double :default .01 + threshold for a major tolerance failure by the approximate solver + +option soiApproxMajorFailurePen --replay-soi-major-threshold-pen int :default 50 + threshold for a major tolerance failure by the approximate solver + +option soiApproxMinorFailure --replay-soi-minor-threshold double :default .0001 + threshold for a minor tolerance failure by the approximate solver + +option soiApproxMinorFailurePen --replay-soi-minor-threshold-pen int :default 10 + threshold for a minor tolerance failure by the approximate solver + +option ppAssertMaxSubSize --pp-assert-max-sub-size unsigned :default 2 + threshold for substituting an equality in ppAssert + +option maxReplayTree --max-replay-tree int :default 512 + threshold for attempting to replay a tree + + +option pbRewrites --pb-rewrites bool :default false + apply pseudo boolean rewrites + +option pbRewriteThreshold --pb-rewrite-threshold int :default 256 + threshold of number of pseudoboolean variables to have before doing rewrites + +endmodule |