/******************************************************************************

 * Top contributors (to current version):

 *   Mathias Preiner, Aina Niemetz

 *

 * This file is part of the cvc5 project.

 *

 * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS

 * in the top-level source directory and their institutional affiliations.

 * All rights reserved.  See the file COPYING in the top-level source

 * directory for licensing information.

 * ****************************************************************************

 *

 * Contains code for handling command-line options.

 *

 * For each <module>_options.toml configuration file, mkoptions.py

 * expands this template and generates a <module>_options.h file.

 */

#include "cvc5_private.h"

#ifndef CVC5__OPTIONS__ARITH_H

#define CVC5__OPTIONS__ARITH_H

#include "options/options.h"

// clang-format off

// clang-format on

namespace cvc5 {

namespace options {

// clang-format off

enum class ArithPropagationMode

{

  BOTH_PROP,

  NO_PROP,

  BOUND_INFERENCE_PROP,

  UNATE_PROP

};

static constexpr size_t ArithPropagationMode__numValues = 4;

std::ostream& operator<<(std::ostream& os, ArithPropagationMode mode);

ArithPropagationMode stringToArithPropagationMode(const std::string& optarg);

enum class ErrorSelectionRule

{

  MINIMUM_AMOUNT,

  SUM_METRIC,

  VAR_ORDER,

  MAXIMUM_AMOUNT

};

static constexpr size_t ErrorSelectionRule__numValues = 4;

std::ostream& operator<<(std::ostream& os, ErrorSelectionRule mode);

ErrorSelectionRule stringToErrorSelectionRule(const std::string& optarg);

enum class NlCadLiftingMode

{

  REGULAR,

  LAZARD

};

static constexpr size_t NlCadLiftingMode__numValues = 2;

std::ostream& operator<<(std::ostream& os, NlCadLiftingMode mode);

NlCadLiftingMode stringToNlCadLiftingMode(const std::string& optarg);

enum class NlCadProjectionMode

{

  LAZARD,

  LAZARDMOD,

  MCCALLUM

};

static constexpr size_t NlCadProjectionMode__numValues = 3;

std::ostream& operator<<(std::ostream& os, NlCadProjectionMode mode);

NlCadProjectionMode stringToNlCadProjectionMode(const std::string& optarg);

enum class NlExtMode

{

  LIGHT,

  FULL,

  NONE

};

static constexpr size_t NlExtMode__numValues = 3;

std::ostream& operator<<(std::ostream& os, NlExtMode mode);

NlExtMode stringToNlExtMode(const std::string& optarg);

enum class NlRlvMode

{

  ALWAYS,

  INTERLEAVE,

  NONE

};

static constexpr size_t NlRlvMode__numValues = 3;

std::ostream& operator<<(std::ostream& os, NlRlvMode mode);

NlRlvMode stringToNlRlvMode(const std::string& optarg);

enum class ArithUnateLemmaMode

{

  ALL,

  NO,

  INEQUALITY,

  EQUALITY

};

static constexpr size_t ArithUnateLemmaMode__numValues = 4;

std::ostream& operator<<(std::ostream& os, ArithUnateLemmaMode mode);

ArithUnateLemmaMode stringToArithUnateLemmaMode(const std::string& optarg);

// clang-format on

#if defined(CVC5_MUZZLED) || defined(CVC5_COMPETITION_MODE)

#  define DO_SEMANTIC_CHECKS_BY_DEFAULT false

#else /* CVC5_MUZZLED || CVC5_COMPETITION_MODE */

#  define DO_SEMANTIC_CHECKS_BY_DEFAULT true

#endif /* CVC5_MUZZLED || CVC5_COMPETITION_MODE */

{

// clang-format off

  int16_t maxApproxDepth = 200;

  bool maxApproxDepthWasSetByUser = false;

  bool brabTest = true;

  bool brabTestWasSetByUser = false;

  bool arithCongMan = true;

  bool arithCongManWasSetByUser = false;

  bool arithEqSolver = false;

  bool arithEqSolverWasSetByUser = false;

  bool arithNoPartialFun = false;

  bool arithNoPartialFunWasSetByUser = false;

  uint16_t arithPropAsLemmaLength = 8;

  bool arithPropAsLemmaLengthWasSetByUser = false;

  ArithPropagationMode arithPropagationMode = ArithPropagationMode::BOTH_PROP;

  bool arithPropagationModeWasSetByUser = false;

  bool arithRewriteEq = false;

  bool arithRewriteEqWasSetByUser = false;

  bool collectPivots = false;

  bool collectPivotsWasSetByUser = false;

  bool doCutAllBounded = false;

  bool doCutAllBoundedWasSetByUser = false;

  bool exportDioDecompositions = false;

  bool exportDioDecompositionsWasSetByUser = false;

  bool dioRepeat = false;

  bool dioRepeatWasSetByUser = false;

  bool arithDioSolver = true;

  bool arithDioSolverWasSetByUser = false;

  int dioSolverTurns = 10;

  bool dioSolverTurnsWasSetByUser = false;

  ErrorSelectionRule arithErrorSelectionRule = ErrorSelectionRule::MINIMUM_AMOUNT;

  bool arithErrorSelectionRuleWasSetByUser = false;

  bool havePenalties = false;

  bool havePenaltiesWasSetByUser = false;

  int16_t arithHeuristicPivots = 0;

  bool arithHeuristicPivotsWasSetByUser = false;

  bool replayFailureLemma = false;

  bool replayFailureLemmaWasSetByUser = false;

  unsigned maxCutsInContext = 65535;

  bool maxCutsInContextWasSetByUser = false;

  bool arithMLTrick = false;

  bool arithMLTrickWasSetByUser = false;

  unsigned arithMLTrickSubstitutions = 1;

  bool arithMLTrickSubstitutionsWasSetByUser = false;

  bool newProp = true;

  bool newPropWasSetByUser = false;

  bool nlCad = false;

  bool nlCadWasSetByUser = false;

  bool nlCadUseInitial = false;

  bool nlCadUseInitialWasSetByUser = false;

  NlCadLiftingMode nlCadLifting = NlCadLiftingMode::REGULAR;

  bool nlCadLiftingWasSetByUser = false;

  NlCadProjectionMode nlCadProjection = NlCadProjectionMode::MCCALLUM;

  bool nlCadProjectionWasSetByUser = false;

  bool nlExtEntailConflicts = false;

  bool nlExtEntailConflictsWasSetByUser = false;

  bool nlExtFactor = true;

  bool nlExtFactorWasSetByUser = false;

  bool nlExtIncPrecision = true;

  bool nlExtIncPrecisionWasSetByUser = false;

  bool nlExtPurify = false;

  bool nlExtPurifyWasSetByUser = false;

  bool nlExtResBound = false;

  bool nlExtResBoundWasSetByUser = false;

  bool nlExtRewrites = true;

  bool nlExtRewritesWasSetByUser = false;

  bool nlExtSplitZero = false;

  bool nlExtSplitZeroWasSetByUser = false;

  int16_t nlExtTfTaylorDegree = 4;

  bool nlExtTfTaylorDegreeWasSetByUser = false;

  bool nlExtTfTangentPlanes = true;

  bool nlExtTfTangentPlanesWasSetByUser = false;

  bool nlExtTangentPlanes = false;

  bool nlExtTangentPlanesWasSetByUser = false;

  bool nlExtTangentPlanesInterleave = false;

  bool nlExtTangentPlanesInterleaveWasSetByUser = false;

  NlExtMode nlExt = NlExtMode::FULL;

  bool nlExtWasSetByUser = false;

  bool nlICP = false;

  bool nlICPWasSetByUser = false;

  NlRlvMode nlRlvMode = NlRlvMode::NONE;

  bool nlRlvModeWasSetByUser = false;

  bool pbRewrites = false;

  bool pbRewritesWasSetByUser = false;

  uint16_t arithPivotThreshold = 2;

  bool arithPivotThresholdWasSetByUser = false;

  unsigned ppAssertMaxSubSize = 2;

  bool ppAssertMaxSubSizeWasSetByUser = false;

  uint16_t arithPropagateMaxLength = 16;

  bool arithPropagateMaxLengthWasSetByUser = false;

  int replayEarlyCloseDepths = 1;

  bool replayEarlyCloseDepthsWasSetByUser = false;

  int replayFailurePenalty = 100;

  bool replayFailurePenaltyWasSetByUser = false;

  unsigned lemmaRejectCutSize = 25500;

  bool lemmaRejectCutSizeWasSetByUser = false;

  int replayNumericFailurePenalty = 4194304;

  bool replayNumericFailurePenaltyWasSetByUser = false;

  unsigned replayRejectCutSize = 25500;

  bool replayRejectCutSizeWasSetByUser = false;

  int soiApproxMajorFailurePen = 50;

  bool soiApproxMajorFailurePenWasSetByUser = false;

  double soiApproxMajorFailure = .01;

  bool soiApproxMajorFailureWasSetByUser = false;

  int soiApproxMinorFailurePen = 10;

  bool soiApproxMinorFailurePenWasSetByUser = false;

  double soiApproxMinorFailure = .0001;

  bool soiApproxMinorFailureWasSetByUser = false;

  bool restrictedPivots = true;

  bool restrictedPivotsWasSetByUser = false;

  bool revertArithModels = false;

  bool revertArithModelsWasSetByUser = false;

  int rrTurns = 3;

  bool rrTurnsWasSetByUser = false;

  bool trySolveIntStandardEffort = false;

  bool trySolveIntStandardEffortWasSetByUser = false;

  uint16_t arithSimplexCheckPeriod = 200;

  bool arithSimplexCheckPeriodWasSetByUser = false;

  bool soiQuickExplain = false;

  bool soiQuickExplainWasSetByUser = false;

  int16_t arithStandardCheckVarOrderPivots = -1;

  bool arithStandardCheckVarOrderPivotsWasSetByUser = false;

  ArithUnateLemmaMode arithUnateLemmaMode = ArithUnateLemmaMode::ALL;

  bool arithUnateLemmaModeWasSetByUser = false;

  bool useApprox = false;

  bool useApproxWasSetByUser = false;

  bool useFC = false;

  bool useFCWasSetByUser = false;

  bool useSOI = false;

  bool useSOIWasSetByUser = false;

// clang-format on

};

#undef DO_SEMANTIC_CHECKS_BY_DEFAULT

// clang-format off

extern struct maxApproxDepth__option_t

{

  typedef int16_t type;

  type operator()() const;

} thread_local maxApproxDepth;

extern struct brabTest__option_t

{

  typedef bool type;

  type operator()() const;

} thread_local brabTest;

extern struct arithCongMan__option_t

{

  typedef bool type;

  type operator()() const;

} thread_local arithCongMan;

extern struct arithEqSolver__option_t

{

  typedef bool type;

  type operator()() const;

} thread_local arithEqSolver;

extern struct arithNoPartialFun__option_t

{

  typedef bool type;

  type operator()() const;

} thread_local arithNoPartialFun;

extern struct arithPropAsLemmaLength__option_t

{

  typedef uint16_t type;

  type operator()() const;

} thread_local arithPropAsLemmaLength;

extern struct arithPropagationMode__option_t

{

  typedef ArithPropagationMode type;

  type operator()() const;

} thread_local arithPropagationMode;

extern struct arithRewriteEq__option_t

{

  typedef bool type;

  type operator()() const;

} thread_local arithRewriteEq;

extern struct collectPivots__option_t

{

  typedef bool type;

  type operator()() const;

} thread_local collectPivots;

extern struct doCutAllBounded__option_t

{

  typedef bool type;

  type operator()() const;

} thread_local doCutAllBounded;

extern struct exportDioDecompositions__option_t

{

  typedef bool type;

  type operator()() const;

} thread_local exportDioDecompositions;

extern struct dioRepeat__option_t

{

  typedef bool type;

  type operator()() const;

} thread_local dioRepeat;

extern struct arithDioSolver__option_t

{

  typedef bool type;

  type operator()() const;

} thread_local arithDioSolver;

extern struct dioSolverTurns__option_t

{

  typedef int type;

  type operator()() const;

} thread_local dioSolverTurns;

extern struct arithErrorSelectionRule__option_t

{

  typedef ErrorSelectionRule type;

  type operator()() const;

} thread_local arithErrorSelectionRule;

extern struct havePenalties__option_t

{

  typedef bool type;

  type operator()() const;

} thread_local havePenalties;

extern struct arithHeuristicPivots__option_t

{

  typedef int16_t type;

  type operator()() const;

} thread_local arithHeuristicPivots;

extern struct replayFailureLemma__option_t

{

  typedef bool type;

  type operator()() const;

} thread_local replayFailureLemma;

extern struct maxCutsInContext__option_t

{

  typedef unsigned type;

  type operator()() const;

} thread_local maxCutsInContext;

extern struct arithMLTrick__option_t

{

  typedef bool type;

  type operator()() const;

} thread_local arithMLTrick;

extern struct arithMLTrickSubstitutions__option_t

{

  typedef unsigned type;

  type operator()() const;

} thread_local arithMLTrickSubstitutions;

extern struct newProp__option_t

{

  typedef bool type;

  type operator()() const;

} thread_local newProp;

extern struct nlCad__option_t

{

  typedef bool type;

  type operator()() const;

} thread_local nlCad;

extern struct nlCadUseInitial__option_t

{

  typedef bool type;

  type operator()() const;

} thread_local nlCadUseInitial;

extern struct nlCadLifting__option_t

{

  typedef NlCadLiftingMode type;

  type operator()() const;

} thread_local nlCadLifting;

extern struct nlCadProjection__option_t

{

  typedef NlCadProjectionMode type;

  type operator()() const;

} thread_local nlCadProjection;

extern struct nlExtEntailConflicts__option_t

{

  typedef bool type;

  type operator()() const;

} thread_local nlExtEntailConflicts;

extern struct nlExtFactor__option_t

{

  typedef bool type;

  type operator()() const;

} thread_local nlExtFactor;

extern struct nlExtIncPrecision__option_t

{

  typedef bool type;

  type operator()() const;

} thread_local nlExtIncPrecision;

extern struct nlExtPurify__option_t

{

  typedef bool type;

  type operator()() const;

} thread_local nlExtPurify;

extern struct nlExtResBound__option_t

{

  typedef bool type;

  type operator()() const;

} thread_local nlExtResBound;

extern struct nlExtRewrites__option_t

{

  typedef bool type;

  type operator()() const;

} thread_local nlExtRewrites;

extern struct nlExtSplitZero__option_t

{

  typedef bool type;

  type operator()() const;

} thread_local nlExtSplitZero;

extern struct nlExtTfTaylorDegree__option_t

{

  typedef int16_t type;

  type operator()() const;

} thread_local nlExtTfTaylorDegree;

extern struct nlExtTfTangentPlanes__option_t

{

  typedef bool type;

  type operator()() const;

} thread_local nlExtTfTangentPlanes;

extern struct nlExtTangentPlanes__option_t

{

  typedef bool type;

  type operator()() const;

} thread_local nlExtTangentPlanes;

extern struct nlExtTangentPlanesInterleave__option_t

{

  typedef bool type;

  type operator()() const;

} thread_local nlExtTangentPlanesInterleave;

extern struct nlExt__option_t

{

  typedef NlExtMode type;

  type operator()() const;

} thread_local nlExt;

extern struct nlICP__option_t

{

  typedef bool type;

  type operator()() const;

} thread_local nlICP;

extern struct nlRlvMode__option_t

{

  typedef NlRlvMode type;

  type operator()() const;

} thread_local nlRlvMode;

extern struct pbRewrites__option_t

{

  typedef bool type;

  type operator()() const;

} thread_local pbRewrites;

extern struct arithPivotThreshold__option_t

{

  typedef uint16_t type;

  type operator()() const;

} thread_local arithPivotThreshold;

extern struct ppAssertMaxSubSize__option_t

{

  typedef unsigned type;

  type operator()() const;

} thread_local ppAssertMaxSubSize;

extern struct arithPropagateMaxLength__option_t

{

  typedef uint16_t type;

  type operator()() const;

} thread_local arithPropagateMaxLength;

extern struct replayEarlyCloseDepths__option_t

{

  typedef int type;

  type operator()() const;

} thread_local replayEarlyCloseDepths;

extern struct replayFailurePenalty__option_t

{

  typedef int type;

  type operator()() const;

} thread_local replayFailurePenalty;

extern struct lemmaRejectCutSize__option_t

{

  typedef unsigned type;

  type operator()() const;

} thread_local lemmaRejectCutSize;

extern struct replayNumericFailurePenalty__option_t

{

  typedef int type;

  type operator()() const;

} thread_local replayNumericFailurePenalty;

extern struct replayRejectCutSize__option_t

{

  typedef unsigned type;

  type operator()() const;

} thread_local replayRejectCutSize;

extern struct soiApproxMajorFailurePen__option_t

{

  typedef int type;

  type operator()() const;

} thread_local soiApproxMajorFailurePen;

extern struct soiApproxMajorFailure__option_t

{

  typedef double type;

  type operator()() const;

} thread_local soiApproxMajorFailure;

extern struct soiApproxMinorFailurePen__option_t

{

  typedef int type;

  type operator()() const;

} thread_local soiApproxMinorFailurePen;

extern struct soiApproxMinorFailure__option_t

{

  typedef double type;

  type operator()() const;

} thread_local soiApproxMinorFailure;

extern struct restrictedPivots__option_t

{

  typedef bool type;

  type operator()() const;

} thread_local restrictedPivots;

extern struct revertArithModels__option_t

{

  typedef bool type;

  type operator()() const;

} thread_local revertArithModels;

extern struct rrTurns__option_t

{

  typedef int type;

  type operator()() const;

} thread_local rrTurns;

extern struct trySolveIntStandardEffort__option_t

{

  typedef bool type;

  type operator()() const;

} thread_local trySolveIntStandardEffort;

extern struct arithSimplexCheckPeriod__option_t

{

  typedef uint16_t type;

  type operator()() const;

} thread_local arithSimplexCheckPeriod;

extern struct soiQuickExplain__option_t

{

  typedef bool type;

  type operator()() const;

} thread_local soiQuickExplain;

extern struct arithStandardCheckVarOrderPivots__option_t

{

  typedef int16_t type;

  type operator()() const;

} thread_local arithStandardCheckVarOrderPivots;

extern struct arithUnateLemmaMode__option_t

{

  typedef ArithUnateLemmaMode type;

  type operator()() const;

} thread_local arithUnateLemmaMode;

extern struct useApprox__option_t

{

  typedef bool type;

  type operator()() const;

} thread_local useApprox;

extern struct useFC__option_t

{

  typedef bool type;

  type operator()() const;

} thread_local useFC;

extern struct useSOI__option_t

{

  typedef bool type;

  type operator()() const;

} thread_local useSOI;

// clang-format on

namespace arith

{

// clang-format off

static constexpr const char* maxApproxDepth__name = "approx-branch-depth";

static constexpr const char* brabTest__name = "arith-brab";

static constexpr const char* arithCongMan__name = "arith-cong-man";

static constexpr const char* arithEqSolver__name = "arith-eq-solver";

static constexpr const char* arithNoPartialFun__name = "arith-no-partial-fun";

static constexpr const char* arithPropAsLemmaLength__name = "arith-prop-clauses";

static constexpr const char* arithPropagationMode__name = "arith-prop";

static constexpr const char* arithRewriteEq__name = "arith-rewrite-equalities";

static constexpr const char* collectPivots__name = "collect-pivot-stats";

static constexpr const char* doCutAllBounded__name = "cut-all-bounded";

static constexpr const char* exportDioDecompositions__name = "dio-decomps";

static constexpr const char* dioRepeat__name = "dio-repeat";

static constexpr const char* arithDioSolver__name = "dio-solver";

static constexpr const char* dioSolverTurns__name = "dio-turns";

static constexpr const char* arithErrorSelectionRule__name = "error-selection-rule";

static constexpr const char* havePenalties__name = "fc-penalties";

static constexpr const char* arithHeuristicPivots__name = "heuristic-pivots";

static constexpr const char* replayFailureLemma__name = "lemmas-on-replay-failure";

static constexpr const char* maxCutsInContext__name = "maxCutsInContext";

static constexpr const char* arithMLTrick__name = "miplib-trick";

static constexpr const char* arithMLTrickSubstitutions__name = "miplib-trick-subs";

static constexpr const char* newProp__name = "new-prop";

static constexpr const char* nlCad__name = "nl-cad";

static constexpr const char* nlCadUseInitial__name = "nl-cad-initial";

static constexpr const char* nlCadLifting__name = "nl-cad-lift";

static constexpr const char* nlCadProjection__name = "nl-cad-proj";

static constexpr const char* nlExtEntailConflicts__name = "nl-ext-ent-conf";

static constexpr const char* nlExtFactor__name = "nl-ext-factor";

static constexpr const char* nlExtIncPrecision__name = "nl-ext-inc-prec";

static constexpr const char* nlExtPurify__name = "nl-ext-purify";

static constexpr const char* nlExtResBound__name = "nl-ext-rbound";

static constexpr const char* nlExtRewrites__name = "nl-ext-rewrite";

static constexpr const char* nlExtSplitZero__name = "nl-ext-split-zero";

static constexpr const char* nlExtTfTaylorDegree__name = "nl-ext-tf-taylor-deg";

static constexpr const char* nlExtTfTangentPlanes__name = "nl-ext-tf-tplanes";

static constexpr const char* nlExtTangentPlanes__name = "nl-ext-tplanes";

static constexpr const char* nlExtTangentPlanesInterleave__name = "nl-ext-tplanes-interleave";

static constexpr const char* nlExt__name = "nl-ext";

static constexpr const char* nlICP__name = "nl-icp";

static constexpr const char* nlRlvMode__name = "nl-rlv";

static constexpr const char* pbRewrites__name = "pb-rewrites";

static constexpr const char* arithPivotThreshold__name = "pivot-threshold";

static constexpr const char* ppAssertMaxSubSize__name = "pp-assert-max-sub-size";

static constexpr const char* arithPropagateMaxLength__name = "prop-row-length";

static constexpr const char* replayEarlyCloseDepths__name = "replay-early-close-depth";

static constexpr const char* replayFailurePenalty__name = "replay-failure-penalty";

static constexpr const char* lemmaRejectCutSize__name = "replay-lemma-reject-cut";

static constexpr const char* replayNumericFailurePenalty__name = "replay-num-err-penalty";

static constexpr const char* replayRejectCutSize__name = "replay-reject-cut";

static constexpr const char* soiApproxMajorFailurePen__name = "replay-soi-major-threshold-pen";

static constexpr const char* soiApproxMajorFailure__name = "replay-soi-major-threshold";

static constexpr const char* soiApproxMinorFailurePen__name = "replay-soi-minor-threshold-pen";

static constexpr const char* soiApproxMinorFailure__name = "replay-soi-minor-threshold";

static constexpr const char* restrictedPivots__name = "restrict-pivots";

static constexpr const char* revertArithModels__name = "revert-arith-models-on-unsat";

static constexpr const char* rrTurns__name = "rr-turns";

static constexpr const char* trySolveIntStandardEffort__name = "se-solve-int";

static constexpr const char* arithSimplexCheckPeriod__name = "simplex-check-period";

static constexpr const char* soiQuickExplain__name = "soi-qe";

static constexpr const char* arithStandardCheckVarOrderPivots__name = "standard-effort-variable-order-pivots";

static constexpr const char* arithUnateLemmaMode__name = "unate-lemmas";

static constexpr const char* useApprox__name = "use-approx";

static constexpr const char* useFC__name = "use-fcsimplex";

static constexpr const char* useSOI__name = "use-soi";

// clang-format on

}

}  // namespace options

// clang-format off

// clang-format on

namespace options {

// clang-format off

inline bool dioRepeat__option_t::operator()() const

{ return Options::current().arith.dioRepeat; }

inline int replayFailurePenalty__option_t::operator()() const

{ return Options::current().arith.replayFailurePenalty; }

inline int soiApproxMajorFailurePen__option_t::operator()() const

{ return Options::current().arith.soiApproxMajorFailurePen; }

inline double soiApproxMajorFailure__option_t::operator()() const

{ return Options::current().arith.soiApproxMajorFailure; }

inline int soiApproxMinorFailurePen__option_t::operator()() const

{ return Options::current().arith.soiApproxMinorFailurePen; }

inline double soiApproxMinorFailure__option_t::operator()() const

{ return Options::current().arith.soiApproxMinorFailure; }

// clang-format on

namespace arith

{

// clang-format off

void setDefaultMaxApproxDepth(Options& opts, int16_t value);

void setDefaultBrabTest(Options& opts, bool value);

void setDefaultArithCongMan(Options& opts, bool value);

void setDefaultArithEqSolver(Options& opts, bool value);

void setDefaultArithNoPartialFun(Options& opts, bool value);

void setDefaultArithPropAsLemmaLength(Options& opts, uint16_t value);

void setDefaultArithPropagationMode(Options& opts, ArithPropagationMode value);

void setDefaultArithRewriteEq(Options& opts, bool value);

void setDefaultCollectPivots(Options& opts, bool value);

void setDefaultDoCutAllBounded(Options& opts, bool value);

void setDefaultExportDioDecompositions(Options& opts, bool value);

void setDefaultDioRepeat(Options& opts, bool value);

void setDefaultArithDioSolver(Options& opts, bool value);

void setDefaultDioSolverTurns(Options& opts, int value);

void setDefaultArithErrorSelectionRule(Options& opts, ErrorSelectionRule value);

void setDefaultHavePenalties(Options& opts, bool value);

void setDefaultArithHeuristicPivots(Options& opts, int16_t value);

void setDefaultReplayFailureLemma(Options& opts, bool value);

void setDefaultMaxCutsInContext(Options& opts, unsigned value);

void setDefaultArithMLTrick(Options& opts, bool value);

void setDefaultArithMLTrickSubstitutions(Options& opts, unsigned value);

void setDefaultNewProp(Options& opts, bool value);

void setDefaultNlCad(Options& opts, bool value);

void setDefaultNlCadUseInitial(Options& opts, bool value);

void setDefaultNlCadLifting(Options& opts, NlCadLiftingMode value);

void setDefaultNlCadProjection(Options& opts, NlCadProjectionMode value);

void setDefaultNlExtEntailConflicts(Options& opts, bool value);

void setDefaultNlExtFactor(Options& opts, bool value);

void setDefaultNlExtIncPrecision(Options& opts, bool value);

void setDefaultNlExtPurify(Options& opts, bool value);

void setDefaultNlExtResBound(Options& opts, bool value);

void setDefaultNlExtRewrites(Options& opts, bool value);

void setDefaultNlExtSplitZero(Options& opts, bool value);

void setDefaultNlExtTfTaylorDegree(Options& opts, int16_t value);

void setDefaultNlExtTfTangentPlanes(Options& opts, bool value);

void setDefaultNlExtTangentPlanes(Options& opts, bool value);

void setDefaultNlExtTangentPlanesInterleave(Options& opts, bool value);

void setDefaultNlExt(Options& opts, NlExtMode value);

void setDefaultNlICP(Options& opts, bool value);

void setDefaultNlRlvMode(Options& opts, NlRlvMode value);

void setDefaultPbRewrites(Options& opts, bool value);

void setDefaultArithPivotThreshold(Options& opts, uint16_t value);

void setDefaultPpAssertMaxSubSize(Options& opts, unsigned value);

void setDefaultArithPropagateMaxLength(Options& opts, uint16_t value);

void setDefaultReplayEarlyCloseDepths(Options& opts, int value);

void setDefaultReplayFailurePenalty(Options& opts, int value);

void setDefaultLemmaRejectCutSize(Options& opts, unsigned value);

void setDefaultReplayNumericFailurePenalty(Options& opts, int value);

void setDefaultReplayRejectCutSize(Options& opts, unsigned value);

void setDefaultSoiApproxMajorFailurePen(Options& opts, int value);

void setDefaultSoiApproxMajorFailure(Options& opts, double value);

void setDefaultSoiApproxMinorFailurePen(Options& opts, int value);

void setDefaultSoiApproxMinorFailure(Options& opts, double value);

void setDefaultRestrictedPivots(Options& opts, bool value);

void setDefaultRevertArithModels(Options& opts, bool value);

void setDefaultRrTurns(Options& opts, int value);

void setDefaultTrySolveIntStandardEffort(Options& opts, bool value);

void setDefaultArithSimplexCheckPeriod(Options& opts, uint16_t value);

void setDefaultSoiQuickExplain(Options& opts, bool value);

void setDefaultArithStandardCheckVarOrderPivots(Options& opts, int16_t value);

void setDefaultArithUnateLemmaMode(Options& opts, ArithUnateLemmaMode value);

void setDefaultUseApprox(Options& opts, bool value);

void setDefaultUseFC(Options& opts, bool value);

void setDefaultUseSOI(Options& opts, bool value);

// clang-format on

}

}  // namespace options

}  // namespace cvc5

#endif /* CVC5__OPTIONS__ARITH_H */