src/options/bv_options.toml

   1 id     = "BV"
   2 name   = "Bitvector Theory"
   3
   4 [[option]]
   5   name       = "bvSatSolver"
   6   category   = "expert"
   7   long       = "bv-sat-solver=MODE"
   8   type       = "SatSolverMode"
   9   default    = "MINISAT"
  10   predicates = ["checkBvSatSolver"]
  11   help       = "choose which sat solver to use, see --bv-sat-solver=help"
  12   help_mode  = "SAT solver for bit-blasting backend."
  13 [[option.mode.MINISAT]]
  14   name = "minisat"
  15 [[option.mode.CRYPTOMINISAT]]
  16   name = "cryptominisat"
  17 [[option.mode.CADICAL]]
  18   name = "cadical"
  19 [[option.mode.KISSAT]]
  20   name = "kissat"
  21
  22 [[option]]
  23   name       = "bitblastMode"
  24   category   = "regular"
  25   long       = "bitblast=MODE"
  26   type       = "BitblastMode"
  27   default    = "LAZY"
  28   help       = "choose bitblasting mode, see --bitblast=help"
  29   help_mode  = "Bit-blasting modes."
  30 [[option.mode.LAZY]]
  31   name = "lazy"
  32   help = "Separate boolean structure and term reasoning between the core SAT solver and the bit-vector SAT solver."
  33 [[option.mode.EAGER]]
  34   name = "eager"
  35   help = "Bitblast eagerly to bit-vector SAT solver."
  36
  37 [[option]]
  38   name       = "bitvectorAig"
  39   category   = "regular"
  40   long       = "bitblast-aig"
  41   type       = "bool"
  42   default    = "false"
  43   predicates = ["abcEnabledBuild", "setBitblastAig"]
  44   help       = "bitblast by first converting to AIG (implies --bitblast=eager)"
  45
  46 [[option]]
  47   name       = "bitvectorAigSimplifications"
  48   category   = "expert"
  49   long       = "bv-aig-simp=COMMAND"
  50   type       = "std::string"
  51   default    = "\"balance;drw\""
  52   predicates = ["abcEnabledBuild"]
  53   help       = "abc command to run AIG simplifications (implies --bitblast-aig, default is \"balance;drw\")"
  54
  55 [[option]]
  56   name       = "bitvectorPropagate"
  57   category   = "regular"
  58   long       = "bv-propagate"
  59   type       = "bool"
  60   default    = "true"
  61   help       = "use bit-vector propagation in the bit-blaster"
  62
  63 [[option]]
  64   name       = "bitvectorEqualitySolver"
  65   category   = "regular"
  66   long       = "bv-eq-solver"
  67   type       = "bool"
  68   default    = "true"
  69   help       = "use the equality engine for the bit-vector theory (only if --bv-solver=layered)"
  70
  71 [[option]]
  72   name       = "bitvectorInequalitySolver"
  73   category   = "regular"
  74   long       = "bv-inequality-solver"
  75   type       = "bool"
  76   default    = "true"
  77   help       = "turn on the inequality solver for the bit-vector theory (only if --bv-solver=layered)"
  78
  79 [[option]]
  80   name       = "bitvectorAlgebraicSolver"
  81   category   = "experimental"
  82   long       = "bv-algebraic-solver"
  83   type       = "bool"
  84   default    = "false"
  85   help       = "turn on experimental algebraic solver for the bit-vector theory (only if --bv-solver=layered)"
  86
  87 [[option]]
  88   name       = "bitvectorAlgebraicBudget"
  89   category   = "expert"
  90   long       = "bv-algebraic-budget=N"
  91   type       = "unsigned"
  92   default    = "1500"
  93   help       = "the budget allowed for the algebraic solver in number of SAT conflicts"
  94
  95 [[option]]
  96   name       = "bitvectorToBool"
  97   category   = "regular"
  98   long       = "bv-to-bool"
  99   type       = "bool"
 100   default    = "false"
 101   help       = "lift bit-vectors of size 1 to booleans when possible"
 102
 103 [[option]]
 104   name       = "boolToBitvector"
 105   category   = "regular"
 106   long       = "bool-to-bv=MODE"
 107   type       = "BoolToBVMode"
 108   default    = "OFF"
 109   help       = "convert booleans to bit-vectors of size 1 at various levels of aggressiveness, see --bool-to-bv=help"
 110   help_mode  = "BoolToBV preprocessing pass modes."
 111 [[option.mode.OFF]]
 112   name = "off"
 113   help = "Don't push any booleans to width one bit-vectors."
 114 [[option.mode.ITE]]
 115   name = "ite"
 116   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."
 117 [[option.mode.ALL]]
 118   name = "all"
 119   help = "Force all booleans to be bit-vectors of width one except at the top level. Most aggressive mode."
 120
 121 [[option]]
 122   name       = "bitwiseEq"
 123   category   = "regular"
 124   long       = "bitwise-eq"
 125   type       = "bool"
 126   default    = "true"
 127   help       = "lift equivalence with one-bit bit-vectors to be boolean operations"
 128
 129 [[option]]
 130   name       = "bvExtractArithRewrite"
 131   category   = "expert"
 132   long       = "bv-extract-arith"
 133   type       = "bool"
 134   default    = "false"
 135   help       = "enable rewrite pushing extract [i:0] over arithmetic operations (can blow up)"
 136
 137 [[option]]
 138   name       = "bvAbstraction"
 139   category   = "undocumented"
 140   long       = "bv-abstraction"
 141   type       = "bool"
 142   default    = "false"
 143   help       = "mcm benchmark abstraction"
 144
 145 [[option]]
 146   name       = "skolemizeArguments"
 147   category   = "undocumented"
 148   long       = "bv-skolemize"
 149   type       = "bool"
 150   default    = "false"
 151   help       = "skolemize arguments for bv abstraction (only does something if --bv-abstraction is on)"
 152
 153 [[option]]
 154   name       = "bvNumFunc"
 155   category   = "expert"
 156   long       = "bv-num-func=N"
 157   type       = "unsigned"
 158   default    = "1"
 159   help       = "number of function symbols in conflicts that are generalized"
 160
 161 [[option]]
 162   name       = "bvEagerExplanations"
 163   category   = "expert"
 164   long       = "bv-eager-explanations"
 165   type       = "bool"
 166   default    = "false"
 167   help       = "compute bit-blasting propagation explanations eagerly"
 168
 169 [[option]]
 170   name       = "bitvectorQuickXplain"
 171   category   = "expert"
 172   long       = "bv-quick-xplain"
 173   type       = "bool"
 174   default    = "false"
 175   help       = "minimize bv conflicts using the QuickXplain algorithm"
 176
 177 [[option]]
 178   name       = "bvIntroducePow2"
 179   category   = "expert"
 180   long       = "bv-intro-pow2"
 181   type       = "bool"
 182   default    = "false"
 183   help       = "introduce bitvector powers of two as a preprocessing pass"
 184
 185 [[option]]
 186   name       = "bvGaussElim"
 187   category   = "expert"
 188   long       = "bv-gauss-elim"
 189   type       = "bool"
 190   default    = "false"
 191   help       = "simplify formula via Gaussian Elimination if applicable"
 192
 193 [[option]]
 194   name       = "bvAlgExtf"
 195   category   = "regular"
 196   long       = "bv-alg-extf"
 197   type       = "bool"
 198   default    = "true"
 199   help       = "algebraic inferences for extended functions"
 200
 201 [[option]]
 202   name       = "bvPrintConstsAsIndexedSymbols"
 203   category   = "regular"
 204   long       = "bv-print-consts-as-indexed-symbols"
 205   type       = "bool"
 206   default    = "false"
 207   help       = "print bit-vector constants in decimal (e.g. (_ bv1 4)) instead of binary (e.g. #b0001), applies to SMT-LIB 2.x"
 208
 209 [[option]]
 210   name       = "bvSolver"
 211   category   = "regular"
 212   long       = "bv-solver=MODE"
 213   type       = "BVSolver"
 214   default    = "BITBLAST"
 215   help       = "choose bit-vector solver, see --bv-solver=help"
 216   help_mode  = "Bit-vector solvers."
 217 [[option.mode.BITBLAST]]
 218   name = "bitblast"
 219   help = "Enables bitblasting solver."
 220 [[option.mode.BITBLAST_INTERNAL]]
 221   name = "bitblast-internal"
 222   help = "Enables bitblasting to internal SAT solver with proof support."
 223 [[option.mode.LAYERED]]
 224   name = "layered"
 225   help = "Enables the layered BV solver."
 226
 227 [[option]]
 228   name       = "bvAssertInput"
 229   category   = "regular"
 230   long       = "bv-assert-input"
 231   type       = "bool"
 232   default    = "false"
 233   help       = "assert input assertions on user-level 0 instead of assuming them in the bit-vector SAT solver"
 234