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

 * 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

#include "options/managed_streams.h"

#include <iostream>

// clang-format on

namespace cvc5 {

namespace options {

// clang-format off

enum class BlockModelsMode

{

  VALUES,

  NONE,

  LITERALS

};

static constexpr size_t BlockModelsMode__numValues = 3;

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

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

enum class IandMode

{

  BITWISE,

  SUM,

  VALUE

};

static constexpr size_t IandMode__numValues = 3;

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

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

enum class ModelCoresMode

{

  NONE,

  NON_IMPLIED,

  SIMPLE

};

static constexpr size_t ModelCoresMode__numValues = 3;

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

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

enum class ModelUninterpPrintMode

{

  None,

  DeclFun,

  DtEnum,

  DeclSortAndFun

};

static constexpr size_t ModelUninterpPrintMode__numValues = 4;

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

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

enum class ProduceInterpols

{

  DEFAULT,

  CONJECTURE,

  NONE,

  ASSUMPTIONS,

  ALL,

  SHARED

};

static constexpr size_t ProduceInterpols__numValues = 6;

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

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

enum class SimplificationMode

{

  NONE,

  BATCH

};

static constexpr size_t SimplificationMode__numValues = 2;

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

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

enum class SolveBVAsIntMode

{

  IAND,

  SUM,

  OFF,

  BV

};

static constexpr size_t SolveBVAsIntMode__numValues = 4;

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

};

static constexpr size_t SygusSolutionOutMode__numValues = 4;

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

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

enum class UnsatCoresMode

{

  SAT_PROOF,

  FULL_PROOF,

  OFF,

  ASSUMPTIONS

};

static constexpr size_t UnsatCoresMode__numValues = 4;

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 abstractValuesWasSetByUser = false;

  bool ackermann = false;

  bool ackermannWasSetByUser = false;

  BlockModelsMode blockModelsMode = BlockModelsMode::NONE;

  bool blockModelsModeWasSetByUser = false;

  uint64_t BVAndIntegerGranularity = 1;

  bool BVAndIntegerGranularityWasSetByUser = false;

  bool checkAbducts = false;

  bool checkAbductsWasSetByUser = false;

  bool checkInterpols = false;

  bool checkInterpolsWasSetByUser = false;

  bool checkModels;

  bool checkModelsWasSetByUser = false;

  bool checkProofs;

  bool checkProofsWasSetByUser = false;

  bool checkSynthSol = false;

  bool checkSynthSolWasSetByUser = false;

  bool checkUnsatCores;

  bool checkUnsatCoresWasSetByUser = false;

  bool debugCheckModels;

  bool debugCheckModelsWasSetByUser = false;

  ManagedOut dumpToFileName;

  bool dumpToFileNameWasSetByUser = false;

  std::string dumpModeString;

  bool dumpModeStringWasSetByUser = false;

  bool earlyIteRemoval = false;

  bool earlyIteRemovalWasSetByUser = false;

  bool expandDefinitions = false;

  bool expandDefinitionsWasSetByUser = false;

  bool extRewPrep = false;

  bool extRewPrepWasSetByUser = false;

  bool extRewPrepAgg = false;

  bool extRewPrepAggWasSetByUser = false;

  bool foreignTheoryRewrite = false;

  bool foreignTheoryRewriteWasSetByUser = false;

  IandMode iandMode = IandMode::VALUE;

  bool iandModeWasSetByUser = false;

  bool interactiveMode;

  bool interactiveModeWasSetByUser = false;

  bool doITESimp;

  bool doITESimpWasSetByUser = false;

  bool learnedRewrite = false;

  bool learnedRewriteWasSetByUser = false;

  bool minimalUnsatCores = false;

  bool minimalUnsatCoresWasSetByUser = false;

  ModelCoresMode modelCoresMode = ModelCoresMode::NONE;

  bool modelCoresModeWasSetByUser = false;

  ModelUninterpPrintMode modelUninterpPrint = ModelUninterpPrintMode::None;

  bool modelUninterpPrintWasSetByUser = false;

  bool modelWitnessValue = false;

  bool modelWitnessValueWasSetByUser = false;

  bool doITESimpOnRepeat = false;

  bool doITESimpOnRepeatWasSetByUser = false;

  bool produceAbducts = false;

  bool produceAbductsWasSetByUser = false;

  bool produceAssertions;

  bool produceAssertionsWasSetByUser = false;

  bool produceAssignments = false;

  bool produceAssignmentsWasSetByUser = false;

  ProduceInterpols produceInterpols = ProduceInterpols::NONE;

  bool produceInterpolsWasSetByUser = false;

  bool produceModels = false;

  bool produceModelsWasSetByUser = false;

  bool produceProofs = false;

  bool produceProofsWasSetByUser = false;

  bool unsatAssumptions = false;

  bool unsatAssumptionsWasSetByUser = false;

  bool unsatCores;

  bool unsatCoresWasSetByUser = false;

  bool repeatSimp;

  bool repeatSimpWasSetByUser = false;

  bool compressItes = false;

  bool compressItesWasSetByUser = false;

  uint64_t zombieHuntThreshold = 524288;

  bool zombieHuntThresholdWasSetByUser = false;

  bool simplifyWithCareEnabled = false;

  bool simplifyWithCareEnabledWasSetByUser = false;

  SimplificationMode simplificationMode = SimplificationMode::BATCH;

  bool simplificationModeWasSetByUser = false;

  SolveBVAsIntMode solveBVAsInt = SolveBVAsIntMode::OFF;

  bool solveBVAsIntWasSetByUser = false;

  uint64_t solveIntAsBV = 0;

  bool solveIntAsBVWasSetByUser = false;

  bool solveRealAsInt = false;

  bool solveRealAsIntWasSetByUser = false;

  bool sortInference = false;

  bool sortInferenceWasSetByUser = false;

  bool doStaticLearning = true;

  bool doStaticLearningWasSetByUser = false;

  SygusSolutionOutMode sygusOut = SygusSolutionOutMode::STANDARD;

  bool sygusOutWasSetByUser = false;

  bool sygusPrintCallbacks = true;

  bool sygusPrintCallbacksWasSetByUser = false;

  bool unconstrainedSimp = false;

  bool unconstrainedSimpWasSetByUser = false;

  UnsatCoresMode unsatCoresMode = UnsatCoresMode::OFF;

  bool unsatCoresModeWasSetByUser = 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 uint64_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 dumpToFileName__option_t

{

  typedef ManagedOut type;

  type operator()() const;

} thread_local dumpToFileName;

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 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 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 learnedRewrite__option_t

{

  typedef bool type;

  type operator()() const;

} thread_local learnedRewrite;

extern struct minimalUnsatCores__option_t

{

  typedef bool type;

  type operator()() const;

} thread_local minimalUnsatCores;

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 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 uint64_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 uint64_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* dumpToFileName__name = "dump-to";

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* foreignTheoryRewrite__name = "foreign-theory-rewrite";

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

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

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

static constexpr const char* learnedRewrite__name = "learned-rewrite";

static constexpr const char* minimalUnsatCores__name = "minimal-unsat-cores";

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

// clang-format on

namespace options {

// clang-format off

inline ManagedOut dumpToFileName__option_t::operator()() const

{ return Options::current().smt.dumpToFileName; }

inline std::string dumpModeString__option_t::operator()() const

{ return Options::current().smt.dumpModeString; }

inline bool expandDefinitions__option_t::operator()() const

{ return Options::current().smt.expandDefinitions; }

inline bool interactiveMode__option_t::operator()() const

{ return Options::current().smt.interactiveMode; }

inline bool sygusPrintCallbacks__option_t::operator()() const

{ return Options::current().smt.sygusPrintCallbacks; }

// clang-format on

namespace smt

{

// clang-format off

void setDefaultAbstractValues(Options& opts, bool value);

void setDefaultAckermann(Options& opts, bool value);

void setDefaultBlockModelsMode(Options& opts, BlockModelsMode value);

void setDefaultBVAndIntegerGranularity(Options& opts, uint64_t value);

void setDefaultCheckAbducts(Options& opts, bool value);

void setDefaultCheckInterpols(Options& opts, bool value);

void setDefaultCheckModels(Options& opts, bool value);

void setDefaultCheckProofs(Options& opts, bool value);

void setDefaultCheckSynthSol(Options& opts, bool value);

void setDefaultCheckUnsatCores(Options& opts, bool value);

void setDefaultDebugCheckModels(Options& opts, bool value);

void setDefaultDumpToFileName(Options& opts, ManagedOut value);

void setDefaultDumpModeString(Options& opts, std::string value);

void setDefaultEarlyIteRemoval(Options& opts, bool value);

void setDefaultExpandDefinitions(Options& opts, bool value);

void setDefaultExtRewPrep(Options& opts, bool value);

void setDefaultExtRewPrepAgg(Options& opts, bool value);

void setDefaultForeignTheoryRewrite(Options& opts, bool value);

void setDefaultIandMode(Options& opts, IandMode value);

void setDefaultInteractiveMode(Options& opts, bool value);

void setDefaultDoITESimp(Options& opts, bool value);

void setDefaultLearnedRewrite(Options& opts, bool value);

void setDefaultMinimalUnsatCores(Options& opts, bool value);

void setDefaultModelCoresMode(Options& opts, ModelCoresMode value);

void setDefaultModelUninterpPrint(Options& opts, ModelUninterpPrintMode value);

void setDefaultModelWitnessValue(Options& opts, bool value);

void setDefaultDoITESimpOnRepeat(Options& opts, bool value);

void setDefaultProduceAbducts(Options& opts, bool value);

void setDefaultProduceAssertions(Options& opts, bool value);

void setDefaultProduceAssignments(Options& opts, bool value);

void setDefaultProduceInterpols(Options& opts, ProduceInterpols value);

void setDefaultProduceModels(Options& opts, bool value);

void setDefaultProduceProofs(Options& opts, bool value);

void setDefaultUnsatAssumptions(Options& opts, bool value);

void setDefaultUnsatCores(Options& opts, bool value);

void setDefaultRepeatSimp(Options& opts, bool value);

void setDefaultCompressItes(Options& opts, bool value);

void setDefaultZombieHuntThreshold(Options& opts, uint64_t value);

void setDefaultSimplifyWithCareEnabled(Options& opts, bool value);

void setDefaultSimplificationMode(Options& opts, SimplificationMode value);

void setDefaultSolveBVAsInt(Options& opts, SolveBVAsIntMode value);

void setDefaultSolveIntAsBV(Options& opts, uint64_t value);

void setDefaultSolveRealAsInt(Options& opts, bool value);

void setDefaultSortInference(Options& opts, bool value);

void setDefaultDoStaticLearning(Options& opts, bool value);

void setDefaultSygusOut(Options& opts, SygusSolutionOutMode value);

void setDefaultSygusPrintCallbacks(Options& opts, bool value);

void setDefaultUnconstrainedSimp(Options& opts, bool value);

void setDefaultUnsatCoresMode(Options& opts, UnsatCoresMode value);

// clang-format on

}

}  // namespace options

}  // namespace cvc5

#endif /* CVC5__OPTIONS__SMT_H */