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

 * 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,

  UNATE_PROP,

  BOUND_INFERENCE_PROP

};

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

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

enum class ErrorSelectionRule

{

  VAR_ORDER,

  MAXIMUM_AMOUNT,

  MINIMUM_AMOUNT,

  SUM_METRIC

};

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

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

enum class NlExtMode

{

  NONE,

  LIGHT,

  FULL

};

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

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

enum class NlRlvMode

{

  NONE,

  ALWAYS,

  INTERLEAVE

};

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

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

enum class ArithUnateLemmaMode

{

  ALL,

  NO,

  EQUALITY,

  INEQUALITY

};

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 maxApproxDepth__setByUser__ = false;

  bool brabTest = true;\

  bool brabTest__setByUser__ = false;

  bool arithNoPartialFun = false;\

  bool arithNoPartialFun__setByUser__ = false;

  uint16_t arithPropAsLemmaLength = 8;\

  bool arithPropAsLemmaLength__setByUser__ = false;

  ArithPropagationMode arithPropagationMode = ArithPropagationMode::BOTH_PROP;\

  bool arithPropagationMode__setByUser__ = false;

  bool arithRewriteEq = false;\

  bool arithRewriteEq__setByUser__ = false;

  bool collectPivots = false;\

  bool collectPivots__setByUser__ = false;

  bool doCutAllBounded = false;\

  bool doCutAllBounded__setByUser__ = false;

  bool exportDioDecompositions = false;\

  bool exportDioDecompositions__setByUser__ = false;

  bool dioRepeat = false;\

  bool dioRepeat__setByUser__ = false;

  bool arithDioSolver = true;\

  bool arithDioSolver__setByUser__ = false;

  int dioSolverTurns = 10;\

  bool dioSolverTurns__setByUser__ = false;

  ErrorSelectionRule arithErrorSelectionRule = ErrorSelectionRule::MINIMUM_AMOUNT;\

  bool arithErrorSelectionRule__setByUser__ = false;

  bool havePenalties = false;\

  bool havePenalties__setByUser__ = false;

  int16_t arithHeuristicPivots = 0;\

  bool arithHeuristicPivots__setByUser__ = false;

  bool replayFailureLemma = false;\

  bool replayFailureLemma__setByUser__ = false;

  unsigned maxCutsInContext = 65535;\

  bool maxCutsInContext__setByUser__ = false;

  bool arithMLTrick = false;\

  bool arithMLTrick__setByUser__ = false;

  unsigned arithMLTrickSubstitutions = 1;\

  bool arithMLTrickSubstitutions__setByUser__ = false;

  bool newProp = true;\

  bool newProp__setByUser__ = false;

  bool nlCad = false;\

  bool nlCad__setByUser__ = false;

  bool nlCadUseInitial = false;\

  bool nlCadUseInitial__setByUser__ = false;

  bool nlExtEntailConflicts = false;\

  bool nlExtEntailConflicts__setByUser__ = false;

  bool nlExtFactor = true;\

  bool nlExtFactor__setByUser__ = false;

  bool nlExtIncPrecision = true;\

  bool nlExtIncPrecision__setByUser__ = false;

  bool nlExtPurify = false;\

  bool nlExtPurify__setByUser__ = false;

  bool nlExtResBound = false;\

  bool nlExtResBound__setByUser__ = false;

  bool nlExtRewrites = true;\

  bool nlExtRewrites__setByUser__ = false;

  bool nlExtSplitZero = false;\

  bool nlExtSplitZero__setByUser__ = false;

  int16_t nlExtTfTaylorDegree = 4;\

  bool nlExtTfTaylorDegree__setByUser__ = false;

  bool nlExtTfTangentPlanes = true;\

  bool nlExtTfTangentPlanes__setByUser__ = false;

  bool nlExtTangentPlanes = false;\

  bool nlExtTangentPlanes__setByUser__ = false;

  bool nlExtTangentPlanesInterleave = false;\

  bool nlExtTangentPlanesInterleave__setByUser__ = false;

  NlExtMode nlExt = NlExtMode::FULL;\

  bool nlExt__setByUser__ = false;

  bool nlICP = false;\

  bool nlICP__setByUser__ = false;

  NlRlvMode nlRlvMode = NlRlvMode::NONE;\

  bool nlRlvMode__setByUser__ = false;

  bool pbRewrites = false;\

  bool pbRewrites__setByUser__ = false;

  uint16_t arithPivotThreshold = 2;\

  bool arithPivotThreshold__setByUser__ = false;

  unsigned ppAssertMaxSubSize = 2;\

  bool ppAssertMaxSubSize__setByUser__ = false;

  uint16_t arithPropagateMaxLength = 16;\

  bool arithPropagateMaxLength__setByUser__ = false;

  int replayEarlyCloseDepths = 1;\

  bool replayEarlyCloseDepths__setByUser__ = false;

  int replayFailurePenalty = 100;\

  bool replayFailurePenalty__setByUser__ = false;

  unsigned lemmaRejectCutSize = 25500;\

  bool lemmaRejectCutSize__setByUser__ = false;

  int replayNumericFailurePenalty = 4194304;\

  bool replayNumericFailurePenalty__setByUser__ = false;

  unsigned replayRejectCutSize = 25500;\

  bool replayRejectCutSize__setByUser__ = false;

  int soiApproxMajorFailurePen = 50;\

  bool soiApproxMajorFailurePen__setByUser__ = false;

  double soiApproxMajorFailure = .01;\

  bool soiApproxMajorFailure__setByUser__ = false;

  int soiApproxMinorFailurePen = 10;\

  bool soiApproxMinorFailurePen__setByUser__ = false;

  double soiApproxMinorFailure = .0001;\

  bool soiApproxMinorFailure__setByUser__ = false;

  bool restrictedPivots = true;\

  bool restrictedPivots__setByUser__ = false;

  bool revertArithModels = false;\

  bool revertArithModels__setByUser__ = false;

  int rrTurns = 3;\

  bool rrTurns__setByUser__ = false;

  bool trySolveIntStandardEffort = false;\

  bool trySolveIntStandardEffort__setByUser__ = false;

  uint16_t arithSimplexCheckPeriod = 200;\

  bool arithSimplexCheckPeriod__setByUser__ = false;

  bool soiQuickExplain = false;\

  bool soiQuickExplain__setByUser__ = false;

  int16_t arithStandardCheckVarOrderPivots = -1;\

  bool arithStandardCheckVarOrderPivots__setByUser__ = false;

  ArithUnateLemmaMode arithUnateLemmaMode = ArithUnateLemmaMode::ALL;\

  bool arithUnateLemmaMode__setByUser__ = false;

  bool useApprox = false;\

  bool useApprox__setByUser__ = false;

  bool useFC = false;\

  bool useFC__setByUser__ = false;

  bool useSOI = false;\

  bool useSOI__setByUser__ = 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 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 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* 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* 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

template <> options::maxApproxDepth__option_t::type& Options::ref(

    options::maxApproxDepth__option_t);

template <> const options::maxApproxDepth__option_t::type& Options::operator[](

    options::maxApproxDepth__option_t) const;

template <> bool Options::wasSetByUser(options::maxApproxDepth__option_t) const;

template <> options::brabTest__option_t::type& Options::ref(

    options::brabTest__option_t);

template <> const options::brabTest__option_t::type& Options::operator[](

    options::brabTest__option_t) const;

template <> bool Options::wasSetByUser(options::brabTest__option_t) const;

template <> options::arithNoPartialFun__option_t::type& Options::ref(

    options::arithNoPartialFun__option_t);

template <> const options::arithNoPartialFun__option_t::type& Options::operator[](

    options::arithNoPartialFun__option_t) const;

template <> bool Options::wasSetByUser(options::arithNoPartialFun__option_t) const;

template <> options::arithPropAsLemmaLength__option_t::type& Options::ref(

    options::arithPropAsLemmaLength__option_t);

template <> const options::arithPropAsLemmaLength__option_t::type& Options::operator[](

    options::arithPropAsLemmaLength__option_t) const;

template <> bool Options::wasSetByUser(options::arithPropAsLemmaLength__option_t) const;

template <> options::arithPropagationMode__option_t::type& Options::ref(

    options::arithPropagationMode__option_t);

template <> const options::arithPropagationMode__option_t::type& Options::operator[](

    options::arithPropagationMode__option_t) const;

template <> bool Options::wasSetByUser(options::arithPropagationMode__option_t) const;

template <> options::arithRewriteEq__option_t::type& Options::ref(

    options::arithRewriteEq__option_t);

template <> const options::arithRewriteEq__option_t::type& Options::operator[](

    options::arithRewriteEq__option_t) const;

template <> bool Options::wasSetByUser(options::arithRewriteEq__option_t) const;

template <> options::collectPivots__option_t::type& Options::ref(

    options::collectPivots__option_t);

template <> const options::collectPivots__option_t::type& Options::operator[](

    options::collectPivots__option_t) const;

template <> bool Options::wasSetByUser(options::collectPivots__option_t) const;

template <> options::doCutAllBounded__option_t::type& Options::ref(

    options::doCutAllBounded__option_t);

template <> const options::doCutAllBounded__option_t::type& Options::operator[](

    options::doCutAllBounded__option_t) const;

template <> bool Options::wasSetByUser(options::doCutAllBounded__option_t) const;

template <> options::exportDioDecompositions__option_t::type& Options::ref(

    options::exportDioDecompositions__option_t);

template <> const options::exportDioDecompositions__option_t::type& Options::operator[](

    options::exportDioDecompositions__option_t) const;

template <> bool Options::wasSetByUser(options::exportDioDecompositions__option_t) const;

template <> options::dioRepeat__option_t::type& Options::ref(

    options::dioRepeat__option_t);

template <> const options::dioRepeat__option_t::type& Options::operator[](

    options::dioRepeat__option_t) const;

template <> bool Options::wasSetByUser(options::dioRepeat__option_t) const;

template <> options::arithDioSolver__option_t::type& Options::ref(

    options::arithDioSolver__option_t);

template <> const options::arithDioSolver__option_t::type& Options::operator[](

    options::arithDioSolver__option_t) const;

template <> bool Options::wasSetByUser(options::arithDioSolver__option_t) const;

template <> options::dioSolverTurns__option_t::type& Options::ref(

    options::dioSolverTurns__option_t);

template <> const options::dioSolverTurns__option_t::type& Options::operator[](

    options::dioSolverTurns__option_t) const;

template <> bool Options::wasSetByUser(options::dioSolverTurns__option_t) const;

template <> options::arithErrorSelectionRule__option_t::type& Options::ref(

    options::arithErrorSelectionRule__option_t);

template <> const options::arithErrorSelectionRule__option_t::type& Options::operator[](

    options::arithErrorSelectionRule__option_t) const;

template <> bool Options::wasSetByUser(options::arithErrorSelectionRule__option_t) const;

template <> options::havePenalties__option_t::type& Options::ref(

    options::havePenalties__option_t);

template <> const options::havePenalties__option_t::type& Options::operator[](

    options::havePenalties__option_t) const;

template <> bool Options::wasSetByUser(options::havePenalties__option_t) const;

template <> options::arithHeuristicPivots__option_t::type& Options::ref(

    options::arithHeuristicPivots__option_t);

template <> const options::arithHeuristicPivots__option_t::type& Options::operator[](

    options::arithHeuristicPivots__option_t) const;

template <> bool Options::wasSetByUser(options::arithHeuristicPivots__option_t) const;

template <> options::replayFailureLemma__option_t::type& Options::ref(

    options::replayFailureLemma__option_t);

template <> const options::replayFailureLemma__option_t::type& Options::operator[](

    options::replayFailureLemma__option_t) const;

template <> bool Options::wasSetByUser(options::replayFailureLemma__option_t) const;

template <> options::maxCutsInContext__option_t::type& Options::ref(

    options::maxCutsInContext__option_t);

template <> const options::maxCutsInContext__option_t::type& Options::operator[](

    options::maxCutsInContext__option_t) const;

template <> bool Options::wasSetByUser(options::maxCutsInContext__option_t) const;

template <> options::arithMLTrick__option_t::type& Options::ref(

    options::arithMLTrick__option_t);

template <> const options::arithMLTrick__option_t::type& Options::operator[](

    options::arithMLTrick__option_t) const;

template <> bool Options::wasSetByUser(options::arithMLTrick__option_t) const;

template <> options::arithMLTrickSubstitutions__option_t::type& Options::ref(

    options::arithMLTrickSubstitutions__option_t);

template <> const options::arithMLTrickSubstitutions__option_t::type& Options::operator[](

    options::arithMLTrickSubstitutions__option_t) const;

template <> bool Options::wasSetByUser(options::arithMLTrickSubstitutions__option_t) const;

template <> options::newProp__option_t::type& Options::ref(

    options::newProp__option_t);

template <> const options::newProp__option_t::type& Options::operator[](

    options::newProp__option_t) const;

template <> bool Options::wasSetByUser(options::newProp__option_t) const;

template <> options::nlCad__option_t::type& Options::ref(

    options::nlCad__option_t);

template <> const options::nlCad__option_t::type& Options::operator[](

    options::nlCad__option_t) const;

template <> bool Options::wasSetByUser(options::nlCad__option_t) const;

template <> options::nlCadUseInitial__option_t::type& Options::ref(

    options::nlCadUseInitial__option_t);

template <> const options::nlCadUseInitial__option_t::type& Options::operator[](

    options::nlCadUseInitial__option_t) const;

template <> bool Options::wasSetByUser(options::nlCadUseInitial__option_t) const;

template <> options::nlExtEntailConflicts__option_t::type& Options::ref(

    options::nlExtEntailConflicts__option_t);

template <> const options::nlExtEntailConflicts__option_t::type& Options::operator[](

    options::nlExtEntailConflicts__option_t) const;

template <> bool Options::wasSetByUser(options::nlExtEntailConflicts__option_t) const;

template <> options::nlExtFactor__option_t::type& Options::ref(

    options::nlExtFactor__option_t);

template <> const options::nlExtFactor__option_t::type& Options::operator[](

    options::nlExtFactor__option_t) const;

template <> bool Options::wasSetByUser(options::nlExtFactor__option_t) const;

template <> options::nlExtIncPrecision__option_t::type& Options::ref(

    options::nlExtIncPrecision__option_t);

template <> const options::nlExtIncPrecision__option_t::type& Options::operator[](

    options::nlExtIncPrecision__option_t) const;

template <> bool Options::wasSetByUser(options::nlExtIncPrecision__option_t) const;

template <> options::nlExtPurify__option_t::type& Options::ref(

    options::nlExtPurify__option_t);

template <> const options::nlExtPurify__option_t::type& Options::operator[](

    options::nlExtPurify__option_t) const;

template <> bool Options::wasSetByUser(options::nlExtPurify__option_t) const;

template <> options::nlExtResBound__option_t::type& Options::ref(

    options::nlExtResBound__option_t);

template <> const options::nlExtResBound__option_t::type& Options::operator[](

    options::nlExtResBound__option_t) const;

template <> bool Options::wasSetByUser(options::nlExtResBound__option_t) const;

template <> options::nlExtRewrites__option_t::type& Options::ref(

    options::nlExtRewrites__option_t);

template <> const options::nlExtRewrites__option_t::type& Options::operator[](

    options::nlExtRewrites__option_t) const;

template <> bool Options::wasSetByUser(options::nlExtRewrites__option_t) const;

template <> options::nlExtSplitZero__option_t::type& Options::ref(

    options::nlExtSplitZero__option_t);

template <> const options::nlExtSplitZero__option_t::type& Options::operator[](

    options::nlExtSplitZero__option_t) const;

template <> bool Options::wasSetByUser(options::nlExtSplitZero__option_t) const;

template <> options::nlExtTfTaylorDegree__option_t::type& Options::ref(

    options::nlExtTfTaylorDegree__option_t);

template <> const options::nlExtTfTaylorDegree__option_t::type& Options::operator[](

    options::nlExtTfTaylorDegree__option_t) const;

template <> bool Options::wasSetByUser(options::nlExtTfTaylorDegree__option_t) const;

template <> options::nlExtTfTangentPlanes__option_t::type& Options::ref(

    options::nlExtTfTangentPlanes__option_t);

template <> const options::nlExtTfTangentPlanes__option_t::type& Options::operator[](

    options::nlExtTfTangentPlanes__option_t) const;

template <> bool Options::wasSetByUser(options::nlExtTfTangentPlanes__option_t) const;

template <> options::nlExtTangentPlanes__option_t::type& Options::ref(

    options::nlExtTangentPlanes__option_t);

template <> const options::nlExtTangentPlanes__option_t::type& Options::operator[](

    options::nlExtTangentPlanes__option_t) const;

template <> bool Options::wasSetByUser(options::nlExtTangentPlanes__option_t) const;

template <> options::nlExtTangentPlanesInterleave__option_t::type& Options::ref(

    options::nlExtTangentPlanesInterleave__option_t);

template <> const options::nlExtTangentPlanesInterleave__option_t::type& Options::operator[](

    options::nlExtTangentPlanesInterleave__option_t) const;

template <> bool Options::wasSetByUser(options::nlExtTangentPlanesInterleave__option_t) const;

template <> options::nlExt__option_t::type& Options::ref(

    options::nlExt__option_t);

template <> const options::nlExt__option_t::type& Options::operator[](

    options::nlExt__option_t) const;

template <> bool Options::wasSetByUser(options::nlExt__option_t) const;

template <> options::nlICP__option_t::type& Options::ref(

    options::nlICP__option_t);

template <> const options::nlICP__option_t::type& Options::operator[](

    options::nlICP__option_t) const;

template <> bool Options::wasSetByUser(options::nlICP__option_t) const;

template <> options::nlRlvMode__option_t::type& Options::ref(

    options::nlRlvMode__option_t);

template <> const options::nlRlvMode__option_t::type& Options::operator[](

    options::nlRlvMode__option_t) const;

template <> bool Options::wasSetByUser(options::nlRlvMode__option_t) const;

template <> options::pbRewrites__option_t::type& Options::ref(

    options::pbRewrites__option_t);

template <> const options::pbRewrites__option_t::type& Options::operator[](

    options::pbRewrites__option_t) const;

template <> bool Options::wasSetByUser(options::pbRewrites__option_t) const;

template <> options::arithPivotThreshold__option_t::type& Options::ref(

    options::arithPivotThreshold__option_t);

template <> const options::arithPivotThreshold__option_t::type& Options::operator[](

    options::arithPivotThreshold__option_t) const;

template <> bool Options::wasSetByUser(options::arithPivotThreshold__option_t) const;

template <> options::ppAssertMaxSubSize__option_t::type& Options::ref(

    options::ppAssertMaxSubSize__option_t);

template <> const options::ppAssertMaxSubSize__option_t::type& Options::operator[](

    options::ppAssertMaxSubSize__option_t) const;

template <> bool Options::wasSetByUser(options::ppAssertMaxSubSize__option_t) const;

template <> options::arithPropagateMaxLength__option_t::type& Options::ref(

    options::arithPropagateMaxLength__option_t);

template <> const options::arithPropagateMaxLength__option_t::type& Options::operator[](

    options::arithPropagateMaxLength__option_t) const;

template <> bool Options::wasSetByUser(options::arithPropagateMaxLength__option_t) const;

template <> options::replayEarlyCloseDepths__option_t::type& Options::ref(

    options::replayEarlyCloseDepths__option_t);

template <> const options::replayEarlyCloseDepths__option_t::type& Options::operator[](

    options::replayEarlyCloseDepths__option_t) const;

template <> bool Options::wasSetByUser(options::replayEarlyCloseDepths__option_t) const;

template <> options::replayFailurePenalty__option_t::type& Options::ref(

    options::replayFailurePenalty__option_t);

template <> const options::replayFailurePenalty__option_t::type& Options::operator[](

    options::replayFailurePenalty__option_t) const;

template <> bool Options::wasSetByUser(options::replayFailurePenalty__option_t) const;

template <> options::lemmaRejectCutSize__option_t::type& Options::ref(

    options::lemmaRejectCutSize__option_t);

template <> const options::lemmaRejectCutSize__option_t::type& Options::operator[](

    options::lemmaRejectCutSize__option_t) const;

template <> bool Options::wasSetByUser(options::lemmaRejectCutSize__option_t) const;

template <> options::replayNumericFailurePenalty__option_t::type& Options::ref(

    options::replayNumericFailurePenalty__option_t);

template <> const options::replayNumericFailurePenalty__option_t::type& Options::operator[](

    options::replayNumericFailurePenalty__option_t) const;

template <> bool Options::wasSetByUser(options::replayNumericFailurePenalty__option_t) const;

template <> options::replayRejectCutSize__option_t::type& Options::ref(

    options::replayRejectCutSize__option_t);

template <> const options::replayRejectCutSize__option_t::type& Options::operator[](

    options::replayRejectCutSize__option_t) const;

template <> bool Options::wasSetByUser(options::replayRejectCutSize__option_t) const;

template <> options::soiApproxMajorFailurePen__option_t::type& Options::ref(

    options::soiApproxMajorFailurePen__option_t);

template <> const options::soiApproxMajorFailurePen__option_t::type& Options::operator[](

    options::soiApproxMajorFailurePen__option_t) const;

template <> bool Options::wasSetByUser(options::soiApproxMajorFailurePen__option_t) const;

template <> options::soiApproxMajorFailure__option_t::type& Options::ref(

    options::soiApproxMajorFailure__option_t);

template <> const options::soiApproxMajorFailure__option_t::type& Options::operator[](

    options::soiApproxMajorFailure__option_t) const;

template <> bool Options::wasSetByUser(options::soiApproxMajorFailure__option_t) const;

template <> options::soiApproxMinorFailurePen__option_t::type& Options::ref(

    options::soiApproxMinorFailurePen__option_t);

template <> const options::soiApproxMinorFailurePen__option_t::type& Options::operator[](

    options::soiApproxMinorFailurePen__option_t) const;

template <> bool Options::wasSetByUser(options::soiApproxMinorFailurePen__option_t) const;

template <> options::soiApproxMinorFailure__option_t::type& Options::ref(

    options::soiApproxMinorFailure__option_t);

template <> const options::soiApproxMinorFailure__option_t::type& Options::operator[](

    options::soiApproxMinorFailure__option_t) const;

template <> bool Options::wasSetByUser(options::soiApproxMinorFailure__option_t) const;

template <> options::restrictedPivots__option_t::type& Options::ref(

    options::restrictedPivots__option_t);

template <> const options::restrictedPivots__option_t::type& Options::operator[](

    options::restrictedPivots__option_t) const;

template <> bool Options::wasSetByUser(options::restrictedPivots__option_t) const;

template <> options::revertArithModels__option_t::type& Options::ref(

    options::revertArithModels__option_t);

template <> const options::revertArithModels__option_t::type& Options::operator[](

    options::revertArithModels__option_t) const;

template <> bool Options::wasSetByUser(options::revertArithModels__option_t) const;

template <> options::rrTurns__option_t::type& Options::ref(

    options::rrTurns__option_t);

template <> const options::rrTurns__option_t::type& Options::operator[](

    options::rrTurns__option_t) const;

template <> bool Options::wasSetByUser(options::rrTurns__option_t) const;

template <> options::trySolveIntStandardEffort__option_t::type& Options::ref(

    options::trySolveIntStandardEffort__option_t);

template <> const options::trySolveIntStandardEffort__option_t::type& Options::operator[](

    options::trySolveIntStandardEffort__option_t) const;

template <> bool Options::wasSetByUser(options::trySolveIntStandardEffort__option_t) const;

template <> options::arithSimplexCheckPeriod__option_t::type& Options::ref(

    options::arithSimplexCheckPeriod__option_t);

template <> const options::arithSimplexCheckPeriod__option_t::type& Options::operator[](

    options::arithSimplexCheckPeriod__option_t) const;

template <> bool Options::wasSetByUser(options::arithSimplexCheckPeriod__option_t) const;

template <> options::soiQuickExplain__option_t::type& Options::ref(

    options::soiQuickExplain__option_t);

template <> const options::soiQuickExplain__option_t::type& Options::operator[](

    options::soiQuickExplain__option_t) const;

template <> bool Options::wasSetByUser(options::soiQuickExplain__option_t) const;

template <> options::arithStandardCheckVarOrderPivots__option_t::type& Options::ref(

    options::arithStandardCheckVarOrderPivots__option_t);

template <> const options::arithStandardCheckVarOrderPivots__option_t::type& Options::operator[](

    options::arithStandardCheckVarOrderPivots__option_t) const;

template <> bool Options::wasSetByUser(options::arithStandardCheckVarOrderPivots__option_t) const;

template <> options::arithUnateLemmaMode__option_t::type& Options::ref(

    options::arithUnateLemmaMode__option_t);

template <> const options::arithUnateLemmaMode__option_t::type& Options::operator[](

    options::arithUnateLemmaMode__option_t) const;

template <> bool Options::wasSetByUser(options::arithUnateLemmaMode__option_t) const;

template <> options::useApprox__option_t::type& Options::ref(

    options::useApprox__option_t);

template <> const options::useApprox__option_t::type& Options::operator[](

    options::useApprox__option_t) const;

template <> bool Options::wasSetByUser(options::useApprox__option_t) const;

template <> options::useFC__option_t::type& Options::ref(

    options::useFC__option_t);

template <> const options::useFC__option_t::type& Options::operator[](

    options::useFC__option_t) const;

template <> bool Options::wasSetByUser(options::useFC__option_t) const;

template <> options::useSOI__option_t::type& Options::ref(

    options::useSOI__option_t);

template <> const options::useSOI__option_t::type& Options::operator[](

    options::useSOI__option_t) const;

template <> bool Options::wasSetByUser(options::useSOI__option_t) const;

// clang-format on

namespace options {

// clang-format off

{

}

{

}

{

}

{

}

{

}

{

}

{

}

{

}

{

}

inline dioRepeat__option_t::type dioRepeat__option_t::operator()() const

{

  return Options::current()[*this];

}

{

}

{

}

{

}

{

}

{

}

{

}

{

}

{

}

{

}

{

}

{

}

{

}

{

}

{

}

{

}

{

}

{

}

{

}

{

}

{

}

{

}

{

}

{

}

{

}

{

}

{

}

{

}

{

}

{

}

{

}

{

}

inline replayFailurePenalty__option_t::type replayFailurePenalty__option_t::operator()() const

{

  return Options::current()[*this];

}

{

}

{

}

{

}

inline soiApproxMajorFailurePen__option_t::type soiApproxMajorFailurePen__option_t::operator()() const

{

  return Options::current()[*this];

}

inline soiApproxMajorFailure__option_t::type soiApproxMajorFailure__option_t::operator()() const

{

  return Options::current()[*this];

}

inline soiApproxMinorFailurePen__option_t::type soiApproxMinorFailurePen__option_t::operator()() const

{

  return Options::current()[*this];

}

inline soiApproxMinorFailure__option_t::type soiApproxMinorFailure__option_t::operator()() const

{

  return Options::current()[*this];

}

{

}

{

}

{

}

{

}

{

}

{

}

{

}

{

}

{

}

{

}

{

}

// clang-format on

}  // namespace options

}  // namespace cvc5

#endif /* CVC5__OPTIONS__ARITH_H */