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

 * 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::options {

// clang-format off

enum class ArithPropagationMode

{

  NO_PROP, BOTH_PROP, UNATE_PROP, BOUND_INFERENCE_PROP,

  __MAX_VALUE = BOUND_INFERENCE_PROP

};

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

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

enum class ErrorSelectionRule

{

  MAXIMUM_AMOUNT, VAR_ORDER, SUM_METRIC, MINIMUM_AMOUNT,

  __MAX_VALUE = MINIMUM_AMOUNT

};

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

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

enum class NlCadLiftingMode

{

  LAZARD, REGULAR,

  __MAX_VALUE = REGULAR

};

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

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

enum class NlCadProjectionMode

{

  LAZARDMOD, LAZARD, MCCALLUM,

  __MAX_VALUE = MCCALLUM

};

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

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

enum class NlExtMode

{

  LIGHT, NONE, FULL,

  __MAX_VALUE = FULL

};

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

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

enum class NlRlvMode

{

  ALWAYS, INTERLEAVE, NONE,

  __MAX_VALUE = NONE

};

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

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

enum class ArithUnateLemmaMode

{

  INEQUALITY, EQUALITY, ALL, NO,

  __MAX_VALUE = NO

};

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

int64_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;

  ArithPropagationMode arithPropagationMode = ArithPropagationMode::BOTH_PROP;

  bool arithPropagationModeWasSetByUser = false;

  uint64_t arithPropAsLemmaLength = 8;

  bool arithPropAsLemmaLengthWasSetByUser = 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 arithDioSolver = true;

  bool arithDioSolverWasSetByUser = false;

  int64_t dioSolverTurns = 10;

  bool dioSolverTurnsWasSetByUser = false;

  ErrorSelectionRule arithErrorSelectionRule = ErrorSelectionRule::MINIMUM_AMOUNT;

  bool arithErrorSelectionRuleWasSetByUser = false;

  bool havePenalties = false;

  bool havePenaltiesWasSetByUser = false;

  int64_t arithHeuristicPivots = 0;

  bool arithHeuristicPivotsWasSetByUser = false;

  bool replayFailureLemma = false;

  bool replayFailureLemmaWasSetByUser = false;

  uint64_t maxCutsInContext = 65535;

  bool maxCutsInContextWasSetByUser = false;

  bool arithMLTrick = false;

  bool arithMLTrickWasSetByUser = false;

  uint64_t 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;

  NlExtMode nlExt = NlExtMode::FULL;

  bool nlExtWasSetByUser = 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;

  int64_t nlExtTfTaylorDegree = 4;

  bool nlExtTfTaylorDegreeWasSetByUser = false;

  bool nlExtTfTangentPlanes = true;

  bool nlExtTfTangentPlanesWasSetByUser = false;

  bool nlExtTangentPlanes = false;

  bool nlExtTangentPlanesWasSetByUser = false;

  bool nlExtTangentPlanesInterleave = false;

  bool nlExtTangentPlanesInterleaveWasSetByUser = false;

  bool nlICP = false;

  bool nlICPWasSetByUser = false;

  NlRlvMode nlRlvMode = NlRlvMode::NONE;

  bool nlRlvModeWasSetByUser = false;

  bool nlRlvAssertBounds = false;

  bool nlRlvAssertBoundsWasSetByUser = false;

  bool pbRewrites = false;

  bool pbRewritesWasSetByUser = false;

  uint64_t arithPivotThreshold = 2;

  bool arithPivotThresholdWasSetByUser = false;

  uint64_t ppAssertMaxSubSize = 2;

  bool ppAssertMaxSubSizeWasSetByUser = false;

  uint64_t arithPropagateMaxLength = 16;

  bool arithPropagateMaxLengthWasSetByUser = false;

  int64_t replayEarlyCloseDepths = 1;

  bool replayEarlyCloseDepthsWasSetByUser = false;

  uint64_t lemmaRejectCutSize = 25500;

  bool lemmaRejectCutSizeWasSetByUser = false;

  int64_t replayNumericFailurePenalty = 4194304;

  bool replayNumericFailurePenaltyWasSetByUser = false;

  uint64_t replayRejectCutSize = 25500;

  bool replayRejectCutSizeWasSetByUser = false;

  bool restrictedPivots = true;

  bool restrictedPivotsWasSetByUser = false;

  bool revertArithModels = false;

  bool revertArithModelsWasSetByUser = false;

  int64_t rrTurns = 3;

  bool rrTurnsWasSetByUser = false;

  bool trySolveIntStandardEffort = false;

  bool trySolveIntStandardEffortWasSetByUser = false;

  uint64_t arithSimplexCheckPeriod = 200;

  bool arithSimplexCheckPeriodWasSetByUser = false;

  bool soiQuickExplain = false;

  bool soiQuickExplainWasSetByUser = false;

  int64_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

inline int64_t maxApproxDepth() { return Options::current().arith.maxApproxDepth; }

inline bool brabTest() { return Options::current().arith.brabTest; }

inline bool arithCongMan() { return Options::current().arith.arithCongMan; }

inline bool arithNoPartialFun() { return Options::current().arith.arithNoPartialFun; }

inline ArithPropagationMode arithPropagationMode() { return Options::current().arith.arithPropagationMode; }

inline uint64_t arithPropAsLemmaLength() { return Options::current().arith.arithPropAsLemmaLength; }

inline bool arithRewriteEq() { return Options::current().arith.arithRewriteEq; }

inline bool collectPivots() { return Options::current().arith.collectPivots; }

inline bool doCutAllBounded() { return Options::current().arith.doCutAllBounded; }

inline bool exportDioDecompositions() { return Options::current().arith.exportDioDecompositions; }

inline bool arithDioSolver() { return Options::current().arith.arithDioSolver; }

inline int64_t dioSolverTurns() { return Options::current().arith.dioSolverTurns; }

inline ErrorSelectionRule arithErrorSelectionRule() { return Options::current().arith.arithErrorSelectionRule; }

inline bool havePenalties() { return Options::current().arith.havePenalties; }

inline int64_t arithHeuristicPivots() { return Options::current().arith.arithHeuristicPivots; }

inline bool replayFailureLemma() { return Options::current().arith.replayFailureLemma; }

inline uint64_t maxCutsInContext() { return Options::current().arith.maxCutsInContext; }

inline bool arithMLTrick() { return Options::current().arith.arithMLTrick; }

inline uint64_t arithMLTrickSubstitutions() { return Options::current().arith.arithMLTrickSubstitutions; }

inline bool newProp() { return Options::current().arith.newProp; }

inline bool nlCad() { return Options::current().arith.nlCad; }

inline bool nlCadUseInitial() { return Options::current().arith.nlCadUseInitial; }

inline NlCadLiftingMode nlCadLifting() { return Options::current().arith.nlCadLifting; }

inline NlCadProjectionMode nlCadProjection() { return Options::current().arith.nlCadProjection; }

inline NlExtMode nlExt() { return Options::current().arith.nlExt; }

inline bool nlExtEntailConflicts() { return Options::current().arith.nlExtEntailConflicts; }

inline bool nlExtFactor() { return Options::current().arith.nlExtFactor; }

inline bool nlExtIncPrecision() { return Options::current().arith.nlExtIncPrecision; }

inline bool nlExtPurify() { return Options::current().arith.nlExtPurify; }

inline bool nlExtResBound() { return Options::current().arith.nlExtResBound; }

inline bool nlExtRewrites() { return Options::current().arith.nlExtRewrites; }

inline bool nlExtSplitZero() { return Options::current().arith.nlExtSplitZero; }

inline int64_t nlExtTfTaylorDegree() { return Options::current().arith.nlExtTfTaylorDegree; }

inline bool nlExtTfTangentPlanes() { return Options::current().arith.nlExtTfTangentPlanes; }

inline bool nlExtTangentPlanes() { return Options::current().arith.nlExtTangentPlanes; }

inline bool nlExtTangentPlanesInterleave() { return Options::current().arith.nlExtTangentPlanesInterleave; }

inline bool nlICP() { return Options::current().arith.nlICP; }

inline NlRlvMode nlRlvMode() { return Options::current().arith.nlRlvMode; }

inline bool nlRlvAssertBounds() { return Options::current().arith.nlRlvAssertBounds; }

inline bool pbRewrites() { return Options::current().arith.pbRewrites; }

inline uint64_t arithPivotThreshold() { return Options::current().arith.arithPivotThreshold; }

inline uint64_t ppAssertMaxSubSize() { return Options::current().arith.ppAssertMaxSubSize; }

inline uint64_t arithPropagateMaxLength() { return Options::current().arith.arithPropagateMaxLength; }

inline int64_t replayEarlyCloseDepths() { return Options::current().arith.replayEarlyCloseDepths; }

inline uint64_t lemmaRejectCutSize() { return Options::current().arith.lemmaRejectCutSize; }

inline int64_t replayNumericFailurePenalty() { return Options::current().arith.replayNumericFailurePenalty; }

inline uint64_t replayRejectCutSize() { return Options::current().arith.replayRejectCutSize; }

inline bool restrictedPivots() { return Options::current().arith.restrictedPivots; }

inline bool revertArithModels() { return Options::current().arith.revertArithModels; }

inline int64_t rrTurns() { return Options::current().arith.rrTurns; }

inline bool trySolveIntStandardEffort() { return Options::current().arith.trySolveIntStandardEffort; }

inline uint64_t arithSimplexCheckPeriod() { return Options::current().arith.arithSimplexCheckPeriod; }

inline bool soiQuickExplain() { return Options::current().arith.soiQuickExplain; }

inline int64_t arithStandardCheckVarOrderPivots() { return Options::current().arith.arithStandardCheckVarOrderPivots; }

inline ArithUnateLemmaMode arithUnateLemmaMode() { return Options::current().arith.arithUnateLemmaMode; }

inline bool useApprox() { return Options::current().arith.useApprox; }

inline bool useFC() { return Options::current().arith.useFC; }

inline bool useSOI() { return Options::current().arith.useSOI; }

// clang-format on

}  // namespace cvc5::options

#endif /* CVC5__OPTIONS__ARITH_H */