2 name = "Bitvector Theory"
7 long = "bv-sat-solver=MODE"
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]]
15 [[option.mode.CRYPTOMINISAT]]
16 name = "cryptominisat"
17 [[option.mode.CADICAL]]
19 [[option.mode.KISSAT]]
25 long = "bitblast=MODE"
28 help = "choose bitblasting mode, see --bitblast=help"
29 help_mode = "Bit-blasting modes."
32 help = "Separate boolean structure and term reasoning between the core SAT solver and the bit-vector SAT solver."
35 help = "Bitblast eagerly to bit-vector SAT solver."
43 predicates = ["abcEnabledBuild", "setBitblastAig"]
44 help = "bitblast by first converting to AIG (implies --bitblast=eager)"
47 name = "bitvectorAigSimplifications"
49 long = "bv-aig-simp=COMMAND"
51 default = "\"balance;drw\""
52 predicates = ["abcEnabledBuild"]
53 help = "abc command to run AIG simplifications (implies --bitblast-aig, default is \"balance;drw\")"
56 name = "bitvectorPropagate"
61 help = "use bit-vector propagation in the bit-blaster"
64 name = "bitvectorEqualitySolver"
69 help = "use the equality engine for the bit-vector theory (only if --bv-solver=layered)"
72 name = "bitvectorInequalitySolver"
74 long = "bv-inequality-solver"
77 help = "turn on the inequality solver for the bit-vector theory (only if --bv-solver=layered)"
80 name = "bitvectorAlgebraicSolver"
81 category = "experimental"
82 long = "bv-algebraic-solver"
85 help = "turn on experimental algebraic solver for the bit-vector theory (only if --bv-solver=layered)"
88 name = "bitvectorAlgebraicBudget"
90 long = "bv-algebraic-budget=N"
93 help = "the budget allowed for the algebraic solver in number of SAT conflicts"
96 name = "bitvectorToBool"
101 help = "lift bit-vectors of size 1 to booleans when possible"
104 name = "boolToBitvector"
106 long = "bool-to-bv=MODE"
107 type = "BoolToBVMode"
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."
113 help = "Don't push any booleans to width one bit-vectors."
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."
119 help = "Force all booleans to be bit-vectors of width one except at the top level. Most aggressive mode."
127 help = "lift equivalence with one-bit bit-vectors to be boolean operations"
130 name = "bvExtractArithRewrite"
132 long = "bv-extract-arith"
135 help = "enable rewrite pushing extract [i:0] over arithmetic operations (can blow up)"
138 name = "bvAbstraction"
139 category = "undocumented"
140 long = "bv-abstraction"
143 help = "mcm benchmark abstraction"
146 name = "skolemizeArguments"
147 category = "undocumented"
148 long = "bv-skolemize"
151 help = "skolemize arguments for bv abstraction (only does something if --bv-abstraction is on)"
156 long = "bv-num-func=N"
159 help = "number of function symbols in conflicts that are generalized"
162 name = "bvEagerExplanations"
164 long = "bv-eager-explanations"
167 help = "compute bit-blasting propagation explanations eagerly"
170 name = "bitvectorQuickXplain"
172 long = "bv-quick-xplain"
175 help = "minimize bv conflicts using the QuickXplain algorithm"
178 name = "bvIntroducePow2"
180 long = "bv-intro-pow2"
183 help = "introduce bitvector powers of two as a preprocessing pass"
188 long = "bv-gauss-elim"
191 help = "simplify formula via Gaussian Elimination if applicable"
199 help = "algebraic inferences for extended functions"
202 name = "bvPrintConstsAsIndexedSymbols"
204 long = "bv-print-consts-as-indexed-symbols"
207 help = "print bit-vector constants in decimal (e.g. (_ bv1 4)) instead of binary (e.g. #b0001), applies to SMT-LIB 2.x"
212 long = "bv-solver=MODE"
215 help = "choose bit-vector solver, see --bv-solver=help"
216 help_mode = "Bit-vector solvers."
217 [[option.mode.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]]
225 help = "Enables the layered BV solver."
228 name = "bvAssertInput"
230 long = "bv-assert-input"
233 help = "assert input assertions on user-level 0 instead of assuming them in the bit-vector SAT solver"