Head

GCC Code Coverage Report

Directory:	.		Exec	Total	Coverage
File:	build-coverage/src/options/arith_options.cpp	Lines:	7	305	2.3 %
Date:	2021-09-15	Branches:	8	308	2.6 %


/******************************************************************************
 * 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.
 * ****************************************************************************
 *
 * Option template for option modules.
 *
 * For each <module>_options.toml configuration file, mkoptions.py
 * expands this template and generates a <module>_options.cpp file.
 */
#include "options/arith_options.h"

#include <iostream>

#include "base/check.h"
#include "options/option_exception.h"

namespace cvc5::options {

// clang-format off
std::ostream& operator<<(std::ostream& os, ArithPropagationMode mode)
{
  switch(mode)
  {
    case ArithPropagationMode::UNATE_PROP: return os << "ArithPropagationMode::UNATE_PROP";
    case ArithPropagationMode::BOTH_PROP: return os << "ArithPropagationMode::BOTH_PROP";
    case ArithPropagationMode::NO_PROP: return os << "ArithPropagationMode::NO_PROP";
    case ArithPropagationMode::BOUND_INFERENCE_PROP: return os << "ArithPropagationMode::BOUND_INFERENCE_PROP";
    default: Unreachable();
  }
  return os;
}
ArithPropagationMode stringToArithPropagationMode(const std::string& optarg)
{
  if (optarg == "unate") return ArithPropagationMode::UNATE_PROP;
  else if (optarg == "both") return ArithPropagationMode::BOTH_PROP;
  else if (optarg == "none") return ArithPropagationMode::NO_PROP;
  else if (optarg == "bi") return ArithPropagationMode::BOUND_INFERENCE_PROP;
  else if (optarg == "help")
  {
    std::cerr << R"FOOBAR(
  This decides on kind of propagation arithmetic attempts to do during the
  search.
Available modes for --arith-prop are:
+ unate
  Use constraints to do unate propagation.
+ both (default)
  Use bounds inference and unate.
+ bi
  (Bounds Inference) infers bounds on basic variables using the upper and lower
  bounds of the non-basic variables in the tableau.
)FOOBAR";
    std::exit(1);
  }
  throw OptionException(std::string("unknown option for --arith-prop: `") +
                        optarg + "'.  Try --arith-prop=help.");
}
std::ostream& operator<<(std::ostream& os, ErrorSelectionRule mode)
{
  switch(mode)
  {
    case ErrorSelectionRule::MINIMUM_AMOUNT: return os << "ErrorSelectionRule::MINIMUM_AMOUNT";
    case ErrorSelectionRule::SUM_METRIC: return os << "ErrorSelectionRule::SUM_METRIC";
    case ErrorSelectionRule::VAR_ORDER: return os << "ErrorSelectionRule::VAR_ORDER";
    case ErrorSelectionRule::MAXIMUM_AMOUNT: return os << "ErrorSelectionRule::MAXIMUM_AMOUNT";
    default: Unreachable();
  }
  return os;
}
ErrorSelectionRule stringToErrorSelectionRule(const std::string& optarg)
{
  if (optarg == "min") return ErrorSelectionRule::MINIMUM_AMOUNT;
  else if (optarg == "sum") return ErrorSelectionRule::SUM_METRIC;
  else if (optarg == "varord") return ErrorSelectionRule::VAR_ORDER;
  else if (optarg == "max") return ErrorSelectionRule::MAXIMUM_AMOUNT;
  else if (optarg == "help")
  {
    std::cerr << R"FOOBAR(
  This decides on the rule used by simplex during heuristic rounds for deciding
  the next basic variable to select.
Available rules for --error-selection-rule are:
+ min (default)
  The minimum abs() value of the variable's violation of its bound.
+ varord
  The variable order.
+ max
  The maximum violation the bound.
)FOOBAR";
    std::exit(1);
  }
  throw OptionException(std::string("unknown option for --error-selection-rule: `") +
                        optarg + "'.  Try --error-selection-rule=help.");
}
std::ostream& operator<<(std::ostream& os, NlCadLiftingMode mode)
{
  switch(mode)
  {
    case NlCadLiftingMode::LAZARD: return os << "NlCadLiftingMode::LAZARD";
    case NlCadLiftingMode::REGULAR: return os << "NlCadLiftingMode::REGULAR";
    default: Unreachable();
  }
  return os;
}
NlCadLiftingMode stringToNlCadLiftingMode(const std::string& optarg)
{
  if (optarg == "lazard") return NlCadLiftingMode::LAZARD;
  else if (optarg == "regular") return NlCadLiftingMode::REGULAR;
  else if (optarg == "help")
  {
    std::cerr << R"FOOBAR(
  Modes for the CAD lifting in non-linear arithmetic.
Available modes for --nl-cad-lift are:
+ lazard
  Lazard's lifting scheme.
+ regular (default)
  Regular lifting.
)FOOBAR";
    std::exit(1);
  }
  throw OptionException(std::string("unknown option for --nl-cad-lift: `") +
                        optarg + "'.  Try --nl-cad-lift=help.");
}
std::ostream& operator<<(std::ostream& os, NlCadProjectionMode mode)
{
  switch(mode)
  {
    case NlCadProjectionMode::MCCALLUM: return os << "NlCadProjectionMode::MCCALLUM";
    case NlCadProjectionMode::LAZARD: return os << "NlCadProjectionMode::LAZARD";
    case NlCadProjectionMode::LAZARDMOD: return os << "NlCadProjectionMode::LAZARDMOD";
    default: Unreachable();
  }
  return os;
}
NlCadProjectionMode stringToNlCadProjectionMode(const std::string& optarg)
{
  if (optarg == "mccallum") return NlCadProjectionMode::MCCALLUM;
  else if (optarg == "lazard") return NlCadProjectionMode::LAZARD;
  else if (optarg == "lazard-mod") return NlCadProjectionMode::LAZARDMOD;
  else if (optarg == "help")
  {
    std::cerr << R"FOOBAR(
  Modes for the CAD projection operator in non-linear arithmetic.
Available modes for --nl-cad-proj are:
+ mccallum (default)
  McCallum's projection operator.
+ lazard
  Lazard's projection operator.
+ lazard-mod
  A modification of Lazard's projection operator.
)FOOBAR";
    std::exit(1);
  }
  throw OptionException(std::string("unknown option for --nl-cad-proj: `") +
                        optarg + "'.  Try --nl-cad-proj=help.");
}
std::ostream& operator<<(std::ostream& os, NlExtMode mode)
{
  switch(mode)
  {
    case NlExtMode::NONE: return os << "NlExtMode::NONE";
    case NlExtMode::FULL: return os << "NlExtMode::FULL";
    case NlExtMode::LIGHT: return os << "NlExtMode::LIGHT";
    default: Unreachable();
  }
  return os;
}
NlExtMode stringToNlExtMode(const std::string& optarg)
{
  if (optarg == "none") return NlExtMode::NONE;
  else if (optarg == "full") return NlExtMode::FULL;
  else if (optarg == "light") return NlExtMode::LIGHT;
  else if (optarg == "help")
  {
    std::cerr << R"FOOBAR(
  Modes for the non-linear linearization
Available modes for --nl-ext are:
+ none
  Disable linearization approach
+ full (default)
  Use all lemma schemes
+ light
  Only use a few light-weight lemma schemes
)FOOBAR";
    std::exit(1);
  }
  throw OptionException(std::string("unknown option for --nl-ext: `") +
                        optarg + "'.  Try --nl-ext=help.");
}
std::ostream& operator<<(std::ostream& os, NlRlvMode mode)
{
  switch(mode)
  {
    case NlRlvMode::NONE: return os << "NlRlvMode::NONE";
    case NlRlvMode::ALWAYS: return os << "NlRlvMode::ALWAYS";
    case NlRlvMode::INTERLEAVE: return os << "NlRlvMode::INTERLEAVE";
    default: Unreachable();
  }
  return os;
}
NlRlvMode stringToNlRlvMode(const std::string& optarg)
{
  if (optarg == "none") return NlRlvMode::NONE;
  else if (optarg == "always") return NlRlvMode::ALWAYS;
  else if (optarg == "interleave") return NlRlvMode::INTERLEAVE;
  else if (optarg == "help")
  {
    std::cerr << R"FOOBAR(
  Modes for using relevance of assertions in non-linear arithmetic.
Available modes for --nl-rlv are:
+ none (default)
  Do not use relevance.
+ always
  Always use relevance.
+ interleave
  Alternate rounds using relevance.
)FOOBAR";
    std::exit(1);
  }
  throw OptionException(std::string("unknown option for --nl-rlv: `") +
                        optarg + "'.  Try --nl-rlv=help.");
}
std::ostream& operator<<(std::ostream& os, ArithUnateLemmaMode mode)
{
  switch(mode)
  {
    case ArithUnateLemmaMode::INEQUALITY: return os << "ArithUnateLemmaMode::INEQUALITY";
    case ArithUnateLemmaMode::ALL: return os << "ArithUnateLemmaMode::ALL";
    case ArithUnateLemmaMode::EQUALITY: return os << "ArithUnateLemmaMode::EQUALITY";
    case ArithUnateLemmaMode::NO: return os << "ArithUnateLemmaMode::NO";
    default: Unreachable();
  }
  return os;
}
ArithUnateLemmaMode stringToArithUnateLemmaMode(const std::string& optarg)
{
  if (optarg == "ineqs") return ArithUnateLemmaMode::INEQUALITY;
  else if (optarg == "all") return ArithUnateLemmaMode::ALL;
  else if (optarg == "eqs") return ArithUnateLemmaMode::EQUALITY;
  else if (optarg == "none") return ArithUnateLemmaMode::NO;
  else if (optarg == "help")
  {
    std::cerr << R"FOOBAR(
  Unate lemmas are generated before SAT search begins using the relationship of
  constant terms and polynomials.
Available modes for --unate-lemmas are:
+ ineqs
  Outputs lemmas of the general form (<= p c) implies (<= p d) for c < d.
+ all (default)
  A combination of inequalities and equalities.
+ eqs
  Outputs lemmas of the general forms (= p c) implies (<= p d) for c < d, or (=
  p c) implies (not (= p d)) for c != d.
)FOOBAR";
    std::exit(1);
  }
  throw OptionException(std::string("unknown option for --unate-lemmas: `") +
                        optarg + "'.  Try --unate-lemmas=help.");
}
// clang-format on

namespace arith
{
// clang-format off
void setDefaultMaxApproxDepth(Options& opts, int64_t value)
{
    if (!opts.arith.maxApproxDepthWasSetByUser) opts.arith.maxApproxDepth = value;
}
void setDefaultBrabTest(Options& opts, bool value)
{
    if (!opts.arith.brabTestWasSetByUser) opts.arith.brabTest = value;
}
void setDefaultArithCongMan(Options& opts, bool value)
{
    if (!opts.arith.arithCongManWasSetByUser) opts.arith.arithCongMan = value;
}
void setDefaultArithEqSolver(Options& opts, bool value)
{
    if (!opts.arith.arithEqSolverWasSetByUser) opts.arith.arithEqSolver = value;
}
void setDefaultArithNoPartialFun(Options& opts, bool value)
{
    if (!opts.arith.arithNoPartialFunWasSetByUser) opts.arith.arithNoPartialFun = value;
}
void setDefaultArithPropagationMode(Options& opts, ArithPropagationMode value)
{
    if (!opts.arith.arithPropagationModeWasSetByUser) opts.arith.arithPropagationMode = value;
}
void setDefaultArithPropAsLemmaLength(Options& opts, uint64_t value)
{
    if (!opts.arith.arithPropAsLemmaLengthWasSetByUser) opts.arith.arithPropAsLemmaLength = value;
}
void setDefaultArithRewriteEq(Options& opts, bool value)
{
    if (!opts.arith.arithRewriteEqWasSetByUser) opts.arith.arithRewriteEq = value;
}
void setDefaultCollectPivots(Options& opts, bool value)
{
    if (!opts.arith.collectPivotsWasSetByUser) opts.arith.collectPivots = value;
}
void setDefaultDoCutAllBounded(Options& opts, bool value)
{
    if (!opts.arith.doCutAllBoundedWasSetByUser) opts.arith.doCutAllBounded = value;
}
void setDefaultExportDioDecompositions(Options& opts, bool value)
{
    if (!opts.arith.exportDioDecompositionsWasSetByUser) opts.arith.exportDioDecompositions = value;
}
void setDefaultDioRepeat(Options& opts, bool value)
{
    if (!opts.arith.dioRepeatWasSetByUser) opts.arith.dioRepeat = value;
}
void setDefaultArithDioSolver(Options& opts, bool value)
{
    if (!opts.arith.arithDioSolverWasSetByUser) opts.arith.arithDioSolver = value;
}
void setDefaultDioSolverTurns(Options& opts, int64_t value)
{
    if (!opts.arith.dioSolverTurnsWasSetByUser) opts.arith.dioSolverTurns = value;
}
void setDefaultArithErrorSelectionRule(Options& opts, ErrorSelectionRule value)
{
    if (!opts.arith.arithErrorSelectionRuleWasSetByUser) opts.arith.arithErrorSelectionRule = value;
}
void setDefaultHavePenalties(Options& opts, bool value)
{
    if (!opts.arith.havePenaltiesWasSetByUser) opts.arith.havePenalties = value;
}
void setDefaultArithHeuristicPivots(Options& opts, int64_t value)
{
    if (!opts.arith.arithHeuristicPivotsWasSetByUser) opts.arith.arithHeuristicPivots = value;
}
void setDefaultReplayFailureLemma(Options& opts, bool value)
{
    if (!opts.arith.replayFailureLemmaWasSetByUser) opts.arith.replayFailureLemma = value;
}
void setDefaultMaxCutsInContext(Options& opts, uint64_t value)
{
    if (!opts.arith.maxCutsInContextWasSetByUser) opts.arith.maxCutsInContext = value;
}
void setDefaultArithMLTrick(Options& opts, bool value)
{
    if (!opts.arith.arithMLTrickWasSetByUser) opts.arith.arithMLTrick = value;
}
void setDefaultArithMLTrickSubstitutions(Options& opts, uint64_t value)
{
    if (!opts.arith.arithMLTrickSubstitutionsWasSetByUser) opts.arith.arithMLTrickSubstitutions = value;
}
void setDefaultNewProp(Options& opts, bool value)
{
    if (!opts.arith.newPropWasSetByUser) opts.arith.newProp = value;
}
void setDefaultNlCad(Options& opts, bool value)
{
    if (!opts.arith.nlCadWasSetByUser) opts.arith.nlCad = value;
}
void setDefaultNlCadUseInitial(Options& opts, bool value)
{
    if (!opts.arith.nlCadUseInitialWasSetByUser) opts.arith.nlCadUseInitial = value;
}
void setDefaultNlCadLifting(Options& opts, NlCadLiftingMode value)
{
    if (!opts.arith.nlCadLiftingWasSetByUser) opts.arith.nlCadLifting = value;
}
void setDefaultNlCadProjection(Options& opts, NlCadProjectionMode value)
{
    if (!opts.arith.nlCadProjectionWasSetByUser) opts.arith.nlCadProjection = value;
}
void setDefaultNlExt(Options& opts, NlExtMode value)
{
    if (!opts.arith.nlExtWasSetByUser) opts.arith.nlExt = value;
}
void setDefaultNlExtEntailConflicts(Options& opts, bool value)
{
    if (!opts.arith.nlExtEntailConflictsWasSetByUser) opts.arith.nlExtEntailConflicts = value;
}
void setDefaultNlExtFactor(Options& opts, bool value)
{
    if (!opts.arith.nlExtFactorWasSetByUser) opts.arith.nlExtFactor = value;
}
void setDefaultNlExtIncPrecision(Options& opts, bool value)
{
    if (!opts.arith.nlExtIncPrecisionWasSetByUser) opts.arith.nlExtIncPrecision = value;
}
void setDefaultNlExtPurify(Options& opts, bool value)
{
    if (!opts.arith.nlExtPurifyWasSetByUser) opts.arith.nlExtPurify = value;
}
void setDefaultNlExtResBound(Options& opts, bool value)
{
    if (!opts.arith.nlExtResBoundWasSetByUser) opts.arith.nlExtResBound = value;
}
void setDefaultNlExtRewrites(Options& opts, bool value)
{
    if (!opts.arith.nlExtRewritesWasSetByUser) opts.arith.nlExtRewrites = value;
}
void setDefaultNlExtSplitZero(Options& opts, bool value)
{
    if (!opts.arith.nlExtSplitZeroWasSetByUser) opts.arith.nlExtSplitZero = value;
}
void setDefaultNlExtTfTaylorDegree(Options& opts, int64_t value)
{
    if (!opts.arith.nlExtTfTaylorDegreeWasSetByUser) opts.arith.nlExtTfTaylorDegree = value;
}
void setDefaultNlExtTfTangentPlanes(Options& opts, bool value)
{
    if (!opts.arith.nlExtTfTangentPlanesWasSetByUser) opts.arith.nlExtTfTangentPlanes = value;
}
void setDefaultNlExtTangentPlanes(Options& opts, bool value)
{
    if (!opts.arith.nlExtTangentPlanesWasSetByUser) opts.arith.nlExtTangentPlanes = value;
}
void setDefaultNlExtTangentPlanesInterleave(Options& opts, bool value)
{
    if (!opts.arith.nlExtTangentPlanesInterleaveWasSetByUser) opts.arith.nlExtTangentPlanesInterleave = value;
}
void setDefaultNlICP(Options& opts, bool value)
{
    if (!opts.arith.nlICPWasSetByUser) opts.arith.nlICP = value;
}
void setDefaultNlRlvMode(Options& opts, NlRlvMode value)
{
    if (!opts.arith.nlRlvModeWasSetByUser) opts.arith.nlRlvMode = value;
}
void setDefaultNlRlvAssertBounds(Options& opts, bool value)
{
    if (!opts.arith.nlRlvAssertBoundsWasSetByUser) opts.arith.nlRlvAssertBounds = value;
}
void setDefaultPbRewrites(Options& opts, bool value)
{
    if (!opts.arith.pbRewritesWasSetByUser) opts.arith.pbRewrites = value;
}
void setDefaultArithPivotThreshold(Options& opts, uint64_t value)
{
    if (!opts.arith.arithPivotThresholdWasSetByUser) opts.arith.arithPivotThreshold = value;
}
void setDefaultPpAssertMaxSubSize(Options& opts, uint64_t value)
{
    if (!opts.arith.ppAssertMaxSubSizeWasSetByUser) opts.arith.ppAssertMaxSubSize = value;
}
void setDefaultArithPropagateMaxLength(Options& opts, uint64_t value)
{
    if (!opts.arith.arithPropagateMaxLengthWasSetByUser) opts.arith.arithPropagateMaxLength = value;
}
void setDefaultReplayEarlyCloseDepths(Options& opts, int64_t value)
{
    if (!opts.arith.replayEarlyCloseDepthsWasSetByUser) opts.arith.replayEarlyCloseDepths = value;
}
void setDefaultReplayFailurePenalty(Options& opts, int64_t value)
{
    if (!opts.arith.replayFailurePenaltyWasSetByUser) opts.arith.replayFailurePenalty = value;
}
void setDefaultLemmaRejectCutSize(Options& opts, uint64_t value)
{
    if (!opts.arith.lemmaRejectCutSizeWasSetByUser) opts.arith.lemmaRejectCutSize = value;
}
void setDefaultReplayNumericFailurePenalty(Options& opts, int64_t value)
{
    if (!opts.arith.replayNumericFailurePenaltyWasSetByUser) opts.arith.replayNumericFailurePenalty = value;
}
void setDefaultReplayRejectCutSize(Options& opts, uint64_t value)
{
    if (!opts.arith.replayRejectCutSizeWasSetByUser) opts.arith.replayRejectCutSize = value;
}
void setDefaultSoiApproxMajorFailure(Options& opts, double value)
{
    if (!opts.arith.soiApproxMajorFailureWasSetByUser) opts.arith.soiApproxMajorFailure = value;
}
void setDefaultSoiApproxMajorFailurePen(Options& opts, int64_t value)
{
    if (!opts.arith.soiApproxMajorFailurePenWasSetByUser) opts.arith.soiApproxMajorFailurePen = value;
}
void setDefaultSoiApproxMinorFailure(Options& opts, double value)
{
    if (!opts.arith.soiApproxMinorFailureWasSetByUser) opts.arith.soiApproxMinorFailure = value;
}
void setDefaultSoiApproxMinorFailurePen(Options& opts, int64_t value)
{
    if (!opts.arith.soiApproxMinorFailurePenWasSetByUser) opts.arith.soiApproxMinorFailurePen = value;
}
void setDefaultRestrictedPivots(Options& opts, bool value)
{
    if (!opts.arith.restrictedPivotsWasSetByUser) opts.arith.restrictedPivots = value;
}
void setDefaultRevertArithModels(Options& opts, bool value)
{
    if (!opts.arith.revertArithModelsWasSetByUser) opts.arith.revertArithModels = value;
}
void setDefaultRrTurns(Options& opts, int64_t value)
{
    if (!opts.arith.rrTurnsWasSetByUser) opts.arith.rrTurns = value;
}
void setDefaultTrySolveIntStandardEffort(Options& opts, bool value)
{
    if (!opts.arith.trySolveIntStandardEffortWasSetByUser) opts.arith.trySolveIntStandardEffort = value;
}
void setDefaultArithSimplexCheckPeriod(Options& opts, uint64_t value)
{
    if (!opts.arith.arithSimplexCheckPeriodWasSetByUser) opts.arith.arithSimplexCheckPeriod = value;
}
void setDefaultSoiQuickExplain(Options& opts, bool value)
{
    if (!opts.arith.soiQuickExplainWasSetByUser) opts.arith.soiQuickExplain = value;
}
void setDefaultArithStandardCheckVarOrderPivots(Options& opts, int64_t value)
{
    if (!opts.arith.arithStandardCheckVarOrderPivotsWasSetByUser) opts.arith.arithStandardCheckVarOrderPivots = value;
}
void setDefaultArithUnateLemmaMode(Options& opts, ArithUnateLemmaMode value)
{
    if (!opts.arith.arithUnateLemmaModeWasSetByUser) opts.arith.arithUnateLemmaMode = value;
}
void setDefaultUseApprox(Options& opts, bool value)
{
    if (!opts.arith.useApproxWasSetByUser) opts.arith.useApprox = value;
}
void setDefaultUseFC(Options& opts, bool value)
{
    if (!opts.arith.useFCWasSetByUser) opts.arith.useFC = value;
}
void setDefaultUseSOI(Options& opts, bool value)
{
    if (!opts.arith.useSOIWasSetByUser) opts.arith.useSOI = value;
}
// clang-format on
}

}  // namespace cvc5::options


Generated by: GCOVR (Version 3.2)

Line	Exec	Source
1		/******************************************************************************
2		* Top contributors (to current version):
3		* Mathias Preiner, Aina Niemetz
4		*
5		* This file is part of the cvc5 project.
6		*
7		* Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
8		* in the top-level source directory and their institutional affiliations.
9		* All rights reserved. See the file COPYING in the top-level source
10		* directory for licensing information.
11		* ****************************************************************************
12		*
13		* Option template for option modules.
14		*
15		* For each <module>_options.toml configuration file, mkoptions.py
16		* expands this template and generates a <module>_options.cpp file.
17		*/
18		#include "options/arith_options.h"
19
20		#include <iostream>
21
22		#include "base/check.h"
23		#include "options/option_exception.h"
24
25		namespace cvc5::options {
26
27		// clang-format off
28		std::ostream& operator<<(std::ostream& os, ArithPropagationMode mode)
29		{
30		switch(mode)
31		{
32		case ArithPropagationMode::UNATE_PROP: return os << "ArithPropagationMode::UNATE_PROP";
33		case ArithPropagationMode::BOTH_PROP: return os << "ArithPropagationMode::BOTH_PROP";
34		case ArithPropagationMode::NO_PROP: return os << "ArithPropagationMode::NO_PROP";
35		case ArithPropagationMode::BOUND_INFERENCE_PROP: return os << "ArithPropagationMode::BOUND_INFERENCE_PROP";
36		default: Unreachable();
37		}
38		return os;
39		}
40		ArithPropagationMode stringToArithPropagationMode(const std::string& optarg)
41		{
42		if (optarg == "unate") return ArithPropagationMode::UNATE_PROP;
43		else if (optarg == "both") return ArithPropagationMode::BOTH_PROP;
44		else if (optarg == "none") return ArithPropagationMode::NO_PROP;
45		else if (optarg == "bi") return ArithPropagationMode::BOUND_INFERENCE_PROP;
46		else if (optarg == "help")
47		{
48		std::cerr << R"FOOBAR(
49		This decides on kind of propagation arithmetic attempts to do during the
50		search.
51		Available modes for --arith-prop are:
52		+ unate
53		Use constraints to do unate propagation.
54		+ both (default)
55		Use bounds inference and unate.
56		+ bi
57		(Bounds Inference) infers bounds on basic variables using the upper and lower
58		bounds of the non-basic variables in the tableau.
59		)FOOBAR";
60		std::exit(1);
61		}
62		throw OptionException(std::string("unknown option for --arith-prop: `") +
63		optarg + "'. Try --arith-prop=help.");
64		}
65		std::ostream& operator<<(std::ostream& os, ErrorSelectionRule mode)
66		{
67		switch(mode)
68		{
69		case ErrorSelectionRule::MINIMUM_AMOUNT: return os << "ErrorSelectionRule::MINIMUM_AMOUNT";
70		case ErrorSelectionRule::SUM_METRIC: return os << "ErrorSelectionRule::SUM_METRIC";
71		case ErrorSelectionRule::VAR_ORDER: return os << "ErrorSelectionRule::VAR_ORDER";
72		case ErrorSelectionRule::MAXIMUM_AMOUNT: return os << "ErrorSelectionRule::MAXIMUM_AMOUNT";
73		default: Unreachable();
74		}
75		return os;
76		}
77		ErrorSelectionRule stringToErrorSelectionRule(const std::string& optarg)
78		{
79		if (optarg == "min") return ErrorSelectionRule::MINIMUM_AMOUNT;
80		else if (optarg == "sum") return ErrorSelectionRule::SUM_METRIC;
81		else if (optarg == "varord") return ErrorSelectionRule::VAR_ORDER;
82		else if (optarg == "max") return ErrorSelectionRule::MAXIMUM_AMOUNT;
83		else if (optarg == "help")
84		{
85		std::cerr << R"FOOBAR(
86		This decides on the rule used by simplex during heuristic rounds for deciding
87		the next basic variable to select.
88		Available rules for --error-selection-rule are:
89		+ min (default)
90		The minimum abs() value of the variable's violation of its bound.
91		+ varord
92		The variable order.
93		+ max
94		The maximum violation the bound.
95		)FOOBAR";
96		std::exit(1);
97		}
98		throw OptionException(std::string("unknown option for --error-selection-rule: `") +
99		optarg + "'. Try --error-selection-rule=help.");
100		}
101		std::ostream& operator<<(std::ostream& os, NlCadLiftingMode mode)
102		{
103		switch(mode)
104		{
105		case NlCadLiftingMode::LAZARD: return os << "NlCadLiftingMode::LAZARD";
106		case NlCadLiftingMode::REGULAR: return os << "NlCadLiftingMode::REGULAR";
107		default: Unreachable();
108		}
109		return os;
110		}
111		NlCadLiftingMode stringToNlCadLiftingMode(const std::string& optarg)
112		{
113		if (optarg == "lazard") return NlCadLiftingMode::LAZARD;
114		else if (optarg == "regular") return NlCadLiftingMode::REGULAR;
115		else if (optarg == "help")
116		{
117		std::cerr << R"FOOBAR(
118		Modes for the CAD lifting in non-linear arithmetic.
119		Available modes for --nl-cad-lift are:
120		+ lazard
121		Lazard's lifting scheme.
122		+ regular (default)
123		Regular lifting.
124		)FOOBAR";
125		std::exit(1);
126		}
127		throw OptionException(std::string("unknown option for --nl-cad-lift: `") +
128		optarg + "'. Try --nl-cad-lift=help.");
129		}
130		std::ostream& operator<<(std::ostream& os, NlCadProjectionMode mode)
131		{
132		switch(mode)
133		{
134		case NlCadProjectionMode::MCCALLUM: return os << "NlCadProjectionMode::MCCALLUM";
135		case NlCadProjectionMode::LAZARD: return os << "NlCadProjectionMode::LAZARD";
136		case NlCadProjectionMode::LAZARDMOD: return os << "NlCadProjectionMode::LAZARDMOD";
137		default: Unreachable();
138		}
139		return os;
140		}
141		NlCadProjectionMode stringToNlCadProjectionMode(const std::string& optarg)
142		{
143		if (optarg == "mccallum") return NlCadProjectionMode::MCCALLUM;
144		else if (optarg == "lazard") return NlCadProjectionMode::LAZARD;
145		else if (optarg == "lazard-mod") return NlCadProjectionMode::LAZARDMOD;
146		else if (optarg == "help")
147		{
148		std::cerr << R"FOOBAR(
149		Modes for the CAD projection operator in non-linear arithmetic.
150		Available modes for --nl-cad-proj are:
151		+ mccallum (default)
152		McCallum's projection operator.
153		+ lazard
154		Lazard's projection operator.
155		+ lazard-mod
156		A modification of Lazard's projection operator.
157		)FOOBAR";
158		std::exit(1);
159		}
160		throw OptionException(std::string("unknown option for --nl-cad-proj: `") +
161		optarg + "'. Try --nl-cad-proj=help.");
162		}
163		std::ostream& operator<<(std::ostream& os, NlExtMode mode)
164		{
165		switch(mode)
166		{
167		case NlExtMode::NONE: return os << "NlExtMode::NONE";
168		case NlExtMode::FULL: return os << "NlExtMode::FULL";
169		case NlExtMode::LIGHT: return os << "NlExtMode::LIGHT";
170		default: Unreachable();
171		}
172		return os;
173		}
174	126	NlExtMode stringToNlExtMode(const std::string& optarg)
175		{
176	126	if (optarg == "none") return NlExtMode::NONE;
177	120	else if (optarg == "full") return NlExtMode::FULL;
178		else if (optarg == "light") return NlExtMode::LIGHT;
179		else if (optarg == "help")
180		{
181		std::cerr << R"FOOBAR(
182		Modes for the non-linear linearization
183		Available modes for --nl-ext are:
184		+ none
185		Disable linearization approach
186		+ full (default)
187		Use all lemma schemes
188		+ light
189		Only use a few light-weight lemma schemes
190		)FOOBAR";
191		std::exit(1);
192		}
193		throw OptionException(std::string("unknown option for --nl-ext: `") +
194		optarg + "'. Try --nl-ext=help.");
195		}
196		std::ostream& operator<<(std::ostream& os, NlRlvMode mode)
197		{
198		switch(mode)
199		{
200		case NlRlvMode::NONE: return os << "NlRlvMode::NONE";
201		case NlRlvMode::ALWAYS: return os << "NlRlvMode::ALWAYS";
202		case NlRlvMode::INTERLEAVE: return os << "NlRlvMode::INTERLEAVE";
203		default: Unreachable();
204		}
205		return os;
206		}
207	6	NlRlvMode stringToNlRlvMode(const std::string& optarg)
208		{
209	6	if (optarg == "none") return NlRlvMode::NONE;
210	3	else if (optarg == "always") return NlRlvMode::ALWAYS;
211		else if (optarg == "interleave") return NlRlvMode::INTERLEAVE;
212		else if (optarg == "help")
213		{
214		std::cerr << R"FOOBAR(
215		Modes for using relevance of assertions in non-linear arithmetic.
216		Available modes for --nl-rlv are:
217		+ none (default)
218		Do not use relevance.
219		+ always
220		Always use relevance.
221		+ interleave
222		Alternate rounds using relevance.
223		)FOOBAR";
224		std::exit(1);
225		}
226		throw OptionException(std::string("unknown option for --nl-rlv: `") +
227		optarg + "'. Try --nl-rlv=help.");
228		}
229		std::ostream& operator<<(std::ostream& os, ArithUnateLemmaMode mode)
230		{
231		switch(mode)
232		{
233		case ArithUnateLemmaMode::INEQUALITY: return os << "ArithUnateLemmaMode::INEQUALITY";
234		case ArithUnateLemmaMode::ALL: return os << "ArithUnateLemmaMode::ALL";
235		case ArithUnateLemmaMode::EQUALITY: return os << "ArithUnateLemmaMode::EQUALITY";
236		case ArithUnateLemmaMode::NO: return os << "ArithUnateLemmaMode::NO";
237		default: Unreachable();
238		}
239		return os;
240		}
241		ArithUnateLemmaMode stringToArithUnateLemmaMode(const std::string& optarg)
242		{
243		if (optarg == "ineqs") return ArithUnateLemmaMode::INEQUALITY;
244		else if (optarg == "all") return ArithUnateLemmaMode::ALL;
245		else if (optarg == "eqs") return ArithUnateLemmaMode::EQUALITY;
246		else if (optarg == "none") return ArithUnateLemmaMode::NO;
247		else if (optarg == "help")
248		{
249		std::cerr << R"FOOBAR(
250		Unate lemmas are generated before SAT search begins using the relationship of
251		constant terms and polynomials.
252		Available modes for --unate-lemmas are:
253		+ ineqs
254		Outputs lemmas of the general form (<= p c) implies (<= p d) for c < d.
255		+ all (default)
256		A combination of inequalities and equalities.
257		+ eqs
258		Outputs lemmas of the general forms (= p c) implies (<= p d) for c < d, or (=
259		p c) implies (not (= p d)) for c != d.
260		)FOOBAR";
261		std::exit(1);
262		}
263		throw OptionException(std::string("unknown option for --unate-lemmas: `") +
264		optarg + "'. Try --unate-lemmas=help.");
265		}
266		// clang-format on
267
268		namespace arith
269		{
270		// clang-format off
271		void setDefaultMaxApproxDepth(Options& opts, int64_t value)
272		{
273		if (!opts.arith.maxApproxDepthWasSetByUser) opts.arith.maxApproxDepth = value;
274		}
275		void setDefaultBrabTest(Options& opts, bool value)
276		{
277		if (!opts.arith.brabTestWasSetByUser) opts.arith.brabTest = value;
278		}
279		void setDefaultArithCongMan(Options& opts, bool value)
280		{
281		if (!opts.arith.arithCongManWasSetByUser) opts.arith.arithCongMan = value;
282		}
283		void setDefaultArithEqSolver(Options& opts, bool value)
284		{
285		if (!opts.arith.arithEqSolverWasSetByUser) opts.arith.arithEqSolver = value;
286		}
287		void setDefaultArithNoPartialFun(Options& opts, bool value)
288		{
289		if (!opts.arith.arithNoPartialFunWasSetByUser) opts.arith.arithNoPartialFun = value;
290		}
291		void setDefaultArithPropagationMode(Options& opts, ArithPropagationMode value)
292		{
293		if (!opts.arith.arithPropagationModeWasSetByUser) opts.arith.arithPropagationMode = value;
294		}
295		void setDefaultArithPropAsLemmaLength(Options& opts, uint64_t value)
296		{
297		if (!opts.arith.arithPropAsLemmaLengthWasSetByUser) opts.arith.arithPropAsLemmaLength = value;
298		}
299		void setDefaultArithRewriteEq(Options& opts, bool value)
300		{
301		if (!opts.arith.arithRewriteEqWasSetByUser) opts.arith.arithRewriteEq = value;
302		}
303		void setDefaultCollectPivots(Options& opts, bool value)
304		{
305		if (!opts.arith.collectPivotsWasSetByUser) opts.arith.collectPivots = value;
306		}
307		void setDefaultDoCutAllBounded(Options& opts, bool value)
308		{
309		if (!opts.arith.doCutAllBoundedWasSetByUser) opts.arith.doCutAllBounded = value;
310		}
311		void setDefaultExportDioDecompositions(Options& opts, bool value)
312		{
313		if (!opts.arith.exportDioDecompositionsWasSetByUser) opts.arith.exportDioDecompositions = value;
314		}
315		void setDefaultDioRepeat(Options& opts, bool value)
316		{
317		if (!opts.arith.dioRepeatWasSetByUser) opts.arith.dioRepeat = value;
318		}
319		void setDefaultArithDioSolver(Options& opts, bool value)
320		{
321		if (!opts.arith.arithDioSolverWasSetByUser) opts.arith.arithDioSolver = value;
322		}
323		void setDefaultDioSolverTurns(Options& opts, int64_t value)
324		{
325		if (!opts.arith.dioSolverTurnsWasSetByUser) opts.arith.dioSolverTurns = value;
326		}
327		void setDefaultArithErrorSelectionRule(Options& opts, ErrorSelectionRule value)
328		{
329		if (!opts.arith.arithErrorSelectionRuleWasSetByUser) opts.arith.arithErrorSelectionRule = value;
330		}
331		void setDefaultHavePenalties(Options& opts, bool value)
332		{
333		if (!opts.arith.havePenaltiesWasSetByUser) opts.arith.havePenalties = value;
334		}
335		void setDefaultArithHeuristicPivots(Options& opts, int64_t value)
336		{
337		if (!opts.arith.arithHeuristicPivotsWasSetByUser) opts.arith.arithHeuristicPivots = value;
338		}
339		void setDefaultReplayFailureLemma(Options& opts, bool value)
340		{
341		if (!opts.arith.replayFailureLemmaWasSetByUser) opts.arith.replayFailureLemma = value;
342		}
343		void setDefaultMaxCutsInContext(Options& opts, uint64_t value)
344		{
345		if (!opts.arith.maxCutsInContextWasSetByUser) opts.arith.maxCutsInContext = value;
346		}
347		void setDefaultArithMLTrick(Options& opts, bool value)
348		{
349		if (!opts.arith.arithMLTrickWasSetByUser) opts.arith.arithMLTrick = value;
350		}
351		void setDefaultArithMLTrickSubstitutions(Options& opts, uint64_t value)
352		{
353		if (!opts.arith.arithMLTrickSubstitutionsWasSetByUser) opts.arith.arithMLTrickSubstitutions = value;
354		}
355		void setDefaultNewProp(Options& opts, bool value)
356		{
357		if (!opts.arith.newPropWasSetByUser) opts.arith.newProp = value;
358		}
359		void setDefaultNlCad(Options& opts, bool value)
360		{
361		if (!opts.arith.nlCadWasSetByUser) opts.arith.nlCad = value;
362		}
363		void setDefaultNlCadUseInitial(Options& opts, bool value)
364		{
365		if (!opts.arith.nlCadUseInitialWasSetByUser) opts.arith.nlCadUseInitial = value;
366		}
367		void setDefaultNlCadLifting(Options& opts, NlCadLiftingMode value)
368		{
369		if (!opts.arith.nlCadLiftingWasSetByUser) opts.arith.nlCadLifting = value;
370		}
371		void setDefaultNlCadProjection(Options& opts, NlCadProjectionMode value)
372		{
373		if (!opts.arith.nlCadProjectionWasSetByUser) opts.arith.nlCadProjection = value;
374		}
375		void setDefaultNlExt(Options& opts, NlExtMode value)
376		{
377		if (!opts.arith.nlExtWasSetByUser) opts.arith.nlExt = value;
378		}
379		void setDefaultNlExtEntailConflicts(Options& opts, bool value)
380		{
381		if (!opts.arith.nlExtEntailConflictsWasSetByUser) opts.arith.nlExtEntailConflicts = value;
382		}
383		void setDefaultNlExtFactor(Options& opts, bool value)
384		{
385		if (!opts.arith.nlExtFactorWasSetByUser) opts.arith.nlExtFactor = value;
386		}
387		void setDefaultNlExtIncPrecision(Options& opts, bool value)
388		{
389		if (!opts.arith.nlExtIncPrecisionWasSetByUser) opts.arith.nlExtIncPrecision = value;
390		}
391		void setDefaultNlExtPurify(Options& opts, bool value)
392		{
393		if (!opts.arith.nlExtPurifyWasSetByUser) opts.arith.nlExtPurify = value;
394		}
395		void setDefaultNlExtResBound(Options& opts, bool value)
396		{
397		if (!opts.arith.nlExtResBoundWasSetByUser) opts.arith.nlExtResBound = value;
398		}
399		void setDefaultNlExtRewrites(Options& opts, bool value)
400		{
401		if (!opts.arith.nlExtRewritesWasSetByUser) opts.arith.nlExtRewrites = value;
402		}
403		void setDefaultNlExtSplitZero(Options& opts, bool value)
404		{
405		if (!opts.arith.nlExtSplitZeroWasSetByUser) opts.arith.nlExtSplitZero = value;
406		}
407		void setDefaultNlExtTfTaylorDegree(Options& opts, int64_t value)
408		{
409		if (!opts.arith.nlExtTfTaylorDegreeWasSetByUser) opts.arith.nlExtTfTaylorDegree = value;
410		}
411		void setDefaultNlExtTfTangentPlanes(Options& opts, bool value)
412		{
413		if (!opts.arith.nlExtTfTangentPlanesWasSetByUser) opts.arith.nlExtTfTangentPlanes = value;
414		}
415		void setDefaultNlExtTangentPlanes(Options& opts, bool value)
416		{
417		if (!opts.arith.nlExtTangentPlanesWasSetByUser) opts.arith.nlExtTangentPlanes = value;
418		}
419		void setDefaultNlExtTangentPlanesInterleave(Options& opts, bool value)
420		{
421		if (!opts.arith.nlExtTangentPlanesInterleaveWasSetByUser) opts.arith.nlExtTangentPlanesInterleave = value;
422		}
423		void setDefaultNlICP(Options& opts, bool value)
424		{
425		if (!opts.arith.nlICPWasSetByUser) opts.arith.nlICP = value;
426		}
427		void setDefaultNlRlvMode(Options& opts, NlRlvMode value)
428		{
429		if (!opts.arith.nlRlvModeWasSetByUser) opts.arith.nlRlvMode = value;
430		}
431		void setDefaultNlRlvAssertBounds(Options& opts, bool value)
432		{
433		if (!opts.arith.nlRlvAssertBoundsWasSetByUser) opts.arith.nlRlvAssertBounds = value;
434		}
435		void setDefaultPbRewrites(Options& opts, bool value)
436		{
437		if (!opts.arith.pbRewritesWasSetByUser) opts.arith.pbRewrites = value;
438		}
439		void setDefaultArithPivotThreshold(Options& opts, uint64_t value)
440		{
441		if (!opts.arith.arithPivotThresholdWasSetByUser) opts.arith.arithPivotThreshold = value;
442		}
443		void setDefaultPpAssertMaxSubSize(Options& opts, uint64_t value)
444		{
445		if (!opts.arith.ppAssertMaxSubSizeWasSetByUser) opts.arith.ppAssertMaxSubSize = value;
446		}
447		void setDefaultArithPropagateMaxLength(Options& opts, uint64_t value)
448		{
449		if (!opts.arith.arithPropagateMaxLengthWasSetByUser) opts.arith.arithPropagateMaxLength = value;
450		}
451		void setDefaultReplayEarlyCloseDepths(Options& opts, int64_t value)
452		{
453		if (!opts.arith.replayEarlyCloseDepthsWasSetByUser) opts.arith.replayEarlyCloseDepths = value;
454		}
455		void setDefaultReplayFailurePenalty(Options& opts, int64_t value)
456		{
457		if (!opts.arith.replayFailurePenaltyWasSetByUser) opts.arith.replayFailurePenalty = value;
458		}
459		void setDefaultLemmaRejectCutSize(Options& opts, uint64_t value)
460		{
461		if (!opts.arith.lemmaRejectCutSizeWasSetByUser) opts.arith.lemmaRejectCutSize = value;
462		}
463		void setDefaultReplayNumericFailurePenalty(Options& opts, int64_t value)
464		{
465		if (!opts.arith.replayNumericFailurePenaltyWasSetByUser) opts.arith.replayNumericFailurePenalty = value;
466		}
467		void setDefaultReplayRejectCutSize(Options& opts, uint64_t value)
468		{
469		if (!opts.arith.replayRejectCutSizeWasSetByUser) opts.arith.replayRejectCutSize = value;
470		}
471		void setDefaultSoiApproxMajorFailure(Options& opts, double value)
472		{
473		if (!opts.arith.soiApproxMajorFailureWasSetByUser) opts.arith.soiApproxMajorFailure = value;
474		}
475		void setDefaultSoiApproxMajorFailurePen(Options& opts, int64_t value)
476		{
477		if (!opts.arith.soiApproxMajorFailurePenWasSetByUser) opts.arith.soiApproxMajorFailurePen = value;
478		}
479		void setDefaultSoiApproxMinorFailure(Options& opts, double value)
480		{
481		if (!opts.arith.soiApproxMinorFailureWasSetByUser) opts.arith.soiApproxMinorFailure = value;
482		}
483		void setDefaultSoiApproxMinorFailurePen(Options& opts, int64_t value)
484		{
485		if (!opts.arith.soiApproxMinorFailurePenWasSetByUser) opts.arith.soiApproxMinorFailurePen = value;
486		}
487		void setDefaultRestrictedPivots(Options& opts, bool value)
488		{
489		if (!opts.arith.restrictedPivotsWasSetByUser) opts.arith.restrictedPivots = value;
490		}
491		void setDefaultRevertArithModels(Options& opts, bool value)
492		{
493		if (!opts.arith.revertArithModelsWasSetByUser) opts.arith.revertArithModels = value;
494		}
495		void setDefaultRrTurns(Options& opts, int64_t value)
496		{
497		if (!opts.arith.rrTurnsWasSetByUser) opts.arith.rrTurns = value;
498		}
499		void setDefaultTrySolveIntStandardEffort(Options& opts, bool value)
500		{
501		if (!opts.arith.trySolveIntStandardEffortWasSetByUser) opts.arith.trySolveIntStandardEffort = value;
502		}
503		void setDefaultArithSimplexCheckPeriod(Options& opts, uint64_t value)
504		{
505		if (!opts.arith.arithSimplexCheckPeriodWasSetByUser) opts.arith.arithSimplexCheckPeriod = value;
506		}
507		void setDefaultSoiQuickExplain(Options& opts, bool value)
508		{
509		if (!opts.arith.soiQuickExplainWasSetByUser) opts.arith.soiQuickExplain = value;
510		}
511		void setDefaultArithStandardCheckVarOrderPivots(Options& opts, int64_t value)
512		{
513		if (!opts.arith.arithStandardCheckVarOrderPivotsWasSetByUser) opts.arith.arithStandardCheckVarOrderPivots = value;
514		}
515		void setDefaultArithUnateLemmaMode(Options& opts, ArithUnateLemmaMode value)
516		{
517		if (!opts.arith.arithUnateLemmaModeWasSetByUser) opts.arith.arithUnateLemmaMode = value;
518		}
519		void setDefaultUseApprox(Options& opts, bool value)
520		{
521		if (!opts.arith.useApproxWasSetByUser) opts.arith.useApprox = value;
522		}
523		void setDefaultUseFC(Options& opts, bool value)
524		{
525		if (!opts.arith.useFCWasSetByUser) opts.arith.useFC = value;
526		}
527		void setDefaultUseSOI(Options& opts, bool value)
528		{
529		if (!opts.arith.useSOIWasSetByUser) opts.arith.useSOI = value;
530		}
531		// clang-format on
532		}
533
534	29577	} // namespace cvc5::options