id     = "BV"
name   = "Bitvector theory"
header = "options/bv_options.h"

[[option]]
  name       = "bvProofFormat"
  category   = "expert"
  long       = "bv-proof-format=MODE"
  type       = "BvProofFormat"
  default    = "ER"
  predicates = ["checkSatSolverEnabled<BvProofFormat>"]
  help       = "choose which UNSAT proof format to use, see --bv-sat-solver=help"
  help_mode  = "Bit-vector proof formats."
[[option.mode.ER]]
  name = "er"
  help = "Extended Resolution, i.e. resolution with new variable definitions."
[[option.mode.DRAT]]
  name = "drat"
  help = "Deletion and Resolution Asymmetric Tautology Additions."
[[option.mode.LRAT]]
  name = "lrat"
  help = "DRAT with unit propagation hints to accelerate checking."

[[option]]
  name       = "bvOptimizeSatProof"
  category   = "expert"
  long       = "bv-optimize-sat-proof=MODE"
  type       = "BvOptimizeSatProof"
  default    = "FORMULA"
  predicates = ["checkSatSolverEnabled<BvOptimizeSatProof>"]
  help       = "enable SAT proof optimizations, see --bv-optimize-sat-proof=help"
  help_mode  = "SAT proof optimization level."
[[option.mode.NONE]]
  name = "none"
  help = "Do not optimize the SAT proof."
[[option.mode.PROOF]]
  name = "proof"
  help = "Use drat-trim to shrink the SAT proof."
[[option.mode.FORMULA]]
  name = "formula"
  help = "Use drat-trim to shrink the SAT proof and formula."

[[option]]
  name       = "bvSatSolver"
  smt_name   = "bv-sat-solver"
  category   = "expert"
  long       = "bv-sat-solver=MODE"
  type       = "SatSolverMode"
  default    = "MINISAT"
  predicates = ["checkBvSatSolver"]
  help       = "choose which sat solver to use, see --bv-sat-solver=help"
  help_mode  = "SAT solver for bit-blasting backend."
[[option.mode.MINISAT]]
  name = "minisat"
[[option.mode.CRYPTOMINISAT]]
  name = "cryptominisat"
[[option.mode.CADICAL]]
  name = "cadical"

[[option]]
  name       = "bitblastMode"
  smt_name   = "bitblast"
  category   = "regular"
  long       = "bitblast=MODE"
  type       = "BitblastMode"
  default    = "LAZY"
  help       = "choose bitblasting mode, see --bitblast=help"
  help_mode  = "Bit-blasting modes."
[[option.mode.LAZY]]
  name = "lazy"
  help = "Separate boolean structure and term reasoning between the core SAT solver and the bit-vector SAT solver."
[[option.mode.EAGER]]
  name = "eager"
  help = "Bitblast eagerly to bit-vector SAT solver."

[[option]]
  name       = "bitvectorAig"
  category   = "regular"
  long       = "bitblast-aig"
  type       = "bool"
  default    = "false"
  predicates = ["abcEnabledBuild", "setBitblastAig"]
  help       = "bitblast by first converting to AIG (implies --bitblast=eager)"

[[option]]
  name       = "bitvectorAigSimplifications"
  category   = "expert"
  long       = "bv-aig-simp=COMMAND"
  type       = "std::string"
  predicates = ["abcEnabledBuild"]
  help       = "abc command to run AIG simplifications (implies --bitblast-aig, default is \"balance;drw\")"

[[option]]
  name       = "bitvectorPropagate"
  category   = "regular"
  long       = "bv-propagate"
  type       = "bool"
  default    = "true"
  help       = "use bit-vector propagation in the bit-blaster"

[[option]]
  name       = "bitvectorEqualitySolver"
  category   = "regular"
  long       = "bv-eq-solver"
  type       = "bool"
  default    = "true"
  help       = "use the equality engine for the bit-vector theory (only if --bitblast=lazy)"

[[option]]
  name       = "bitvectorEqualitySlicer"
  category   = "regular"
  long       = "bv-eq-slicer=MODE"
  type       = "BvSlicerMode"
  default    = "OFF"
  help       = "turn on the slicing equality solver for the bit-vector theory (only if --bitblast=lazy)"
  help_mode  = "Bit-vector equality slicer modes."
[[option.mode.ON]]
  name = "on"
  help = "Turn slicer on."
[[option.mode.OFF]]
  name = "off"
  help = "Turn slicer off."
[[option.mode.AUTO]]
  name = "auto"
  help = "Turn slicer on if input has only equalities over core symbols."

[[option]]
  name       = "bitvectorInequalitySolver"
  category   = "regular"
  long       = "bv-inequality-solver"
  type       = "bool"
  default    = "true"
  help       = "turn on the inequality solver for the bit-vector theory (only if --bitblast=lazy)"

[[option]]
  name       = "bitvectorAlgebraicSolver"
  category   = "regular"
  long       = "bv-algebraic-solver"
  type       = "bool"
  default    = "true"
  help       = "turn on the algebraic solver for the bit-vector theory (only if --bitblast=lazy)"

[[option]]
  name       = "bitvectorAlgebraicBudget"
  category   = "expert"
  long       = "bv-algebraic-budget=N"
  type       = "unsigned"
  default    = "1500"
  help       = "the budget allowed for the algebraic solver in number of SAT conflicts"

[[option]]
  name       = "bitvectorToBool"
  category   = "regular"
  long       = "bv-to-bool"
  type       = "bool"
  default    = "false"
  help       = "lift bit-vectors of size 1 to booleans when possible"

[[option]]
  name       = "boolToBitvector"
  smt_name   = "bool-to-bv"
  category   = "regular"
  long       = "bool-to-bv=MODE"
  type       = "BoolToBVMode"
  default    = "OFF"
  help       = "convert booleans to bit-vectors of size 1 at various levels of aggressiveness, see --bool-to-bv=help"
  help_mode  = "BoolToBV preprocessing pass modes."
[[option.mode.OFF]]
  name = "off"
  help = "Don't push any booleans to width one bit-vectors."
[[option.mode.ITE]]
  name = "ite"
  help = "Try to turn ITEs into BITVECTOR_ITE when possible. It can fail per-formula if not all sub-formulas can be turned to bit-vectors."
[[option.mode.ALL]]
  name = "all"
  help = "Force all booleans to be bit-vectors of width one except at the top level. Most aggressive mode."

[[option]]
  name       = "bitwiseEq"
  category   = "regular"
  long       = "bitwise-eq"
  type       = "bool"
  default    = "true"
  help       = "lift equivalence with one-bit bit-vectors to be boolean operations"

[[option]]
  name       = "bitvectorDivByZeroConst"
  category   = "regular"
  long       = "bv-div-zero-const"
  type       = "bool"
  default    = "false"
  help       = "always return -1 on division by zero"

[[option]]
  name       = "bvExtractArithRewrite"
  category   = "expert"
  long       = "bv-extract-arith"
  type       = "bool"
  default    = "false"
  help       = "enable rewrite pushing extract [i:0] over arithmetic operations (can blow up)"

[[option]]
  name       = "bvAbstraction"
  category   = "undocumented"
  long       = "bv-abstraction"
  type       = "bool"
  default    = "false"
  help       = "mcm benchmark abstraction"

[[option]]
  name       = "skolemizeArguments"
  category   = "undocumented"
  long       = "bv-skolemize"
  type       = "bool"
  default    = "false"
  help       = "skolemize arguments for bv abstraction (only does something if --bv-abstraction is on)"

[[option]]
  name       = "bvNumFunc"
  category   = "expert"
  long       = "bv-num-func=N"
  type       = "unsigned"
  default    = "1"
  read_only  = true
  help       = "number of function symbols in conflicts that are generalized"

[[option]]
  name       = "bvEagerExplanations"
  category   = "expert"
  long       = "bv-eager-explanations"
  type       = "bool"
  default    = "false"
  help       = "compute bit-blasting propagation explanations eagerly"

[[option]]
  name       = "bitvectorQuickXplain"
  category   = "expert"
  long       = "bv-quick-xplain"
  type       = "bool"
  default    = "false"
  read_only  = true
  help       = "minimize bv conflicts using the QuickXplain algorithm"

[[option]]
  name       = "bvIntroducePow2"
  category   = "expert"
  long       = "bv-intro-pow2"
  type       = "bool"
  default    = "false"
  read_only  = true
  help       = "introduce bitvector powers of two as a preprocessing pass"

[[option]]
  name       = "bvGaussElim"
  category   = "expert"
  long       = "bv-gauss-elim"
  type       = "bool"
  default    = "false"
  read_only  = true
  help       = "simplify formula via Gaussian Elimination if applicable"

[[option]]
  name       = "bvLazyRewriteExtf"
  category   = "regular"
  long       = "bv-lazy-rewrite-extf"
  type       = "bool"
  default    = "true"
  help       = "lazily rewrite extended functions like bv2nat and int2bv"

[[option]]
  name       = "bvLazyReduceExtf"
  category   = "regular"
  long       = "bv-lazy-reduce-extf"
  type       = "bool"
  default    = "false"
  help       = "reduce extended functions like bv2nat and int2bv at last call instead of full effort"

[[option]]
  name       = "bvAlgExtf"
  category   = "regular"
  long       = "bv-alg-extf"
  type       = "bool"
  default    = "true"
  help       = "algebraic inferences for extended functions"

[[option]]
  name       = "bvPrintConstsInBinary"
  category   = "regular"
  long       = "bv-print-consts-in-binary"
  type       = "bool"
  default    = "false"
  help       = "print bit-vector constants in binary (e.g. #b0001) instead of decimal (e.g. (_ bv1 4)), applies to SMT-LIB 2.x"