blob: f434339b05149979cf4e400c94796378e5b57993 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
|
#
# 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
|
