diff options
Diffstat (limited to 'src/options/bv_options')
| -rw-r--r-- | src/options/bv_options | 69 |
1 files changed, 69 insertions, 0 deletions
diff --git a/src/options/bv_options b/src/options/bv_options new file mode 100644 index 000000000..73790b562 --- /dev/null +++ b/src/options/bv_options @@ -0,0 +1,69 @@ +# +# Option specification file for CVC4 +# See src/options/base_options for a description of this file format +# + +module BV "options/bv_options.h" Bitvector theory + +# Option to set the bit-blasting mode (lazy, eager) + +option bitblastMode bitblast --bitblast=MODE CVC4::theory::bv::BitblastMode :handler CVC4::options::stringToBitblastMode :default CVC4::theory::bv::BITBLAST_MODE_LAZY :read-write :include "options/bv_bitblast_mode.h" :handler-include "options/options_handler_interface.h" + choose bitblasting mode, see --bitblast=help + +# Options for eager bit-blasting + +option bitvectorAig --bitblast-aig bool :default false :predicate CVC4::options::abcEnabledBuild CVC4::options::setBitblastAig :predicate-include "options/options_handler_interface.h" :read-write + bitblast by first converting to AIG (implies --bitblast=eager) +expert-option bitvectorAigSimplifications --bv-aig-simp=COMMAND std::string :default "" :predicate CVC4::options::abcEnabledBuild :read-write :link --bitblast-aig :link-smt bitblast-aig + abc command to run AIG simplifications (implies --bitblast-aig, default is "balance;drw") + +# Options for lazy bit-blasting + +option bitvectorPropagate --bv-propagate bool :default true :read-write :link --bitblast=lazy + use bit-vector propagation in the bit-blaster + +option bitvectorEqualitySolver --bv-eq-solver bool :default true :read-write :link --bitblast=lazy + use the equality engine for the bit-vector theory (only if --bitblast=lazy) + +option bitvectorEqualitySlicer --bv-eq-slicer=MODE CVC4::theory::bv::BvSlicerMode :handler CVC4::options::stringToBvSlicerMode :default CVC4::theory::bv::BITVECTOR_SLICER_OFF :read-write :include "options/bv_bitblast_mode.h" :handler-include "options/options_handler_interface.h" :read-write :link --bv-eq-solver + turn on the slicing equality solver for the bit-vector theory (only if --bitblast=lazy) + +option bitvectorInequalitySolver --bv-inequality-solver bool :default true :read-write :link --bitblast=lazy + turn on the inequality solver for the bit-vector theory (only if --bitblast=lazy) + +option bitvectorAlgebraicSolver --bv-algebraic-solver bool :default true :read-write :link --bitblast=lazy + turn on the algebraic solver for the bit-vector theory (only if --bitblast=lazy) + +expert-option bitvectorAlgebraicBudget --bv-algebraic-budget unsigned :default 1500 :read-write :link --bv-algebraic-solver + the budget allowed for the algebraic solver in number of SAT conflicts + +# General options + +option bitvectorToBool --bv-to-bool bool :default false :read-write + lift bit-vectors of size 1 to booleans when possible + +option bitvectorDivByZeroConst --bv-div-zero-const bool :default false :read-write + always return -1 on division by zero + +expert-option bvExtractArithRewrite --bv-extract-arith bool :default false :read-write + enable rewrite pushing extract [i:0] over arithmetic operations (can blow up) + +expert-option bvAbstraction --bv-abstraction bool :default false :read-write + mcm benchmark abstraction + +expert-option skolemizeArguments --bv-skolemize bool :default false :read-write + skolemize arguments for bv abstraction (only does something if --bv-abstraction is on) + +expert-option bvNumFunc --bv-num-func=NUM unsigned :default 1 + number of function symbols in conflicts that are generalized + +expert-option bvEagerExplanations --bv-eager-explanations bool :default false :read-write + compute bit-blasting propagation explanations eagerly + +expert-option bitvectorQuickXplain --bv-quick-xplain bool :default false + minimize bv conflicts using the QuickXplain algorithm + +expert-option bvIntroducePow2 --bv-intro-pow2 bool :default false + introduce bitvector powers of two as a preprocessing pass + +endmodule |