diff options
| author | Liana Hadarean <lianahady@gmail.com> | 2016-01-26 16:04:26 -0800 |
|---|---|---|
| committer | Liana Hadarean <lianahady@gmail.com> | 2016-01-26 16:04:26 -0800 |
| commit | 42b665f2a00643c81b42932fab1441987628c5a5 (patch) | |
| tree | aa851e1fc4828f5a4d94ce0c11fa6d2d1199636f /src/options | |
| parent | 7006d5ba2f68c01638a2ab2c98a86b41dcf4467c (diff) | |
Merged bit-vector and uf proof branch.
Diffstat (limited to 'src/options')
| -rw-r--r-- | src/options/bv_options | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/src/options/bv_options b/src/options/bv_options index 73790b562..245c56b51 100644 --- a/src/options/bv_options +++ b/src/options/bv_options @@ -19,19 +19,19 @@ expert-option bitvectorAigSimplifications --bv-aig-simp=COMMAND std::string :def # Options for lazy bit-blasting -option bitvectorPropagate --bv-propagate bool :default true :read-write :link --bitblast=lazy +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 :link --bitblast=lazy +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 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 +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 :link --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 |