diff options
Diffstat (limited to 'src/theory/arith/options')
| -rw-r--r-- | src/theory/arith/options | 55 |
1 files changed, 55 insertions, 0 deletions
diff --git a/src/theory/arith/options b/src/theory/arith/options new file mode 100644 index 000000000..8b45a6da2 --- /dev/null +++ b/src/theory/arith/options @@ -0,0 +1,55 @@ +# +# Option specification file for CVC4 +# See src/options/base_options for a description of this file format +# + +module ARITH "theory/arith/options.h" Arithmetic theory + +option arithUnateLemmaMode --unate-lemmas=MODE ArithUnateLemmaMode :handler CVC4::theory::arith::stringToArithUnateLemmaMode :default ALL_PRESOLVE_LEMMAS :handler-include "theory/arith/options_handlers.h" :include "theory/arith/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::theory::arith::stringToArithPropagationMode :default BOTH_PROP :handler-include "theory/arith/options_handlers.h" :include "theory/arith/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 arithHeuristicPivotRule --heuristic-pivot-rule=RULE ArithHeuristicPivotRule :handler CVC4::theory::arith::stringToArithHeuristicPivotRule :default MINIMUM :handler-include "theory/arith/options_handlers.h" :include "theory/arith/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 + use Linear Diophantine Equation solver (Griggio, JSAT 2012) +/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 + +endmodule |