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

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

#define CVC5__OPTIONS__BV_H

#include "options/options.h"

// clang-format off

// clang-format on

namespace cvc5::options {

// clang-format off

enum class BitblastMode

{

  LAZY,

  EAGER

};

static constexpr size_t BitblastMode__numValues = 2;

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

BitblastMode stringToBitblastMode(const std::string& optarg);

enum class BoolToBVMode

{

  ITE,

  ALL,

  OFF

};

static constexpr size_t BoolToBVMode__numValues = 3;

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

BoolToBVMode stringToBoolToBVMode(const std::string& optarg);

enum class SatSolverMode

{

  MINISAT,

  CADICAL,

  KISSAT,

  CRYPTOMINISAT

};

static constexpr size_t SatSolverMode__numValues = 4;

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

SatSolverMode stringToSatSolverMode(const std::string& optarg);

enum class BVSolver

{

  BITBLAST_INTERNAL,

  BITBLAST,

  LAYERED

};

static constexpr size_t BVSolver__numValues = 3;

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

BVSolver stringToBVSolver(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 bitvectorAig = false;

  bool bitvectorAigWasSetByUser = false;

  BitblastMode bitblastMode = BitblastMode::LAZY;

  bool bitblastModeWasSetByUser = false;

  bool bitwiseEq = true;

  bool bitwiseEqWasSetByUser = false;

  BoolToBVMode boolToBitvector = BoolToBVMode::OFF;

  bool boolToBitvectorWasSetByUser = false;

  bool bvAbstraction = false;

  bool bvAbstractionWasSetByUser = false;

  std::string bitvectorAigSimplifications = "balance;drw";

  bool bitvectorAigSimplificationsWasSetByUser = false;

  bool bvAlgExtf = true;

  bool bvAlgExtfWasSetByUser = false;

  uint64_t bitvectorAlgebraicBudget = 1500;

  bool bitvectorAlgebraicBudgetWasSetByUser = false;

  bool bitvectorAlgebraicSolver = false;

  bool bitvectorAlgebraicSolverWasSetByUser = false;

  bool bvAssertInput = false;

  bool bvAssertInputWasSetByUser = false;

  bool bvEagerExplanations = false;

  bool bvEagerExplanationsWasSetByUser = false;

  bool bitvectorEqualitySolver = true;

  bool bitvectorEqualitySolverWasSetByUser = false;

  bool bvExtractArithRewrite = false;

  bool bvExtractArithRewriteWasSetByUser = false;

  bool bvGaussElim = false;

  bool bvGaussElimWasSetByUser = false;

  bool bitvectorInequalitySolver = true;

  bool bitvectorInequalitySolverWasSetByUser = false;

  bool bvIntroducePow2 = false;

  bool bvIntroducePow2WasSetByUser = false;

  uint64_t bvNumFunc = 1;

  bool bvNumFuncWasSetByUser = false;

  bool bvPrintConstsAsIndexedSymbols = false;

  bool bvPrintConstsAsIndexedSymbolsWasSetByUser = false;

  bool bitvectorPropagate = true;

  bool bitvectorPropagateWasSetByUser = false;

  bool bitvectorQuickXplain = false;

  bool bitvectorQuickXplainWasSetByUser = false;

  SatSolverMode bvSatSolver = SatSolverMode::MINISAT;

  bool bvSatSolverWasSetByUser = false;

  bool skolemizeArguments = false;

  bool skolemizeArgumentsWasSetByUser = false;

  BVSolver bvSolver = BVSolver::BITBLAST;

  bool bvSolverWasSetByUser = false;

  bool bitvectorToBool = false;

  bool bitvectorToBoolWasSetByUser = false;

// clang-format on

};

#undef DO_SEMANTIC_CHECKS_BY_DEFAULT

// clang-format off

inline std::string bitvectorAigSimplifications() { return Options::current().bv.bitvectorAigSimplifications; }

inline bool bvAlgExtf() { return Options::current().bv.bvAlgExtf; }

// clang-format on

namespace bv

{

// clang-format off

static constexpr const char* bitvectorAig__name = "bitblast-aig";

static constexpr const char* bitblastMode__name = "bitblast";

static constexpr const char* bitwiseEq__name = "bitwise-eq";

static constexpr const char* boolToBitvector__name = "bool-to-bv";

static constexpr const char* bvAbstraction__name = "bv-abstraction";

static constexpr const char* bitvectorAigSimplifications__name = "bv-aig-simp";

static constexpr const char* bvAlgExtf__name = "bv-alg-extf";

static constexpr const char* bitvectorAlgebraicBudget__name = "bv-algebraic-budget";

static constexpr const char* bitvectorAlgebraicSolver__name = "bv-algebraic-solver";

static constexpr const char* bvAssertInput__name = "bv-assert-input";

static constexpr const char* bvEagerExplanations__name = "bv-eager-explanations";

static constexpr const char* bitvectorEqualitySolver__name = "bv-eq-solver";

static constexpr const char* bvExtractArithRewrite__name = "bv-extract-arith";

static constexpr const char* bvGaussElim__name = "bv-gauss-elim";

static constexpr const char* bitvectorInequalitySolver__name = "bv-inequality-solver";

static constexpr const char* bvIntroducePow2__name = "bv-intro-pow2";

static constexpr const char* bvNumFunc__name = "bv-num-func";

static constexpr const char* bvPrintConstsAsIndexedSymbols__name = "bv-print-consts-as-indexed-symbols";

static constexpr const char* bitvectorPropagate__name = "bv-propagate";

static constexpr const char* bitvectorQuickXplain__name = "bv-quick-xplain";

static constexpr const char* bvSatSolver__name = "bv-sat-solver";

static constexpr const char* skolemizeArguments__name = "bv-skolemize";

static constexpr const char* bvSolver__name = "bv-solver";

static constexpr const char* bitvectorToBool__name = "bv-to-bool";

void setDefaultBitvectorAig(Options& opts, bool value);void setDefaultBitblastMode(Options& opts, BitblastMode value);void setDefaultBitwiseEq(Options& opts, bool value);void setDefaultBoolToBitvector(Options& opts, BoolToBVMode value);void setDefaultBvAbstraction(Options& opts, bool value);void setDefaultBitvectorAigSimplifications(Options& opts, std::string value);void setDefaultBvAlgExtf(Options& opts, bool value);void setDefaultBitvectorAlgebraicBudget(Options& opts, uint64_t value);void setDefaultBitvectorAlgebraicSolver(Options& opts, bool value);void setDefaultBvAssertInput(Options& opts, bool value);void setDefaultBvEagerExplanations(Options& opts, bool value);void setDefaultBitvectorEqualitySolver(Options& opts, bool value);void setDefaultBvExtractArithRewrite(Options& opts, bool value);void setDefaultBvGaussElim(Options& opts, bool value);void setDefaultBitvectorInequalitySolver(Options& opts, bool value);void setDefaultBvIntroducePow2(Options& opts, bool value);void setDefaultBvNumFunc(Options& opts, uint64_t value);void setDefaultBvPrintConstsAsIndexedSymbols(Options& opts, bool value);void setDefaultBitvectorPropagate(Options& opts, bool value);void setDefaultBitvectorQuickXplain(Options& opts, bool value);void setDefaultBvSatSolver(Options& opts, SatSolverMode value);void setDefaultSkolemizeArguments(Options& opts, bool value);void setDefaultBvSolver(Options& opts, BVSolver value);void setDefaultBitvectorToBool(Options& opts, bool value);

// clang-format on

}

}  // namespace cvc5::options

#endif /* CVC5__OPTIONS__BV_H */