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

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

namespace options {

// clang-format off

enum class BitblastMode

{

  EAGER,

  LAZY

};

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,

  OFF,

  ALL

};

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,

  KISSAT,

  CADICAL,

  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

{

  LAYERED,

  BITBLAST_INTERNAL,

  BITBLAST

};

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;

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

  unsigned 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

extern struct bitvectorAig__option_t

{

  typedef bool type;

  type operator()() const;

} thread_local bitvectorAig;

extern struct bitblastMode__option_t

{

  typedef BitblastMode type;

  type operator()() const;

} thread_local bitblastMode;

extern struct bitwiseEq__option_t

{

  typedef bool type;

  type operator()() const;

} thread_local bitwiseEq;

extern struct boolToBitvector__option_t

{

  typedef BoolToBVMode type;

  type operator()() const;

} thread_local boolToBitvector;

extern struct bvAbstraction__option_t

{

  typedef bool type;

  type operator()() const;

} thread_local bvAbstraction;

extern struct bitvectorAigSimplifications__option_t

{

  typedef std::string type;

  type operator()() const;

} thread_local bitvectorAigSimplifications;

extern struct bvAlgExtf__option_t

{

  typedef bool type;

  type operator()() const;

} thread_local bvAlgExtf;

extern struct bitvectorAlgebraicBudget__option_t

{

  typedef unsigned type;

  type operator()() const;

} thread_local bitvectorAlgebraicBudget;

extern struct bitvectorAlgebraicSolver__option_t

{

  typedef bool type;

  type operator()() const;

} thread_local bitvectorAlgebraicSolver;

extern struct bvAssertInput__option_t

{

  typedef bool type;

  type operator()() const;

} thread_local bvAssertInput;

extern struct bvEagerExplanations__option_t

{

  typedef bool type;

  type operator()() const;

} thread_local bvEagerExplanations;

extern struct bitvectorEqualitySolver__option_t

{

  typedef bool type;

  type operator()() const;

} thread_local bitvectorEqualitySolver;

extern struct bvExtractArithRewrite__option_t

{

  typedef bool type;

  type operator()() const;

} thread_local bvExtractArithRewrite;

extern struct bvGaussElim__option_t

{

  typedef bool type;

  type operator()() const;

} thread_local bvGaussElim;

extern struct bitvectorInequalitySolver__option_t

{

  typedef bool type;

  type operator()() const;

} thread_local bitvectorInequalitySolver;

extern struct bvIntroducePow2__option_t

{

  typedef bool type;

  type operator()() const;

} thread_local bvIntroducePow2;

extern struct bvNumFunc__option_t

{

  typedef unsigned type;

  type operator()() const;

} thread_local bvNumFunc;

extern struct bvPrintConstsAsIndexedSymbols__option_t

{

  typedef bool type;

  type operator()() const;

} thread_local bvPrintConstsAsIndexedSymbols;

extern struct bitvectorPropagate__option_t

{

  typedef bool type;

  type operator()() const;

} thread_local bitvectorPropagate;

extern struct bitvectorQuickXplain__option_t

{

  typedef bool type;

  type operator()() const;

} thread_local bitvectorQuickXplain;

extern struct bvSatSolver__option_t

{

  typedef SatSolverMode type;

  type operator()() const;

} thread_local bvSatSolver;

extern struct skolemizeArguments__option_t

{

  typedef bool type;

  type operator()() const;

} thread_local skolemizeArguments;

extern struct bvSolver__option_t

{

  typedef BVSolver type;

  type operator()() const;

} thread_local bvSolver;

extern struct bitvectorToBool__option_t

{

  typedef bool type;

  type operator()() const;

} thread_local bitvectorToBool;

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

// clang-format on

}

}  // namespace options

// clang-format off

// clang-format on

namespace options {

// clang-format off

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

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

inline bool bvAlgExtf__option_t::operator()() const

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

// clang-format on

namespace bv

{

// clang-format off

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, unsigned 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, unsigned 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 options

}  // namespace cvc5

#endif /* CVC5__OPTIONS__BV_H */