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

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

#define CVC5__OPTIONS__SMT_H

#include "options/options.h"

// clang-format off

// clang-format on

namespace cvc5 {

namespace options {

// clang-format off

enum class BlockModelsMode

{

  NONE,

  LITERALS,

  VALUES

};

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

BlockModelsMode stringToBlockModelsMode(const std::string& optarg);

enum class IandMode

{

  BITWISE,

  SUM,

  VALUE

};

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

IandMode stringToIandMode(const std::string& optarg);

enum class ModelCoresMode

{

  NONE,

  NON_IMPLIED,

  SIMPLE

};

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

ModelCoresMode stringToModelCoresMode(const std::string& optarg);

enum class ModelUninterpPrintMode

{

  DeclFun,

  DtEnum,

  None,

  DeclSortAndFun

};

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

ModelUninterpPrintMode stringToModelUninterpPrintMode(const std::string& optarg);

enum class ProduceInterpols

{

  NONE,

  CONJECTURE,

  DEFAULT,

  ASSUMPTIONS,

  ALL,

  SHARED

};

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

ProduceInterpols stringToProduceInterpols(const std::string& optarg);

enum class SimplificationMode

{

  NONE,

  BATCH

};

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

SimplificationMode stringToSimplificationMode(const std::string& optarg);

enum class SolveBVAsIntMode

{

  IAND,

  SUM,

  BV,

  OFF

};

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

SolveBVAsIntMode stringToSolveBVAsIntMode(const std::string& optarg);

enum class SygusSolutionOutMode

{

  STATUS_OR_DEF,

  STATUS_AND_DEF,

  STANDARD,

  STATUS

};

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

SygusSolutionOutMode stringToSygusSolutionOutMode(const std::string& optarg);

enum class UnsatCoresMode

{

  ASSUMPTIONS,

  SAT_PROOF,

  FULL_PROOF,

  OFF

};

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

UnsatCoresMode stringToUnsatCoresMode(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

  bool abstractValues = false;\

  bool abstractValues__setByUser__ = false;

  bool ackermann = false;\

  bool ackermann__setByUser__ = false;

  BlockModelsMode blockModelsMode = BlockModelsMode::NONE;\

  bool blockModelsMode__setByUser__ = false;

  uint32_t BVAndIntegerGranularity = 1;\

  bool BVAndIntegerGranularity__setByUser__ = false;

  bool checkAbducts = false;\

  bool checkAbducts__setByUser__ = false;

  bool checkInterpols = false;\

  bool checkInterpols__setByUser__ = false;

  bool checkModels;\

  bool checkModels__setByUser__ = false;

  bool checkProofs;\

  bool checkProofs__setByUser__ = false;

  bool checkSynthSol = false;\

  bool checkSynthSol__setByUser__ = false;

  bool checkUnsatCores;\

  bool checkUnsatCores__setByUser__ = false;

  bool debugCheckModels;\

  bool debugCheckModels__setByUser__ = false;

  std::string diagnosticChannelName;\

  bool diagnosticChannelName__setByUser__ = false;

  bool dumpInstantiations = false;\

  bool dumpInstantiations__setByUser__ = false;

  bool dumpModels = false;\

  bool dumpModels__setByUser__ = false;

  bool dumpProofs = false;\

  bool dumpProofs__setByUser__ = false;

  std::string dumpToFileName;\

  bool dumpToFileName__setByUser__ = false;

  bool dumpUnsatCores = false;\

  bool dumpUnsatCores__setByUser__ = false;

  bool dumpUnsatCoresFull = false;\

  bool dumpUnsatCoresFull__setByUser__ = false;

  std::string dumpModeString;\

  bool dumpModeString__setByUser__ = false;

  bool earlyIteRemoval = false;\

  bool earlyIteRemoval__setByUser__ = false;

  bool expandDefinitions = false;\

  bool expandDefinitions__setByUser__ = false;

  bool extRewPrep = false;\

  bool extRewPrep__setByUser__ = false;

  bool extRewPrepAgg = false;\

  bool extRewPrepAgg__setByUser__ = false;

  bool forceNoLimitCpuWhileDump = false;\

  bool forceNoLimitCpuWhileDump__setByUser__ = false;

  bool foreignTheoryRewrite = false;\

  bool foreignTheoryRewrite__setByUser__ = false;

  IandMode iandMode = IandMode::VALUE;\

  bool iandMode__setByUser__ = false;

  bool incrementalSolving = true;\

  bool incrementalSolving__setByUser__ = false;

  bool interactiveMode;\

  bool interactiveMode__setByUser__ = false;

  bool doITESimp;\

  bool doITESimp__setByUser__ = false;

  ModelCoresMode modelCoresMode = ModelCoresMode::NONE;\

  bool modelCoresMode__setByUser__ = false;

  ModelUninterpPrintMode modelUninterpPrint = ModelUninterpPrintMode::None;\

  bool modelUninterpPrint__setByUser__ = false;

  bool modelWitnessValue = false;\

  bool modelWitnessValue__setByUser__ = false;

  bool doITESimpOnRepeat = false;\

  bool doITESimpOnRepeat__setByUser__ = false;

  bool produceAbducts = false;\

  bool produceAbducts__setByUser__ = false;

  bool produceAssertions;\

  bool produceAssertions__setByUser__ = false;

  bool produceAssignments = false;\

  bool produceAssignments__setByUser__ = false;

  ProduceInterpols produceInterpols = ProduceInterpols::NONE;\

  bool produceInterpols__setByUser__ = false;

  bool produceModels = false;\

  bool produceModels__setByUser__ = false;

  bool produceProofs = false;\

  bool produceProofs__setByUser__ = false;

  bool unsatAssumptions = false;\

  bool unsatAssumptions__setByUser__ = false;

  bool unsatCores;\

  bool unsatCores__setByUser__ = false;

  std::string regularChannelName;\

  bool regularChannelName__setByUser__ = false;

  bool repeatSimp;\

  bool repeatSimp__setByUser__ = false;

  bool compressItes = false;\

  bool compressItes__setByUser__ = false;

  uint32_t zombieHuntThreshold = 524288;\

  bool zombieHuntThreshold__setByUser__ = false;

  bool simplifyWithCareEnabled = false;\

  bool simplifyWithCareEnabled__setByUser__ = false;

  SimplificationMode simplificationMode = SimplificationMode::BATCH;\

  bool simplificationMode__setByUser__ = false;

  SolveBVAsIntMode solveBVAsInt = SolveBVAsIntMode::OFF;\

  bool solveBVAsInt__setByUser__ = false;

  uint32_t solveIntAsBV = 0;\

  bool solveIntAsBV__setByUser__ = false;

  bool solveRealAsInt = false;\

  bool solveRealAsInt__setByUser__ = false;

  bool sortInference = false;\

  bool sortInference__setByUser__ = false;

  bool doStaticLearning = true;\

  bool doStaticLearning__setByUser__ = false;

  SygusSolutionOutMode sygusOut = SygusSolutionOutMode::STANDARD;\

  bool sygusOut__setByUser__ = false;

  bool sygusPrintCallbacks = true;\

  bool sygusPrintCallbacks__setByUser__ = false;

  bool unconstrainedSimp = false;\

  bool unconstrainedSimp__setByUser__ = false;

  UnsatCoresMode unsatCoresMode = UnsatCoresMode::OFF;\

  bool unsatCoresMode__setByUser__ = false;

// clang-format on

};

#undef DO_SEMANTIC_CHECKS_BY_DEFAULT

// clang-format off

extern struct abstractValues__option_t

{

  typedef bool type;

  type operator()() const;

} thread_local abstractValues;

extern struct ackermann__option_t

{

  typedef bool type;

  type operator()() const;

} thread_local ackermann;

extern struct blockModelsMode__option_t

{

  typedef BlockModelsMode type;

  type operator()() const;

} thread_local blockModelsMode;

extern struct BVAndIntegerGranularity__option_t

{

  typedef uint32_t type;

  type operator()() const;

} thread_local BVAndIntegerGranularity;

extern struct checkAbducts__option_t

{

  typedef bool type;

  type operator()() const;

} thread_local checkAbducts;

extern struct checkInterpols__option_t

{

  typedef bool type;

  type operator()() const;

} thread_local checkInterpols;

extern struct checkModels__option_t

{

  typedef bool type;

  type operator()() const;

} thread_local checkModels;

extern struct checkProofs__option_t

{

  typedef bool type;

  type operator()() const;

} thread_local checkProofs;

extern struct checkSynthSol__option_t

{

  typedef bool type;

  type operator()() const;

} thread_local checkSynthSol;

extern struct checkUnsatCores__option_t

{

  typedef bool type;

  type operator()() const;

} thread_local checkUnsatCores;

extern struct debugCheckModels__option_t

{

  typedef bool type;

  type operator()() const;

} thread_local debugCheckModels;

extern struct diagnosticChannelName__option_t

{

  typedef std::string type;

  type operator()() const;

} thread_local diagnosticChannelName;

extern struct dumpInstantiations__option_t

{

  typedef bool type;

  type operator()() const;

} thread_local dumpInstantiations;

extern struct dumpModels__option_t

{

  typedef bool type;

  type operator()() const;

} thread_local dumpModels;

extern struct dumpProofs__option_t

{

  typedef bool type;

  type operator()() const;

} thread_local dumpProofs;

extern struct dumpToFileName__option_t

{

  typedef std::string type;

  type operator()() const;

} thread_local dumpToFileName;

extern struct dumpUnsatCores__option_t

{

  typedef bool type;

  type operator()() const;

} thread_local dumpUnsatCores;

extern struct dumpUnsatCoresFull__option_t

{

  typedef bool type;

  type operator()() const;

} thread_local dumpUnsatCoresFull;

extern struct dumpModeString__option_t

{

  typedef std::string type;

  type operator()() const;

} thread_local dumpModeString;

extern struct earlyIteRemoval__option_t

{

  typedef bool type;

  type operator()() const;

} thread_local earlyIteRemoval;

extern struct expandDefinitions__option_t

{

  typedef bool type;

  type operator()() const;

} thread_local expandDefinitions;

extern struct extRewPrep__option_t

{

  typedef bool type;

  type operator()() const;

} thread_local extRewPrep;

extern struct extRewPrepAgg__option_t

{

  typedef bool type;

  type operator()() const;

} thread_local extRewPrepAgg;

extern struct forceNoLimitCpuWhileDump__option_t

{

  typedef bool type;

  type operator()() const;

} thread_local forceNoLimitCpuWhileDump;

extern struct foreignTheoryRewrite__option_t

{

  typedef bool type;

  type operator()() const;

} thread_local foreignTheoryRewrite;

extern struct iandMode__option_t

{

  typedef IandMode type;

  type operator()() const;

} thread_local iandMode;

extern struct incrementalSolving__option_t

{

  typedef bool type;

  type operator()() const;

} thread_local incrementalSolving;

extern struct interactiveMode__option_t

{

  typedef bool type;

  type operator()() const;

} thread_local interactiveMode;

extern struct doITESimp__option_t

{

  typedef bool type;

  type operator()() const;

} thread_local doITESimp;

extern struct modelCoresMode__option_t

{

  typedef ModelCoresMode type;

  type operator()() const;

} thread_local modelCoresMode;

extern struct modelUninterpPrint__option_t

{

  typedef ModelUninterpPrintMode type;

  type operator()() const;

} thread_local modelUninterpPrint;

extern struct modelWitnessValue__option_t

{

  typedef bool type;

  type operator()() const;

} thread_local modelWitnessValue;

extern struct doITESimpOnRepeat__option_t

{

  typedef bool type;

  type operator()() const;

} thread_local doITESimpOnRepeat;

extern struct produceAbducts__option_t

{

  typedef bool type;

  type operator()() const;

} thread_local produceAbducts;

extern struct produceAssertions__option_t

{

  typedef bool type;

  type operator()() const;

} thread_local produceAssertions;

extern struct produceAssignments__option_t

{

  typedef bool type;

  type operator()() const;

} thread_local produceAssignments;

extern struct produceInterpols__option_t

{

  typedef ProduceInterpols type;

  type operator()() const;

} thread_local produceInterpols;

extern struct produceModels__option_t

{

  typedef bool type;

  type operator()() const;

} thread_local produceModels;

extern struct produceProofs__option_t

{

  typedef bool type;

  type operator()() const;

} thread_local produceProofs;

extern struct unsatAssumptions__option_t

{

  typedef bool type;

  type operator()() const;

} thread_local unsatAssumptions;

extern struct unsatCores__option_t

{

  typedef bool type;

  type operator()() const;

} thread_local unsatCores;

extern struct regularChannelName__option_t

{

  typedef std::string type;

  type operator()() const;

} thread_local regularChannelName;

extern struct repeatSimp__option_t

{

  typedef bool type;

  type operator()() const;

} thread_local repeatSimp;

extern struct compressItes__option_t

{

  typedef bool type;

  type operator()() const;

} thread_local compressItes;

extern struct zombieHuntThreshold__option_t

{

  typedef uint32_t type;

  type operator()() const;

} thread_local zombieHuntThreshold;

extern struct simplifyWithCareEnabled__option_t

{

  typedef bool type;

  type operator()() const;

} thread_local simplifyWithCareEnabled;

extern struct simplificationMode__option_t

{

  typedef SimplificationMode type;

  type operator()() const;

} thread_local simplificationMode;

extern struct solveBVAsInt__option_t

{

  typedef SolveBVAsIntMode type;

  type operator()() const;

} thread_local solveBVAsInt;

extern struct solveIntAsBV__option_t

{

  typedef uint32_t type;

  type operator()() const;

} thread_local solveIntAsBV;

extern struct solveRealAsInt__option_t

{

  typedef bool type;

  type operator()() const;

} thread_local solveRealAsInt;

extern struct sortInference__option_t

{

  typedef bool type;

  type operator()() const;

} thread_local sortInference;

extern struct doStaticLearning__option_t

{

  typedef bool type;

  type operator()() const;

} thread_local doStaticLearning;

extern struct sygusOut__option_t

{

  typedef SygusSolutionOutMode type;

  type operator()() const;

} thread_local sygusOut;

extern struct sygusPrintCallbacks__option_t

{

  typedef bool type;

  type operator()() const;

} thread_local sygusPrintCallbacks;

extern struct unconstrainedSimp__option_t

{

  typedef bool type;

  type operator()() const;

} thread_local unconstrainedSimp;

extern struct unsatCoresMode__option_t

{

  typedef UnsatCoresMode type;

  type operator()() const;

} thread_local unsatCoresMode;

// clang-format on

namespace smt

{

// clang-format off

static constexpr const char* abstractValues__name = "abstract-values";

static constexpr const char* ackermann__name = "ackermann";

static constexpr const char* blockModelsMode__name = "block-models";

static constexpr const char* BVAndIntegerGranularity__name = "bvand-integer-granularity";

static constexpr const char* checkAbducts__name = "check-abducts";

static constexpr const char* checkInterpols__name = "check-interpols";

static constexpr const char* checkModels__name = "check-models";

static constexpr const char* checkProofs__name = "check-proofs";

static constexpr const char* checkSynthSol__name = "check-synth-sol";

static constexpr const char* checkUnsatCores__name = "check-unsat-cores";

static constexpr const char* debugCheckModels__name = "debug-check-models";

static constexpr const char* diagnosticChannelName__name = "diagnostic-output-channel";

static constexpr const char* dumpInstantiations__name = "dump-instantiations";

static constexpr const char* dumpModels__name = "dump-models";

static constexpr const char* dumpProofs__name = "dump-proofs";

static constexpr const char* dumpToFileName__name = "dump-to";

static constexpr const char* dumpUnsatCores__name = "dump-unsat-cores";

static constexpr const char* dumpUnsatCoresFull__name = "dump-unsat-cores-full";

static constexpr const char* dumpModeString__name = "dump";

static constexpr const char* earlyIteRemoval__name = "early-ite-removal";

static constexpr const char* expandDefinitions__name = "expand-definitions";

static constexpr const char* extRewPrep__name = "ext-rew-prep";

static constexpr const char* extRewPrepAgg__name = "ext-rew-prep-agg";

static constexpr const char* forceNoLimitCpuWhileDump__name = "force-no-limit-cpu-while-dump";

static constexpr const char* foreignTheoryRewrite__name = "foreign-theory-rewrite";

static constexpr const char* iandMode__name = "iand-mode";

static constexpr const char* incrementalSolving__name = "incremental";

static constexpr const char* interactiveMode__name = "interactive-mode";

static constexpr const char* doITESimp__name = "ite-simp";

static constexpr const char* modelCoresMode__name = "model-cores";

static constexpr const char* modelUninterpPrint__name = "model-u-print";

static constexpr const char* modelWitnessValue__name = "model-witness-value";

static constexpr const char* doITESimpOnRepeat__name = "on-repeat-ite-simp";

static constexpr const char* produceAbducts__name = "produce-abducts";

static constexpr const char* produceAssertions__name = "produce-assertions";

static constexpr const char* produceAssignments__name = "produce-assignments";

static constexpr const char* produceInterpols__name = "produce-interpols";

static constexpr const char* produceModels__name = "produce-models";

static constexpr const char* produceProofs__name = "produce-proofs";

static constexpr const char* unsatAssumptions__name = "produce-unsat-assumptions";

static constexpr const char* unsatCores__name = "produce-unsat-cores";

static constexpr const char* regularChannelName__name = "regular-output-channel";

static constexpr const char* repeatSimp__name = "repeat-simp";

static constexpr const char* compressItes__name = "simp-ite-compress";

static constexpr const char* zombieHuntThreshold__name = "simp-ite-hunt-zombies";

static constexpr const char* simplifyWithCareEnabled__name = "simp-with-care";

static constexpr const char* simplificationMode__name = "simplification";

static constexpr const char* solveBVAsInt__name = "solve-bv-as-int";

static constexpr const char* solveIntAsBV__name = "solve-int-as-bv";

static constexpr const char* solveRealAsInt__name = "solve-real-as-int";

static constexpr const char* sortInference__name = "sort-inference";

static constexpr const char* doStaticLearning__name = "static-learning";

static constexpr const char* sygusOut__name = "sygus-out";

static constexpr const char* sygusPrintCallbacks__name = "sygus-print-callbacks";

static constexpr const char* unconstrainedSimp__name = "unconstrained-simp";

static constexpr const char* unsatCoresMode__name = "unsat-cores-mode";

// clang-format on

}

}  // namespace options

// clang-format off

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

    options::abstractValues__option_t);

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

    options::abstractValues__option_t) const;

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

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

    options::ackermann__option_t);

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

    options::ackermann__option_t) const;

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

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

    options::blockModelsMode__option_t);

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

    options::blockModelsMode__option_t) const;

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

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

    options::BVAndIntegerGranularity__option_t);

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

    options::BVAndIntegerGranularity__option_t) const;

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

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

    options::checkAbducts__option_t);

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

    options::checkAbducts__option_t) const;

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

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

    options::checkInterpols__option_t);

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

    options::checkInterpols__option_t) const;

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

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

    options::checkModels__option_t);

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

    options::checkModels__option_t) const;

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

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

    options::checkProofs__option_t);

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

    options::checkProofs__option_t) const;

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

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

    options::checkSynthSol__option_t);

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

    options::checkSynthSol__option_t) const;

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

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

    options::checkUnsatCores__option_t);

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

    options::checkUnsatCores__option_t) const;

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

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

    options::debugCheckModels__option_t);

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

    options::debugCheckModels__option_t) const;

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

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

    options::diagnosticChannelName__option_t);

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

    options::diagnosticChannelName__option_t) const;

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

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

    options::dumpInstantiations__option_t);

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

    options::dumpInstantiations__option_t) const;

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

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

    options::dumpModels__option_t);

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

    options::dumpModels__option_t) const;

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

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

    options::dumpProofs__option_t);

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

    options::dumpProofs__option_t) const;

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

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

    options::dumpToFileName__option_t);

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

    options::dumpToFileName__option_t) const;

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

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

    options::dumpUnsatCores__option_t);

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

    options::dumpUnsatCores__option_t) const;

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

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

    options::dumpUnsatCoresFull__option_t);

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

    options::dumpUnsatCoresFull__option_t) const;

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

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

    options::dumpModeString__option_t);

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

    options::dumpModeString__option_t) const;

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

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

    options::earlyIteRemoval__option_t);

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

    options::earlyIteRemoval__option_t) const;

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

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

    options::expandDefinitions__option_t);

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

    options::expandDefinitions__option_t) const;

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

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

    options::extRewPrep__option_t);

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

    options::extRewPrep__option_t) const;

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

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

    options::extRewPrepAgg__option_t);

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

    options::extRewPrepAgg__option_t) const;

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

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

    options::forceNoLimitCpuWhileDump__option_t);

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

    options::forceNoLimitCpuWhileDump__option_t) const;

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

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

    options::foreignTheoryRewrite__option_t);

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

    options::foreignTheoryRewrite__option_t) const;

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

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

    options::iandMode__option_t);

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

    options::iandMode__option_t) const;

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

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

    options::incrementalSolving__option_t);

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

    options::incrementalSolving__option_t) const;

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

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

    options::interactiveMode__option_t);

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

    options::interactiveMode__option_t) const;

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

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

    options::doITESimp__option_t);

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

    options::doITESimp__option_t) const;

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

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

    options::modelCoresMode__option_t);

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

    options::modelCoresMode__option_t) const;

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

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

    options::modelUninterpPrint__option_t);

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

    options::modelUninterpPrint__option_t) const;

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

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

    options::modelWitnessValue__option_t);

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

    options::modelWitnessValue__option_t) const;

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

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

    options::doITESimpOnRepeat__option_t);

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

    options::doITESimpOnRepeat__option_t) const;

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

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

    options::produceAbducts__option_t);

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

    options::produceAbducts__option_t) const;

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

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

    options::produceAssertions__option_t);

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

    options::produceAssertions__option_t) const;

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

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

    options::produceAssignments__option_t);

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

    options::produceAssignments__option_t) const;

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

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

    options::produceInterpols__option_t);

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

    options::produceInterpols__option_t) const;

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

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

    options::produceModels__option_t);

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

    options::produceModels__option_t) const;

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

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

    options::produceProofs__option_t);

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

    options::produceProofs__option_t) const;

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

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

    options::unsatAssumptions__option_t);

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

    options::unsatAssumptions__option_t) const;

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

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

    options::unsatCores__option_t);

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

    options::unsatCores__option_t) const;

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

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

    options::regularChannelName__option_t);

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

    options::regularChannelName__option_t) const;

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

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

    options::repeatSimp__option_t);

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

    options::repeatSimp__option_t) const;

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

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

    options::compressItes__option_t);

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

    options::compressItes__option_t) const;

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

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

    options::zombieHuntThreshold__option_t);

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

    options::zombieHuntThreshold__option_t) const;

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

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

    options::simplifyWithCareEnabled__option_t);

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

    options::simplifyWithCareEnabled__option_t) const;

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

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

    options::simplificationMode__option_t);

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

    options::simplificationMode__option_t) const;

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

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

    options::solveBVAsInt__option_t);

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

    options::solveBVAsInt__option_t) const;

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

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

    options::solveIntAsBV__option_t);

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

    options::solveIntAsBV__option_t) const;

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

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

    options::solveRealAsInt__option_t);

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

    options::solveRealAsInt__option_t) const;

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

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

    options::sortInference__option_t);

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

    options::sortInference__option_t) const;

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

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

    options::doStaticLearning__option_t);

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

    options::doStaticLearning__option_t) const;

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

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

    options::sygusOut__option_t);

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

    options::sygusOut__option_t) const;

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

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

    options::sygusPrintCallbacks__option_t);

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

    options::sygusPrintCallbacks__option_t) const;

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

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

    options::unconstrainedSimp__option_t);

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

    options::unconstrainedSimp__option_t) const;

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

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

    options::unsatCoresMode__option_t);

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

    options::unsatCoresMode__option_t) const;

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

// clang-format on

namespace options {

// clang-format off

{

}

{

}

{

}

{

}

{

}

{

}

{

}

{

}

{

}

{

}

{

}

{

}

inline dumpInstantiations__option_t::type dumpInstantiations__option_t::operator()() const

{

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

}

{

}

{

}

{

}

{

}

{

}

inline dumpModeString__option_t::type dumpModeString__option_t::operator()() const

{

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

}

{

}

inline expandDefinitions__option_t::type expandDefinitions__option_t::operator()() const

{

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

}

{

}

{

}

inline forceNoLimitCpuWhileDump__option_t::type forceNoLimitCpuWhileDump__option_t::operator()() const

{

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

}

{

}

{

}

{

}

inline interactiveMode__option_t::type interactiveMode__option_t::operator()() const

{

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

}

{

}

{

}

{

}

{

}

{

}

{

}

{

}

{

}

{

}

{

}

{

}

{

}

{

}

{

}

{

}

{

}

{

}

{

}

{

}

{

}

{

}

{

}

{

}

{

}

{

}

inline sygusPrintCallbacks__option_t::type sygusPrintCallbacks__option_t::operator()() const

{

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

}

{

}

{

}

// clang-format on

}  // namespace options

}  // namespace cvc5

#endif /* CVC5__OPTIONS__SMT_H */