Head

GCC Code Coverage Report
Directory:	.		Exec	Total	Coverage
File:	build-coverage/src/options/smt_options.cpp	Lines:	57	415	13.7 %
Date:	2021-09-07	Branches:	37	333	11.1 %

/******************************************************************************
 * 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/smt_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, BlockModelsMode mode)
{
  switch(mode) {
    case BlockModelsMode::VALUES:
      return os << "BlockModelsMode::VALUES";
    case BlockModelsMode::LITERALS:
      return os << "BlockModelsMode::LITERALS";
    case BlockModelsMode::NONE:
      return os << "BlockModelsMode::NONE";
    default:
      Unreachable();
  }
  return os;
}
BlockModelsMode stringToBlockModelsMode(const std::string& optarg)
{
  if (optarg == "values")
  {
    return BlockModelsMode::VALUES;
  }
  else if (optarg == "literals")
  {
    return BlockModelsMode::LITERALS;
  }
  else if (optarg == "none")
  {
    return BlockModelsMode::NONE;
  }
  else if (optarg == "help")
  {
    std::cerr << "Blocking models modes.\n"
         "Available modes for --block-models are:\n"
         "+ values\n"
         "  Block models based on the concrete model values for the free variables.\n"
         "+ literals\n"
         "  Block models based on the SAT skeleton.\n"
         "+ none (default)\n"
         "  Do not block models.\n";
    std::exit(1);
  }
  throw OptionException(std::string("unknown option for --block-models: `") +
                        optarg + "'.  Try --block-models=help.");
}
std::ostream& operator<<(std::ostream& os, IandMode mode)
{
  switch(mode) {
    case IandMode::BITWISE:
      return os << "IandMode::BITWISE";
    case IandMode::VALUE:
      return os << "IandMode::VALUE";
    case IandMode::SUM:
      return os << "IandMode::SUM";
    default:
      Unreachable();
  }
  return os;
}
IandMode stringToIandMode(const std::string& optarg)
{
  if (optarg == "bitwise")
  {
    return IandMode::BITWISE;
  }
  else if (optarg == "value")
  {
    return IandMode::VALUE;
  }
  else if (optarg == "sum")
  {
    return IandMode::SUM;
  }
  else if (optarg == "help")
  {
    std::cerr << "Refinement modes for integer AND\n"
         "Available modes for --iand-mode are:\n"
         "+ bitwise\n"
         "  use bitwise comparisons on binary representation of integer for refinement\n"
         "  (experimental)\n"
         "+ value (default)\n"
         "  value-based refinement\n"
         "+ sum\n"
         "  use sum to represent integer AND in refinement\n";
    std::exit(1);
  }
  throw OptionException(std::string("unknown option for --iand-mode: `") +
                        optarg + "'.  Try --iand-mode=help.");
}
std::ostream& operator<<(std::ostream& os, ModelCoresMode mode)
{
  switch(mode) {
    case ModelCoresMode::NON_IMPLIED:
      return os << "ModelCoresMode::NON_IMPLIED";
    case ModelCoresMode::SIMPLE:
      return os << "ModelCoresMode::SIMPLE";
    case ModelCoresMode::NONE:
      return os << "ModelCoresMode::NONE";
    default:
      Unreachable();
  }
  return os;
}
ModelCoresMode stringToModelCoresMode(const std::string& optarg)
{
  if (optarg == "non-implied")
  {
    return ModelCoresMode::NON_IMPLIED;
  }
  else if (optarg == "simple")
  {
    return ModelCoresMode::SIMPLE;
  }
  else if (optarg == "none")
  {
    return ModelCoresMode::NONE;
  }
  else if (optarg == "help")
  {
    std::cerr << "Model cores modes.\n"
         "Available modes for --model-cores are:\n"
         "+ non-implied\n"
         "  Only include a subset of variables whose values, in addition to the values of\n"
         "  variables whose values are implied, are sufficient to show the input formula\n"
         "  is satisfied by the given model.\n"
         "+ simple\n"
         "  Only include a subset of variables whose values are sufficient to show the\n"
         "  input formula is satisfied by the given model.\n"
         "+ none (default)\n"
         "  Do not compute model cores.\n";
    std::exit(1);
  }
  throw OptionException(std::string("unknown option for --model-cores: `") +
                        optarg + "'.  Try --model-cores=help.");
}
std::ostream& operator<<(std::ostream& os, ModelUninterpPrintMode mode)
{
  switch(mode) {
    case ModelUninterpPrintMode::DeclSortAndFun:
      return os << "ModelUninterpPrintMode::DeclSortAndFun";
    case ModelUninterpPrintMode::None:
      return os << "ModelUninterpPrintMode::None";
    case ModelUninterpPrintMode::DeclFun:
      return os << "ModelUninterpPrintMode::DeclFun";
    default:
      Unreachable();
  }
  return os;
}
ModelUninterpPrintMode stringToModelUninterpPrintMode(const std::string& optarg)
{
  if (optarg == "decl-sort-and-fun")
  {
    return ModelUninterpPrintMode::DeclSortAndFun;
  }
  else if (optarg == "none")
  {
    return ModelUninterpPrintMode::None;
  }
  else if (optarg == "decl-fun")
  {
    return ModelUninterpPrintMode::DeclFun;
  }
  else if (optarg == "help")
  {
    std::cerr << "uninterpreted elements in models printing modes.\n"
         "Available modes for --model-u-print are:\n"
         "+ decl-sort-and-fun\n"
         "  print uninterpreted elements declare-fun, and also include a declare-sort for\n"
         "  the sort\n"
         "+ none (default)\n"
         "  (default) do not print declarations of uninterpreted elements in models.\n"
         "+ decl-fun\n"
         "  print uninterpreted elements declare-fun, but don't include a declare-sort for\n"
         "  the sort\n";
    std::exit(1);
  }
  throw OptionException(std::string("unknown option for --model-u-print: `") +
                        optarg + "'.  Try --model-u-print=help.");
}
std::ostream& operator<<(std::ostream& os, ProduceInterpols mode)
{
  switch(mode) {
    case ProduceInterpols::CONJECTURE:
      return os << "ProduceInterpols::CONJECTURE";
    case ProduceInterpols::SHARED:
      return os << "ProduceInterpols::SHARED";
    case ProduceInterpols::NONE:
      return os << "ProduceInterpols::NONE";
    case ProduceInterpols::ALL:
      return os << "ProduceInterpols::ALL";
    case ProduceInterpols::ASSUMPTIONS:
      return os << "ProduceInterpols::ASSUMPTIONS";
    case ProduceInterpols::DEFAULT:
      return os << "ProduceInterpols::DEFAULT";
    default:
      Unreachable();
  }
  return os;
}
ProduceInterpols stringToProduceInterpols(const std::string& optarg)
{
  if (optarg == "conjecture")
  {
    return ProduceInterpols::CONJECTURE;
  }
  else if (optarg == "shared")
  {
    return ProduceInterpols::SHARED;
  }
  else if (optarg == "none")
  {
    return ProduceInterpols::NONE;
  }
  else if (optarg == "all")
  {
    return ProduceInterpols::ALL;
  }
  else if (optarg == "assumptions")
  {
    return ProduceInterpols::ASSUMPTIONS;
  }
  else if (optarg == "default")
  {
    return ProduceInterpols::DEFAULT;
  }
  else if (optarg == "help")
  {
    std::cerr << "Interpolants grammar mode\n"
         "Available modes for --produce-interpols are:\n"
         "+ conjecture\n"
         "  use only operators that occur in the conjecture\n"
         "+ shared\n"
         "  use only operators that occur both in the assumptions and the conjecture\n"
         "+ none (default)\n"
         "  don't compute interpolants\n"
         "+ all\n"
         "  use only operators that occur either in the assumptions or the conjecture\n"
         "+ assumptions\n"
         "  use only operators that occur in the assumptions\n"
         "+ default\n"
         "  use the default grammar for the theory or the user-defined grammar if given\n";
    std::exit(1);
  }
  throw OptionException(std::string("unknown option for --produce-interpols: `") +
                        optarg + "'.  Try --produce-interpols=help.");
}
std::ostream& operator<<(std::ostream& os, SimplificationMode mode)
{
  switch(mode) {
    case SimplificationMode::BATCH:
      return os << "SimplificationMode::BATCH";
    case SimplificationMode::NONE:
      return os << "SimplificationMode::NONE";
    default:
      Unreachable();
  }
  return os;
}
SimplificationMode stringToSimplificationMode(const std::string& optarg)
{
  if (optarg == "batch")
  {
    return SimplificationMode::BATCH;
  }
  else if (optarg == "none")
  {
    return SimplificationMode::NONE;
  }
  else if (optarg == "help")
  {
    std::cerr << "Simplification modes.\n"
         "Available modes for --simplification are:\n"
         "+ batch (default)\n"
         "  Save up all ASSERTions; run nonclausal simplification and clausal (MiniSat)\n"
         "  propagation for all of them only after reaching a querying command (CHECKSAT\n"
         "  or QUERY or predicate SUBTYPE declaration).\n"
         "+ none\n"
         "  Do not perform nonclausal simplification.\n";
    std::exit(1);
  }
  throw OptionException(std::string("unknown option for --simplification: `") +
                        optarg + "'.  Try --simplification=help.");
}
std::ostream& operator<<(std::ostream& os, SolveBVAsIntMode mode)
{
  switch(mode) {
    case SolveBVAsIntMode::IAND:
      return os << "SolveBVAsIntMode::IAND";
    case SolveBVAsIntMode::OFF:
      return os << "SolveBVAsIntMode::OFF";
    case SolveBVAsIntMode::BV:
      return os << "SolveBVAsIntMode::BV";
    case SolveBVAsIntMode::SUM:
      return os << "SolveBVAsIntMode::SUM";
    default:
      Unreachable();
  }
  return os;
}
SolveBVAsIntMode stringToSolveBVAsIntMode(const std::string& optarg)
{
  if (optarg == "iand")
  {
    return SolveBVAsIntMode::IAND;
  }
  else if (optarg == "off")
  {
    return SolveBVAsIntMode::OFF;
  }
  else if (optarg == "bv")
  {
    return SolveBVAsIntMode::BV;
  }
  else if (optarg == "sum")
  {
    return SolveBVAsIntMode::SUM;
  }
  else if (optarg == "help")
  {
    std::cerr << "solve-bv-as-int modes.\n"
         "Available modes for --solve-bv-as-int are:\n"
         "+ iand\n"
         "  Translate bvand to the iand operator (experimental)\n"
         "+ off (default)\n"
         "  Do not translate bit-vectors to integers\n"
         "+ bv\n"
         "  Translate bvand back to bit-vectors\n"
         "+ sum\n"
         "  Generate a sum expression for each bvand instance, based on the value in\n"
         "  --solbv-bv-as-int-granularity\n";
    std::exit(1);
  }
  throw OptionException(std::string("unknown option for --solve-bv-as-int: `") +
                        optarg + "'.  Try --solve-bv-as-int=help.");
}
std::ostream& operator<<(std::ostream& os, SygusSolutionOutMode mode)
{
  switch(mode) {
    case SygusSolutionOutMode::STATUS_AND_DEF:
      return os << "SygusSolutionOutMode::STATUS_AND_DEF";
    case SygusSolutionOutMode::STATUS:
      return os << "SygusSolutionOutMode::STATUS";
    case SygusSolutionOutMode::STANDARD:
      return os << "SygusSolutionOutMode::STANDARD";
    case SygusSolutionOutMode::STATUS_OR_DEF:
      return os << "SygusSolutionOutMode::STATUS_OR_DEF";
    default:
      Unreachable();
  }
  return os;
}
SygusSolutionOutMode stringToSygusSolutionOutMode(const std::string& optarg)
{
  if (optarg == "status-and-def")
  {
    return SygusSolutionOutMode::STATUS_AND_DEF;
  }
  else if (optarg == "status")
  {
    return SygusSolutionOutMode::STATUS;
  }
  else if (optarg == "sygus-standard")
  {
    return SygusSolutionOutMode::STANDARD;
  }
  else if (optarg == "status-or-def")
  {
    return SygusSolutionOutMode::STATUS_OR_DEF;
  }
  else if (optarg == "help")
  {
    std::cerr << "Modes for sygus solution output.\n"
         "Available modes for --sygus-out are:\n"
         "+ status-and-def\n"
         "  Print status followed by definition corresponding to solution.\n"
         "+ status\n"
         "  Print only status for check-synth calls.\n"
         "+ sygus-standard (default)\n"
         "  Print based on SyGuS standard.\n"
         "+ status-or-def\n"
         "  Print status if infeasible, or definition corresponding to solution if\n"
         "  feasible.\n";
    std::exit(1);
  }
  throw OptionException(std::string("unknown option for --sygus-out: `") +
                        optarg + "'.  Try --sygus-out=help.");
}
std::ostream& operator<<(std::ostream& os, UnsatCoresMode mode)
{
  switch(mode) {
    case UnsatCoresMode::FULL_PROOF:
      return os << "UnsatCoresMode::FULL_PROOF";
    case UnsatCoresMode::OFF:
      return os << "UnsatCoresMode::OFF";
    case UnsatCoresMode::SAT_PROOF:
      return os << "UnsatCoresMode::SAT_PROOF";
    case UnsatCoresMode::ASSUMPTIONS:
      return os << "UnsatCoresMode::ASSUMPTIONS";
    default:
      Unreachable();
  }
  return os;
}
UnsatCoresMode stringToUnsatCoresMode(const std::string& optarg)
{
  if (optarg == "full-proof")
  {
    return UnsatCoresMode::FULL_PROOF;
  }
  else if (optarg == "off")
  {
    return UnsatCoresMode::OFF;
  }
  else if (optarg == "sat-proof")
  {
    return UnsatCoresMode::SAT_PROOF;
  }
  else if (optarg == "assumptions")
  {
    return UnsatCoresMode::ASSUMPTIONS;
  }
  else if (optarg == "help")
  {
    std::cerr << "unsat cores modes.\n"
         "Available modes for --unsat-cores-mode are:\n"
         "+ full-proof\n"
         "  Produce unsat cores from full proofs.\n"
         "+ off (default)\n"
         "  Do not produce unsat cores.\n"
         "+ sat-proof\n"
         "  Produce unsat cores from SAT and preprocessing proofs.\n"
         "+ assumptions\n"
         "  Produce unsat cores using solving under assumptions and preprocessing proofs.\n";
    std::exit(1);
  }
  throw OptionException(std::string("unknown option for --unsat-cores-mode: `") +
                        optarg + "'.  Try --unsat-cores-mode=help.");
}

namespace smt
{
// clang-format off
void setDefaultAbstractValues(Options& opts, bool value)
{
    if (!opts.smt.abstractValuesWasSetByUser) {
        opts.smt.abstractValues = value;
    }
}
void setDefaultAckermann(Options& opts, bool value)
{
    if (!opts.smt.ackermannWasSetByUser) {
        opts.smt.ackermann = value;
    }
}
void setDefaultBlockModelsMode(Options& opts, BlockModelsMode value)
{
    if (!opts.smt.blockModelsModeWasSetByUser) {
        opts.smt.blockModelsMode = value;
    }
}
void setDefaultBVAndIntegerGranularity(Options& opts, uint64_t value)
{
    if (!opts.smt.BVAndIntegerGranularityWasSetByUser) {
        opts.smt.BVAndIntegerGranularity = value;
    }
}
void setDefaultCheckAbducts(Options& opts, bool value)
{
    if (!opts.smt.checkAbductsWasSetByUser) {
        opts.smt.checkAbducts = value;
    }
}
void setDefaultCheckInterpols(Options& opts, bool value)
{
    if (!opts.smt.checkInterpolsWasSetByUser) {
        opts.smt.checkInterpols = value;
    }
}
void setDefaultCheckModels(Options& opts, bool value)
{
    if (!opts.smt.checkModelsWasSetByUser) {
        opts.smt.checkModels = value;
    }
}
void setDefaultCheckProofs(Options& opts, bool value)
{
    if (!opts.smt.checkProofsWasSetByUser) {
        opts.smt.checkProofs = value;
    }
}
void setDefaultCheckSynthSol(Options& opts, bool value)
{
    if (!opts.smt.checkSynthSolWasSetByUser) {
        opts.smt.checkSynthSol = value;
    }
}
void setDefaultCheckUnsatCores(Options& opts, bool value)
{
    if (!opts.smt.checkUnsatCoresWasSetByUser) {
        opts.smt.checkUnsatCores = value;
    }
}
void setDefaultDebugCheckModels(Options& opts, bool value)
{
    if (!opts.smt.debugCheckModelsWasSetByUser) {
        opts.smt.debugCheckModels = value;
    }
}
void setDefaultDumpToFileName(Options& opts, ManagedOut value)
{
    if (!opts.smt.dumpToFileNameWasSetByUser) {
        opts.smt.dumpToFileName = value;
    }
}
void setDefaultDumpModeString(Options& opts, std::string value)
{
    if (!opts.smt.dumpModeStringWasSetByUser) {
        opts.smt.dumpModeString = value;
    }
}
void setDefaultEarlyIteRemoval(Options& opts, bool value)
{
    if (!opts.smt.earlyIteRemovalWasSetByUser) {
        opts.smt.earlyIteRemoval = value;
    }
}
void setDefaultExpandDefinitions(Options& opts, bool value)
{
    if (!opts.smt.expandDefinitionsWasSetByUser) {
        opts.smt.expandDefinitions = value;
    }
}
void setDefaultExtRewPrep(Options& opts, bool value)
{
    if (!opts.smt.extRewPrepWasSetByUser) {
        opts.smt.extRewPrep = value;
    }
}
void setDefaultExtRewPrepAgg(Options& opts, bool value)
{
    if (!opts.smt.extRewPrepAggWasSetByUser) {
        opts.smt.extRewPrepAgg = value;
    }
}
void setDefaultForeignTheoryRewrite(Options& opts, bool value)
{
    if (!opts.smt.foreignTheoryRewriteWasSetByUser) {
        opts.smt.foreignTheoryRewrite = value;
    }
}
void setDefaultIandMode(Options& opts, IandMode value)
{
    if (!opts.smt.iandModeWasSetByUser) {
        opts.smt.iandMode = value;
    }
}
void setDefaultInteractiveMode(Options& opts, bool value)
{
    if (!opts.smt.interactiveModeWasSetByUser) {
        opts.smt.interactiveMode = value;
    }
}
void setDefaultDoITESimp(Options& opts, bool value)
{
    if (!opts.smt.doITESimpWasSetByUser) {
        opts.smt.doITESimp = value;
    }
}
void setDefaultLearnedRewrite(Options& opts, bool value)
{
    if (!opts.smt.learnedRewriteWasSetByUser) {
        opts.smt.learnedRewrite = value;
    }
}
void setDefaultMinimalUnsatCores(Options& opts, bool value)
{
    if (!opts.smt.minimalUnsatCoresWasSetByUser) {
        opts.smt.minimalUnsatCores = value;
    }
}
void setDefaultModelCoresMode(Options& opts, ModelCoresMode value)
{
    if (!opts.smt.modelCoresModeWasSetByUser) {
        opts.smt.modelCoresMode = value;
    }
}
void setDefaultModelUninterpPrint(Options& opts, ModelUninterpPrintMode value)
{
    if (!opts.smt.modelUninterpPrintWasSetByUser) {
        opts.smt.modelUninterpPrint = value;
    }
}
void setDefaultModelWitnessValue(Options& opts, bool value)
{
    if (!opts.smt.modelWitnessValueWasSetByUser) {
        opts.smt.modelWitnessValue = value;
    }
}
void setDefaultDoITESimpOnRepeat(Options& opts, bool value)
{
    if (!opts.smt.doITESimpOnRepeatWasSetByUser) {
        opts.smt.doITESimpOnRepeat = value;
    }
}
void setDefaultProduceAbducts(Options& opts, bool value)
{
    if (!opts.smt.produceAbductsWasSetByUser) {
        opts.smt.produceAbducts = value;
    }
}
void setDefaultProduceAssertions(Options& opts, bool value)
{
    if (!opts.smt.produceAssertionsWasSetByUser) {
        opts.smt.produceAssertions = value;
    }
}
void setDefaultProduceAssignments(Options& opts, bool value)
{
    if (!opts.smt.produceAssignmentsWasSetByUser) {
        opts.smt.produceAssignments = value;
    }
}
void setDefaultProduceInterpols(Options& opts, ProduceInterpols value)
{
    if (!opts.smt.produceInterpolsWasSetByUser) {
        opts.smt.produceInterpols = value;
    }
}
void setDefaultProduceModels(Options& opts, bool value)
{
    if (!opts.smt.produceModelsWasSetByUser) {
        opts.smt.produceModels = value;
    }
}
void setDefaultProduceProofs(Options& opts, bool value)
{
    if (!opts.smt.produceProofsWasSetByUser) {
        opts.smt.produceProofs = value;
    }
}
void setDefaultUnsatAssumptions(Options& opts, bool value)
{
    if (!opts.smt.unsatAssumptionsWasSetByUser) {
        opts.smt.unsatAssumptions = value;
    }
}
void setDefaultUnsatCores(Options& opts, bool value)
{
    if (!opts.smt.unsatCoresWasSetByUser) {
        opts.smt.unsatCores = value;
    }
}
void setDefaultRepeatSimp(Options& opts, bool value)
{
    if (!opts.smt.repeatSimpWasSetByUser) {
        opts.smt.repeatSimp = value;
    }
}
void setDefaultCompressItes(Options& opts, bool value)
{
    if (!opts.smt.compressItesWasSetByUser) {
        opts.smt.compressItes = value;
    }
}
void setDefaultZombieHuntThreshold(Options& opts, uint64_t value)
{
    if (!opts.smt.zombieHuntThresholdWasSetByUser) {
        opts.smt.zombieHuntThreshold = value;
    }
}
void setDefaultSimplifyWithCareEnabled(Options& opts, bool value)
{
    if (!opts.smt.simplifyWithCareEnabledWasSetByUser) {
        opts.smt.simplifyWithCareEnabled = value;
    }
}
void setDefaultSimplificationMode(Options& opts, SimplificationMode value)
{
    if (!opts.smt.simplificationModeWasSetByUser) {
        opts.smt.simplificationMode = value;
    }
}
void setDefaultSolveBVAsInt(Options& opts, SolveBVAsIntMode value)
{
    if (!opts.smt.solveBVAsIntWasSetByUser) {
        opts.smt.solveBVAsInt = value;
    }
}
void setDefaultSolveIntAsBV(Options& opts, uint64_t value)
{
    if (!opts.smt.solveIntAsBVWasSetByUser) {
        opts.smt.solveIntAsBV = value;
    }
}
void setDefaultSolveRealAsInt(Options& opts, bool value)
{
    if (!opts.smt.solveRealAsIntWasSetByUser) {
        opts.smt.solveRealAsInt = value;
    }
}
void setDefaultSortInference(Options& opts, bool value)
{
    if (!opts.smt.sortInferenceWasSetByUser) {
        opts.smt.sortInference = value;
    }
}
void setDefaultDoStaticLearning(Options& opts, bool value)
{
    if (!opts.smt.doStaticLearningWasSetByUser) {
        opts.smt.doStaticLearning = value;
    }
}
void setDefaultSygusOut(Options& opts, SygusSolutionOutMode value)
{
    if (!opts.smt.sygusOutWasSetByUser) {
        opts.smt.sygusOut = value;
    }
}
void setDefaultSygusPrintCallbacks(Options& opts, bool value)
{
    if (!opts.smt.sygusPrintCallbacksWasSetByUser) {
        opts.smt.sygusPrintCallbacks = value;
    }
}
void setDefaultUnconstrainedSimp(Options& opts, bool value)
{
    if (!opts.smt.unconstrainedSimpWasSetByUser) {
        opts.smt.unconstrainedSimp = value;
    }
}
void setDefaultUnsatCoresMode(Options& opts, UnsatCoresMode value)
{
    if (!opts.smt.unsatCoresModeWasSetByUser) {
        opts.smt.unsatCoresMode = value;
    }
}
// clang-format on
}

}  // namespace cvc5::options
// clang-format on

Generated by: GCOVR (Version 3.2)