#
# 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 stringToArithUnateLemmaMode :default ALL_PRESOLVE_LEMMAS :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 stringToArithPropagationMode :default BOTH_PROP :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 stringToErrorSelectionRule :default MINIMUM_AMOUNT :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 --enable-dio-solver/--disable-dio-solver bool :default true
 turns on 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


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

option sNormInferEq --snorm-infer-eq bool :default false
 infer equalities based on Shostak normalization

endmodule