blob: 8b45a6da237e08eee9c52fc0d826f9d46dbc6a52 (
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
|
#
# Option specification file for CVC4
# See src/options/base_options for a description of this file format
#
module ARITH "theory/arith/options.h" Arithmetic theory
option arithUnateLemmaMode --unate-lemmas=MODE ArithUnateLemmaMode :handler CVC4::theory::arith::stringToArithUnateLemmaMode :default ALL_PRESOLVE_LEMMAS :handler-include "theory/arith/options_handlers.h" :include "theory/arith/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 CVC4::theory::arith::stringToArithPropagationMode :default BOTH_PROP :handler-include "theory/arith/options_handlers.h" :include "theory/arith/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 arithHeuristicPivotRule --heuristic-pivot-rule=RULE ArithHeuristicPivotRule :handler CVC4::theory::arith::stringToArithHeuristicPivotRule :default MINIMUM :handler-include "theory/arith/options_handlers.h" :include "theory/arith/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 /--disable-dio-solver bool :default true
use 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
endmodule
|
