id     = "ARITH"
name   = "Arithmetic Theory"

[[option]]
  name       = "arithUnateLemmaMode"
  category   = "regular"
  long       = "unate-lemmas=MODE"
  type       = "ArithUnateLemmaMode"
  default    = "ALL"
  help       = "determines which lemmas to add before solving (default is 'all', see --unate-lemmas=help)"
  help_mode  = "Unate lemmas are generated before SAT search begins using the relationship of constant terms and polynomials."
[[option.mode.ALL]]
  name = "all"
  help = "A combination of inequalities and equalities."
[[option.mode.EQUALITY]]
  name = "eqs"
  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."
[[option.mode.INEQUALITY]]
  name = "ineqs"
  help  = "Outputs lemmas of the general form (<= p c) implies (<= p d) for c < d."
[[option.mode.NO]]
  name = "none"

[[option]]
  name       = "arithPropagationMode"
  category   = "regular"
  long       = "arith-prop=MODE"
  type       = "ArithPropagationMode"
  default    = "BOTH_PROP"
  help       = "turns on arithmetic propagation (default is 'old', see --arith-prop=help)"
  help_mode  = "This decides on kind of propagation arithmetic attempts to do during the search."
[[option.mode.NO_PROP]]
  name = "none"
[[option.mode.UNATE_PROP]]
  name = "unate"
  help = "Use constraints to do unate propagation."
[[option.mode.BOUND_INFERENCE_PROP]]
  name = "bi"
  help  = "(Bounds Inference) infers bounds on basic variables using the upper and lower bounds of the non-basic variables in the tableau."
[[option.mode.BOTH_PROP]]
  name = "both"
  help = "Use bounds inference and unate."



# 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]]
  name       = "arithHeuristicPivots"
  category   = "regular"
  long       = "heuristic-pivots=N"
  type       = "int64_t"
  default    = "0"
  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"


# 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.
[[option]]
  name       = "arithStandardCheckVarOrderPivots"
  category   = "expert"
  long       = "standard-effort-variable-order-pivots=N"
  type       = "int64_t"
  default    = "-1"
  help       = "limits the number of pivots in a single invocation of check() at a non-full effort level using Bland's pivot rule"

[[option]]
  name       = "arithErrorSelectionRule"
  category   = "regular"
  long       = "error-selection-rule=RULE"
  type       = "ErrorSelectionRule"
  default    = "MINIMUM_AMOUNT"
  help       = "change the pivot rule for the basic variable (default is 'min', see --pivot-rule help)"
  help_mode  = "This decides on the rule used by simplex during heuristic rounds for deciding the next basic variable to select."
[[option.mode.MINIMUM_AMOUNT]]
  name = "min"
  help = "The minimum abs() value of the variable's violation of its bound."
[[option.mode.VAR_ORDER]]
  name = "varord"
  help = "The variable order."
[[option.mode.MAXIMUM_AMOUNT]]
  name = "max"
  help = "The maximum violation the bound."
[[option.mode.SUM_METRIC]]
  name = "sum"

# The number of pivots before simplex rechecks every basic variable for a conflict
[[option]]
  name       = "arithSimplexCheckPeriod"
  category   = "regular"
  long       = "simplex-check-period=N"
  type       = "uint64_t"
  default    = "200"
  help       = "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]]
  name       = "arithPivotThreshold"
  category   = "regular"
  long       = "pivot-threshold=N"
  type       = "uint64_t"
  default    = "2"
  help       = "sets the number of pivots using --pivot-rule per basic variable per simplex instance before using variable order"

[[option]]
  name       = "arithPropagateMaxLength"
  category   = "regular"
  long       = "prop-row-length=N"
  type       = "uint64_t"
  default    = "16"
  help       = "sets the maximum row length to be used in propagation"

[[option]]
  name       = "arithDioSolver"
  category   = "regular"
  long       = "dio-solver"
  type       = "bool"
  default    = "true"
  help       = "turns on Linear Diophantine Equation solver (Griggio, JSAT 2012)"

# Whether to split (= x y) into (and (<= x y) (>= x y)) in
# arithmetic preprocessing.
[[option]]
  name       = "arithRewriteEq"
  category   = "regular"
  long       = "arith-rewrite-equalities"
  type       = "bool"
  default    = "false"
  help       = "turns on the preprocessing rewrite turning equalities into a conjunction of inequalities"

[[option]]
  name       = "arithMLTrick"
  category   = "regular"
  long       = "miplib-trick"
  type       = "bool"
  default    = "false"
  help       = "turns on the preprocessing step of attempting to infer bounds on miplib problems"

[[option]]
  name       = "arithMLTrickSubstitutions"
  category   = "regular"
  long       = "miplib-trick-subs=N"
  type       = "uint64_t"
  default    = "1"
  help       = "do substitution for miplib 'tmp' vars if defined in <= N eliminated vars"

[[option]]
  name       = "doCutAllBounded"
  category   = "regular"
  long       = "cut-all-bounded"
  type       = "bool"
  default    = "false"
  help       = "turns on the integer solving step of periodically cutting all integer variables that have both upper and lower bounds"

[[option]]
  name       = "maxCutsInContext"
  category   = "regular"
  long       = "maxCutsInContext=N"
  type       = "uint64_t"
  default    = "65535"
  help       = "maximum cuts in a given context before signalling a restart"

[[option]]
  name       = "revertArithModels"
  category   = "regular"
  long       = "revert-arith-models-on-unsat"
  type       = "bool"
  default    = "false"
  help       = "revert the arithmetic model to a known safe model on unsat if one is cached"

[[option]]
  name       = "havePenalties"
  category   = "regular"
  long       = "fc-penalties"
  type       = "bool"
  default    = "false"
  help       = "turns on degenerate pivot penalties"

[[option]]
  name       = "useFC"
  category   = "regular"
  long       = "use-fcsimplex"
  type       = "bool"
  default    = "false"
  help       = "use focusing and converging simplex (FMCAD 2013 submission)"

[[option]]
  name       = "useSOI"
  category   = "regular"
  long       = "use-soi"
  type       = "bool"
  default    = "false"
  help       = "use sum of infeasibility simplex (FMCAD 2013 submission)"

[[option]]
  name       = "restrictedPivots"
  category   = "regular"
  long       = "restrict-pivots"
  type       = "bool"
  default    = "true"
  help       = "have a pivot cap for simplex at effort levels below fullEffort"

[[option]]
  name       = "collectPivots"
  category   = "regular"
  long       = "collect-pivot-stats"
  type       = "bool"
  default    = "false"
  help       = "collect the pivot history"

[[option]]
  name       = "useApprox"
  category   = "regular"
  long       = "use-approx"
  type       = "bool"
  default    = "false"
  help       = "attempt to use an approximate solver"

[[option]]
  name       = "maxApproxDepth"
  category   = "regular"
  long       = "approx-branch-depth=N"
  type       = "int64_t"
  default    = "200"
  help       = "maximum branch depth the approximate solver is allowed to take"

[[option]]
  name       = "exportDioDecompositions"
  category   = "regular"
  long       = "dio-decomps"
  type       = "bool"
  default    = "false"
  help       = "let skolem variables for integer divisibility constraints leak from the dio solver"

[[option]]
  name       = "newProp"
  category   = "regular"
  long       = "new-prop"
  type       = "bool"
  default    = "true"
  help       = "use the new row propagation system"

[[option]]
  name       = "arithPropAsLemmaLength"
  category   = "regular"
  long       = "arith-prop-clauses=N"
  type       = "uint64_t"
  default    = "8"
  help       = "rows shorter than this are propagated as clauses"

[[option]]
  name       = "soiQuickExplain"
  category   = "regular"
  long       = "soi-qe"
  type       = "bool"
  default    = "false"
  help       = "use quick explain to minimize the sum of infeasibility conflicts"

[[option]]
  name       = "trySolveIntStandardEffort"
  category   = "regular"
  long       = "se-solve-int"
  type       = "bool"
  default    = "false"
  help       = "attempt to use the approximate solve integer method on standard effort"

[[option]]
  name       = "replayFailureLemma"
  category   = "regular"
  long       = "lemmas-on-replay-failure"
  type       = "bool"
  default    = "false"
  help       = "attempt to use external lemmas if approximate solve integer failed"

[[option]]
  name       = "dioSolverTurns"
  category   = "regular"
  long       = "dio-turns=N"
  type       = "int64_t"
  default    = "10"
  help       = "turns in a row dio solver cutting gets"

[[option]]
  name       = "rrTurns"
  category   = "regular"
  long       = "rr-turns=N"
  type       = "int64_t"
  default    = "3"
  help       = "round robin turn"

[[option]]
  name       = "replayEarlyCloseDepths"
  category   = "regular"
  long       = "replay-early-close-depth=N"
  type       = "int64_t"
  default    = "1"
  help       = "multiples of the depths to try to close the approx log eagerly"

[[option]]
  name       = "replayNumericFailurePenalty"
  category   = "regular"
  long       = "replay-num-err-penalty=N"
  type       = "int64_t"
  default    = "4194304"
  help       = "number of solve integer attempts to skips after a numeric failure"

[[option]]
  name       = "replayRejectCutSize"
  category   = "regular"
  long       = "replay-reject-cut=N"
  type       = "uint64_t"
  default    = "25500"
  help       = "maximum complexity of any coefficient while replaying cuts"

[[option]]
  name       = "lemmaRejectCutSize"
  category   = "regular"
  long       = "replay-lemma-reject-cut=N"
  type       = "uint64_t"
  default    = "25500"
  help       = "maximum complexity of any coefficient while outputting replaying cut lemmas"

[[option]]
  name       = "ppAssertMaxSubSize"
  category   = "regular"
  long       = "pp-assert-max-sub-size=N"
  type       = "uint64_t"
  default    = "2"
  help       = "threshold for substituting an equality in ppAssert"

[[option]]
  name       = "arithNoPartialFun"
  category   = "regular"
  long       = "arith-no-partial-fun"
  type       = "bool"
  default    = "false"
  help       = "do not use partial function semantics for arithmetic (not SMT LIB compliant)"

[[option]]
  name       = "pbRewrites"
  category   = "regular"
  long       = "pb-rewrites"
  type       = "bool"
  default    = "false"
  help       = "apply pseudo boolean rewrites"

[[option]]
  name       = "nlExt"
  category   = "regular"
  long       = "nl-ext=MODE"
  type       = "NlExtMode"
  default    = "FULL"
  help       = "incremental linearization approach to non-linear"
  help_mode  = "Modes for the non-linear linearization"
[[option.mode.NONE]]
  name = "none"
  help = "Disable linearization approach"
[[option.mode.LIGHT]]
  name = "light"
  help = "Only use a few light-weight lemma schemes"
[[option.mode.FULL]]
  name = "full"
  help = "Use all lemma schemes"

[[option]]
  name       = "nlRlvAssertBounds"
  category   = "regular"
  long       = "nl-rlv-assert-bounds"
  type       = "bool"
  default    = "false"
  help       = "use bound inference utility to prune when an assertion is entailed by another"

[[option]]
  name       = "nlExtResBound"
  category   = "regular"
  long       = "nl-ext-rbound"
  type       = "bool"
  default    = "false"
  help       = "use resolution-style inference for inferring new bounds in non-linear incremental linearization solver"

[[option]]
  name       = "nlExtFactor"
  category   = "regular"
  long       = "nl-ext-factor"
  type       = "bool"
  default    = "true"
  help       = "use factoring inference in non-linear incremental linearization solver"

[[option]]
  name       = "nlExtTangentPlanes"
  category   = "regular"
  long       = "nl-ext-tplanes"
  type       = "bool"
  default    = "false"
  help       = "use non-terminating tangent plane strategy for non-linear incremental linearization solver"

[[option]]
  name       = "nlExtTangentPlanesInterleave"
  category   = "regular"
  long       = "nl-ext-tplanes-interleave"
  type       = "bool"
  default    = "false"
  help       = "interleave tangent plane strategy for non-linear incremental linearization solver"

[[option]]
  name       = "nlExtTfTangentPlanes"
  category   = "regular"
  long       = "nl-ext-tf-tplanes"
  type       = "bool"
  default    = "true"
  help       = "use non-terminating tangent plane strategy for transcendental functions for non-linear incremental linearization solver"

[[option]]
  name       = "nlExtEntailConflicts"
  category   = "regular"
  long       = "nl-ext-ent-conf"
  type       = "bool"
  default    = "false"
  help       = "check for entailed conflicts in non-linear solver"

[[option]]
  name       = "nlExtRewrites"
  category   = "regular"
  long       = "nl-ext-rewrite"
  type       = "bool"
  default    = "true"
  help       = "do context-dependent simplification based on rewrites in non-linear solver"

[[option]]
  name       = "nlExtPurify"
  category   = "regular"
  long       = "nl-ext-purify"
  type       = "bool"
  default    = "false"
  help       = "purify non-linear terms at preprocess"

[[option]]
  name       = "nlExtSplitZero"
  category   = "regular"
  long       = "nl-ext-split-zero"
  type       = "bool"
  default    = "false"
  help       = "initial splits on zero for all variables"

[[option]]
  name       = "nlExtTfTaylorDegree"
  category   = "regular"
  long       = "nl-ext-tf-taylor-deg=N"
  type       = "int64_t"
  default    = "4"
  help       = "initial degree of polynomials for Taylor approximation"

[[option]]
  name       = "nlExtIncPrecision"
  category   = "regular"
  long       = "nl-ext-inc-prec"
  type       = "bool"
  default    = "true"
  help       = "whether to increment the precision for irrational function constraints"

[[option]]
  name       = "nlRlvMode"
  category   = "regular"
  long       = "nl-rlv=MODE"
  type       = "NlRlvMode"
  default    = "NONE"
  help       = "choose mode for using relevance of assertions in non-linear arithmetic"
  help_mode  = "Modes for using relevance of assertions in non-linear arithmetic."
[[option.mode.NONE]]
  name = "none"
  help = "Do not use relevance."
[[option.mode.INTERLEAVE]]
  name = "interleave"
  help = "Alternate rounds using relevance."
[[option.mode.ALWAYS]]
  name = "always"
  help = "Always use relevance."
  
[[option]]
  name       = "brabTest"
  category   = "regular"
  long       = "arith-brab"
  type       = "bool"
  default    = "true"
  help       = "whether to use simple rounding, similar to a unit-cube test, for integers"

[[option]]
  name       = "nlCad"
  category   = "regular"
  long       = "nl-cad"
  type       = "bool"
  default    = "false"
  help       = "whether to use the cylindrical algebraic coverings solver for non-linear arithmetic"

[[option]]
  name       = "nlCadPrune"
  category   = "regular"
  long       = "nl-cad-prune"
  type       = "bool"
  default    = "false"
  help       = "whether to prune intervals more agressively"

[[option]]
  name       = "nlCadLinearModel"
  category   = "regular"
  long       = "nl-cad-linear-model=MODE"
  type       = "NlCadLinearModelMode"
  default    = "NONE"
  help       = "whether to use the linear model as initial guess for the cylindrical algebraic coverings solver"
  help_mode  = "Modes for the usage of the linear model in non-linear arithmetic."
[[option.mode.NONE]]
  name       = "none"
  help       = "Do not use linear model to seed nonlinear model"
[[option.mode.INITIAL]]
  name       = "initial"
  help       = "Use linear model to seed nonlinear model initially, discard it when it does not work"
[[option.mode.PERSISTENT]]
  name       = "persistent"
  help       = "Use linear model to seed nonlinear model whenever possible"

[[option]]
  name       = "nlCadProjection"
  category   = "expert"
  long       = "nl-cad-proj=MODE"
  type       = "NlCadProjectionMode"
  default    = "MCCALLUM"
  help       = "choose the CAD projection operator"
  help_mode  = "Modes for the CAD projection operator in non-linear arithmetic."
[[option.mode.MCCALLUM]]
  name = "mccallum"
  help = "McCallum's projection operator."
[[option.mode.LAZARD]]
  name = "lazard"
  help = "Lazard's projection operator."
[[option.mode.LAZARDMOD]]
  name = "lazard-mod"
  help = "A modification of Lazard's projection operator."

[[option]]
  name       = "nlCadLifting"
  category   = "expert"
  long       = "nl-cad-lift=MODE"
  type       = "NlCadLiftingMode"
  default    = "REGULAR"
  help       = "choose the CAD lifting mode"
  help_mode  = "Modes for the CAD lifting in non-linear arithmetic."
[[option.mode.REGULAR]]
  name = "regular"
  help = "Regular lifting."
[[option.mode.LAZARD]]
  name = "lazard"
  help = "Lazard's lifting scheme."

[[option]]
  name       = "nlICP"
  category   = "regular"
  long       = "nl-icp"
  type       = "bool"
  default    = "false"
  help       = "whether to use ICP-style propagations for non-linear arithmetic"

[[option]]
  name       = "arithEqSolver"
  category   = "regular"
  long       = "arith-eq-solver"
  type       = "bool"
  default    = "false"
  help       = "whether to use the equality solver in the theory of arithmetic"

[[option]]
  name       = "arithCongMan"
  category   = "regular"
  long       = "arith-cong-man"
  type       = "bool"
  default    = "true"
  help       = "(experimental) whether to use the congruence manager when the equality solver is enabled"