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

 * 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::options {

// clang-format off

enum class BlockModelsMode

{

  NONE, VALUES, LITERALS,

  __MAX_VALUE = LITERALS

};

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

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

enum class DifficultyMode

{

  LEMMA_LITERAL, MODEL_CHECK,

  __MAX_VALUE = MODEL_CHECK

};

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

DifficultyMode stringToDifficultyMode(const std::string& optarg);

enum class IandMode

{

  VALUE, SUM, BITWISE,

  __MAX_VALUE = BITWISE

};

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

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

enum class ModelCoresMode

{

  NONE, SIMPLE, NON_IMPLIED,

  __MAX_VALUE = NON_IMPLIED

};

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

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

enum class ModelUninterpPrintMode

{

  DeclFun, None, DeclSortAndFun,

  __MAX_VALUE = DeclSortAndFun

};

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

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

enum class ProduceInterpols

{

  NONE, SHARED, ALL, ASSUMPTIONS, CONJECTURE, DEFAULT,

  __MAX_VALUE = DEFAULT

};

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

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

enum class SimplificationMode

{

  NONE, BATCH,

  __MAX_VALUE = BATCH

};

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

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

enum class SolveBVAsIntMode

{

  OFF, BV, SUM, IAND,

  __MAX_VALUE = IAND

};

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

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

enum class SygusSolutionOutMode

{

  STATUS_OR_DEF, STATUS, STATUS_AND_DEF, STANDARD,

  __MAX_VALUE = STANDARD

};

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

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

enum class UnsatCoresMode

{

  OFF, FULL_PROOF, ASSUMPTIONS, SAT_PROOF, PP_ONLY,

  __MAX_VALUE = PP_ONLY

};

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;

  DifficultyMode difficultyMode = DifficultyMode::LEMMA_LITERAL;

  bool difficultyModeWasSetByUser = 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 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;

  bool produceDifficulty = false;

  bool produceDifficultyWasSetByUser = 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 unconstrainedSimp = false;

  bool unconstrainedSimpWasSetByUser = false;

  UnsatCoresMode unsatCoresMode = UnsatCoresMode::OFF;

  bool unsatCoresModeWasSetByUser = false;

// clang-format on

};

#undef DO_SEMANTIC_CHECKS_BY_DEFAULT

// clang-format off

inline bool ackermann() { return Options::current().smt.ackermann; }

inline BlockModelsMode blockModelsMode() { return Options::current().smt.blockModelsMode; }

inline uint64_t BVAndIntegerGranularity() { return Options::current().smt.BVAndIntegerGranularity; }

inline bool checkAbducts() { return Options::current().smt.checkAbducts; }

inline bool checkInterpols() { return Options::current().smt.checkInterpols; }

inline bool checkModels() { return Options::current().smt.checkModels; }

inline bool checkProofs() { return Options::current().smt.checkProofs; }

inline bool checkSynthSol() { return Options::current().smt.checkSynthSol; }

inline bool checkUnsatCores() { return Options::current().smt.checkUnsatCores; }

inline bool earlyIteRemoval() { return Options::current().smt.earlyIteRemoval; }

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

inline bool extRewPrep() { return Options::current().smt.extRewPrep; }

inline bool extRewPrepAgg() { return Options::current().smt.extRewPrepAgg; }

inline bool foreignTheoryRewrite() { return Options::current().smt.foreignTheoryRewrite; }

inline IandMode iandMode() { return Options::current().smt.iandMode; }

inline bool doITESimp() { return Options::current().smt.doITESimp; }

inline bool learnedRewrite() { return Options::current().smt.learnedRewrite; }

inline ModelCoresMode modelCoresMode() { return Options::current().smt.modelCoresMode; }

inline bool modelWitnessValue() { return Options::current().smt.modelWitnessValue; }

inline bool doITESimpOnRepeat() { return Options::current().smt.doITESimpOnRepeat; }

inline bool produceAbducts() { return Options::current().smt.produceAbducts; }

inline bool produceAssertions() { return Options::current().smt.produceAssertions; }

inline bool produceAssignments() { return Options::current().smt.produceAssignments; }

inline ProduceInterpols produceInterpols() { return Options::current().smt.produceInterpols; }

inline bool produceModels() { return Options::current().smt.produceModels; }

inline bool unsatAssumptions() { return Options::current().smt.unsatAssumptions; }

inline bool repeatSimp() { return Options::current().smt.repeatSimp; }

inline bool compressItes() { return Options::current().smt.compressItes; }

inline uint64_t zombieHuntThreshold() { return Options::current().smt.zombieHuntThreshold; }

inline bool simplifyWithCareEnabled() { return Options::current().smt.simplifyWithCareEnabled; }

inline SimplificationMode simplificationMode() { return Options::current().smt.simplificationMode; }

inline SolveBVAsIntMode solveBVAsInt() { return Options::current().smt.solveBVAsInt; }

inline bool sortInference() { return Options::current().smt.sortInference; }

inline bool doStaticLearning() { return Options::current().smt.doStaticLearning; }

inline bool unconstrainedSimp() { return Options::current().smt.unconstrainedSimp; }

// clang-format on

}  // namespace cvc5::options

#endif /* CVC5__OPTIONS__SMT_H */