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

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

// clang-format off

enum class BlockModelsMode

{

  NONE, VALUES, LITERALS

};

static constexpr size_t BlockModelsMode__numValues = 3;

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

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

enum class DifficultyMode

{

  MODEL_CHECK, LEMMA_LITERAL

};

static constexpr size_t DifficultyMode__numValues = 2;

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

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

enum class IandMode

{

  VALUE, SUM, BITWISE

};

static constexpr size_t IandMode__numValues = 3;

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

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

enum class ModelCoresMode

{

  NON_IMPLIED, NONE, 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

{

  DeclFun, DeclSortAndFun, None

};

static constexpr size_t ModelUninterpPrintMode__numValues = 3;

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

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

enum class ProduceInterpols

{

  CONJECTURE, NONE, DEFAULT, ALL, SHARED, ASSUMPTIONS

};

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

{

  OFF, IAND, BV, SUM

};

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_AND_DEF, STATUS, STATUS_OR_DEF, STANDARD

};

static constexpr size_t SygusSolutionOutMode__numValues = 4;

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

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

enum class UnsatCoresMode

{

  OFF, FULL_PROOF, SAT_PROOF, ASSUMPTIONS, PP_ONLY

};

static constexpr size_t UnsatCoresMode__numValues = 5;

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;

  std::string dumpModeString;

  bool dumpModeStringWasSetByUser = false;

  ManagedOut dumpToFileName;

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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 bool sygusPrintCallbacks() { return Options::current().smt.sygusPrintCallbacks; }

// 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* difficultyMode__name = "difficulty-mode";

static constexpr const char* dumpModeString__name = "dump";

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

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* produceDifficulty__name = "produce-difficulty";

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";

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 setDefaultDifficultyMode(Options& opts, DifficultyMode value);

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

void setDefaultDumpToFileName(Options& opts, ManagedOut 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 setDefaultProduceDifficulty(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 cvc5::options

#endif /* CVC5__OPTIONS__SMT_H */