diff options
Diffstat (limited to 'src/options/bv_options')
-rw-r--r-- | src/options/bv_options | 87 |
1 files changed, 0 insertions, 87 deletions
diff --git a/src/options/bv_options b/src/options/bv_options deleted file mode 100644 index f434339b0..000000000 --- a/src/options/bv_options +++ /dev/null @@ -1,87 +0,0 @@ -# -# 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) - -expert-option bvSatSolver bv-sat-solver --bv-sat-solver=MODE CVC4::theory::bv::SatSolverMode :predicate satSolverEnabledBuild :handler stringToSatSolver :default CVC4::theory::bv::SAT_SOLVER_MINISAT :read-write :include "options/bv_bitblast_mode.h" - choose which sat solver to use, see --bv-sat-solver=help - -option bitblastMode bitblast --bitblast=MODE CVC4::theory::bv::BitblastMode :handler stringToBitblastMode :default CVC4::theory::bv::BITBLAST_MODE_LAZY :read-write :include "options/bv_bitblast_mode.h" - choose bitblasting mode, see --bitblast=help - -# Options for eager bit-blasting - -option bitvectorAig --bitblast-aig bool :default false :predicate abcEnabledBuild setBitblastAig :read-write - bitblast by first converting to AIG (implies --bitblast=eager) -expert-option bitvectorAigSimplifications --bv-aig-simp=COMMAND std::string :default "" :predicate 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 - use bit-vector propagation in the bit-blaster - -option bitvectorEqualitySolver --bv-eq-solver bool :default true :read-write - use the equality engine for the bit-vector theory (only if --bitblast=lazy) - -option bitvectorEqualitySlicer --bv-eq-slicer=MODE CVC4::theory::bv::BvSlicerMode :handler stringToBvSlicerMode :default CVC4::theory::bv::BITVECTOR_SLICER_OFF :read-write :include "options/bv_bitblast_mode.h" :read-write :link --bv-eq-solver :link-smt 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 - turn on the inequality solver for the bit-vector theory (only if --bitblast=lazy) - -option bitvectorAlgebraicSolver --bv-algebraic-solver bool :default true :read-write - 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 :link-smt 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 boolToBitvector --bool-to-bv bool :default false :read-write - convert booleans to bit-vectors of size 1 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 - -expert-option bvGaussElim --bv-gauss-elim bool :default false - simplify formula via Gaussian Elimination if applicable - -option bvLazyRewriteExtf --bv-lazy-rewrite-extf bool :default true :read-write - lazily rewrite extended functions like bv2nat and int2bv - -option bvLazyReduceExtf --bv-lazy-reduce-extf bool :default false :read-write - reduce extended functions like bv2nat and int2bv at last call instead of full effort - -option bvAlgExtf --bv-alg-extf bool :default true :read-write - algebraic inferences for extended functions - -endmodule |