Head

GCC Code Coverage Report
Directory:	.		Exec	Total	Coverage
File:	build-coverage/src/options/arith_options.cpp	Lines:	13	419	3.1 %
Date:	2021-09-07	Branches:	10	306	3.3 %

/******************************************************************************
 * 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"

// clang-format off
namespace cvc5::options {

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

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 setDefaultArithPropAsLemmaLength(Options& opts, uint64_t value)
{
    if (!opts.arith.arithPropAsLemmaLengthWasSetByUser) {
        opts.arith.arithPropAsLemmaLength = value;
    }
}
void setDefaultArithPropagationMode(Options& opts, ArithPropagationMode value)
{
    if (!opts.arith.arithPropagationModeWasSetByUser) {
        opts.arith.arithPropagationMode = 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 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 setDefaultNlExt(Options& opts, NlExtMode value)
{
    if (!opts.arith.nlExtWasSetByUser) {
        opts.arith.nlExt = 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 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 setDefaultSoiApproxMajorFailurePen(Options& opts, int64_t value)
{
    if (!opts.arith.soiApproxMajorFailurePenWasSetByUser) {
        opts.arith.soiApproxMajorFailurePen = value;
    }
}
void setDefaultSoiApproxMajorFailure(Options& opts, double value)
{
    if (!opts.arith.soiApproxMajorFailureWasSetByUser) {
        opts.arith.soiApproxMajorFailure = value;
    }
}
void setDefaultSoiApproxMinorFailurePen(Options& opts, int64_t value)
{
    if (!opts.arith.soiApproxMinorFailurePenWasSetByUser) {
        opts.arith.soiApproxMinorFailurePen = value;
    }
}
void setDefaultSoiApproxMinorFailure(Options& opts, double value)
{
    if (!opts.arith.soiApproxMinorFailureWasSetByUser) {
        opts.arith.soiApproxMinorFailure = 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
// clang-format on

Generated by: GCOVR (Version 3.2)