#
# 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 arithErrorSelectionRule --error-selection-rule=RULE ErrorSelectionRule :handler CVC4::theory::arith::stringToErrorSelectionRule :default MINIMUM_AMOUNT :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
 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 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 fancyFinal --fancy-final bool :default false :read-write
 Tuning how final check works for really hard problems.

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 int :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.


endmodule