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
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
|
#
# Option specification file for CVC4
# See src/options/base_options for a description of this file format
#
module ARITH "options/arith_options.h" Arithmetic theory
option arithUnateLemmaMode --unate-lemmas=MODE ArithUnateLemmaMode :handler stringToArithUnateLemmaMode :default ALL_PRESOLVE_LEMMAS :include "options/arith_unate_lemma_mode.h"
determines which lemmas to add before solving (default is 'all', see --unate-lemmas=help)
option arithPropagationMode --arith-prop=MODE ArithPropagationMode :handler stringToArithPropagationMode :default BOTH_PROP :include "options/arith_propagation_mode.h"
turns on arithmetic propagation (default is 'old', see --arith-prop=help)
# The maximum number of difference pivots to do per invocation of simplex.
# If this is negative, the number of pivots done is the number of variables.
# If this is not set by the user, different logics are free to chose different
# defaults.
option arithHeuristicPivots --heuristic-pivots=N int16_t :default 0 :read-write
the number of times to apply the heuristic pivot rule; if N < 0, this defaults to the number of variables; if this is unset, this is tuned by the logic selection
# The maximum number of variable order pivots to do per invocation of simplex.
# If this is negative, the number of pivots done is unlimited.
# If this is not set by the user, different logics are free to chose different
# defaults.
expert-option arithStandardCheckVarOrderPivots --standard-effort-variable-order-pivots=N int16_t :default -1 :read-write
limits the number of pivots in a single invocation of check() at a non-full effort level using Bland's pivot rule
option arithErrorSelectionRule --error-selection-rule=RULE ErrorSelectionRule :handler stringToErrorSelectionRule :default MINIMUM_AMOUNT :include "options/arith_heuristic_pivot_rule.h"
change the pivot rule for the basic variable (default is 'min', see --pivot-rule help)
# The number of pivots before simplex rechecks every basic variable for a conflict
option arithSimplexCheckPeriod --simplex-check-period=N uint16_t :default 200
the number of pivots to do in simplex before rechecking for a conflict on all variables
# This is the pivots per basic variable that can be done using heuristic choices
# before variable order must be used.
# If this is not set by the user, different logics are free to chose different
# defaults.
option arithPivotThreshold --pivot-threshold=N uint16_t :default 2 :read-write
sets the number of pivots using --pivot-rule per basic variable per simplex instance before using variable order
option arithPropagateMaxLength --prop-row-length=N uint16_t :default 16
sets the maximum row length to be used in propagation
option arithDioSolver --enable-dio-solver/--disable-dio-solver bool :default true
turns on Linear Diophantine Equation solver (Griggio, JSAT 2012)
/turns off Linear Diophantine Equation solver (Griggio, JSAT 2012)
# Whether to split (= x y) into (and (<= x y) (>= x y)) in
# arithmetic preprocessing.
option arithRewriteEq --enable-arith-rewrite-equalities/--disable-arith-rewrite-equalities bool :default false :read-write
turns on the preprocessing rewrite turning equalities into a conjunction of inequalities
/turns off the preprocessing rewrite turning equalities into a conjunction of inequalities
option arithMLTrick miplib-trick --enable-miplib-trick/--disable-miplib-trick bool :default false
turns on the preprocessing step of attempting to infer bounds on miplib problems
/turns off the preprocessing step of attempting to infer bounds on miplib problems
option arithMLTrickSubstitutions miplib-trick-subs --miplib-trick-subs=N unsigned :default 1
do substitution for miplib 'tmp' vars if defined in <= N eliminated vars
option doCutAllBounded --cut-all-bounded bool :default false :read-write
turns on the integer solving step of periodically cutting all integer variables that have both upper and lower bounds
/turns off the integer solving step of periodically cutting all integer variables that have both upper and lower bounds
option maxCutsInContext --maxCutsInContext unsigned :default 65535
maximum cuts in a given context before signalling a restart
option revertArithModels --revert-arith-models-on-unsat bool :default false
revert the arithmetic model to a known safe model on unsat if one is cached
option havePenalties --fc-penalties bool :default false :read-write
turns on degenerate pivot penalties
/turns off degenerate pivot penalties
option useFC --use-fcsimplex bool :default false :read-write
use focusing and converging simplex (FMCAD 2013 submission)
option useSOI --use-soi bool :default false :read-write
use sum of infeasibility simplex (FMCAD 2013 submission)
option restrictedPivots --restrict-pivots bool :default true :read-write
have a pivot cap for simplex at effort levels below fullEffort
option collectPivots --collect-pivot-stats bool :default false :read-write
collect the pivot history
option useApprox --use-approx bool :default false :read-write
attempt to use an approximate solver
option maxApproxDepth --approx-branch-depth int16_t :default 200 :read-write
maximum branch depth the approximate solver is allowed to take
option exportDioDecompositions --dio-decomps bool :default false :read-write
let skolem variables for integer divisibility constraints leak from the dio solver
option newProp --new-prop bool :default false :read-write
use the new row propagation system
option arithPropAsLemmaLength --arith-prop-clauses uint16_t :default 8 :read-write
rows shorter than this are propagated as clauses
option soiQuickExplain --soi-qe bool :default false :read-write
use quick explain to minimize the sum of infeasibility conflicts
option rewriteDivk rewrite-divk --rewrite-divk bool :default false :read-write
rewrite division and mod when by a constant into linear terms
option trySolveIntStandardEffort --se-solve-int bool :default false
attempt to use the approximate solve integer method on standard effort
option replayFailureLemma --lemmas-on-replay-failure bool :default false
attempt to use external lemmas if approximate solve integer failed
option dioSolverTurns --dio-turns int :default 10
turns in a row dio solver cutting gets
option rrTurns --rr-turns int :default 3
round robin turn
option dioRepeat --dio-repeat bool :default false
handle dio solver constraints in mass or one at a time
option replayEarlyCloseDepths --replay-early-close-depth int :default 1
multiples of the depths to try to close the approx log eagerly
option replayFailurePenalty --replay-failure-penalty int :default 100
number of solve integer attempts to skips after a numeric failure
option replayNumericFailurePenalty --replay-num-err-penalty int :default 4194304
number of solve integer attempts to skips after a numeric failure
option replayRejectCutSize --replay-reject-cut unsigned :default 25500
maximum complexity of any coefficient while replaying cuts
option lemmaRejectCutSize --replay-lemma-reject-cut unsigned :default 25500
maximum complexity of any coefficient while outputting replaying cut lemmas
option soiApproxMajorFailure --replay-soi-major-threshold double :default .01
threshold for a major tolerance failure by the approximate solver
option soiApproxMajorFailurePen --replay-soi-major-threshold-pen int :default 50
threshold for a major tolerance failure by the approximate solver
option soiApproxMinorFailure --replay-soi-minor-threshold double :default .0001
threshold for a minor tolerance failure by the approximate solver
option soiApproxMinorFailurePen --replay-soi-minor-threshold-pen int :default 10
threshold for a minor tolerance failure by the approximate solver
option ppAssertMaxSubSize --pp-assert-max-sub-size unsigned :default 2
threshold for substituting an equality in ppAssert
option maxReplayTree --max-replay-tree int :default 512
threshold for attempting to replay a tree
option pbRewrites --pb-rewrites bool :default false
apply pseudo boolean rewrites
option pbRewriteThreshold --pb-rewrite-threshold int :default 256
threshold of number of pseudoboolean variables to have before doing rewrites
option sNormInferEq --snorm-infer-eq bool :default false
infer equalities based on Shostak normalization
option nlAlg --nl-alg bool :default false
algebraic approach to non-linear
option nlAlgResBound --nl-alg-rbound bool :default false
use resolution-style inference for inferring new bounds
option nlAlgTangentPlanes --nl-alg-tplanes bool :default false
use non-terminating tangent plane strategy for non-linear
option nlAlgEntailConflicts --nl-alg-ent-conf bool :default false
check for entailed conflicts in non-linear solver
option nlAlgRewrites --nl-alg-rewrite bool :default true
do rewrites in non-linear solver
option nlAlgSolveSubs --nl-alg-solve-subs bool :default true
do solving for determining constant substitutions
option nlAlgPurify --nl-alg-purify bool :default false
purify non-linear terms at preprocess
option nlAlgSplitZero --nl-alg-split-zero bool :default false
intial splits on zero for all variables
endmodule
|
