blob: e0c34127a213856c5e6e2303b6f230fc9a07cebb (
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
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
|
id = "UF"
name = "Uninterpreted functions theory"
header = "options/uf_options.h"
[[option]]
name = "ufSymmetryBreaker"
smt_name = "uf-symmetry-breaker"
category = "regular"
long = "symmetry-breaker"
type = "bool"
default = "true"
help = "use UF symmetry breaker (Deharbe et al., CADE 2011)"
[[option]]
name = "ufssRegions"
category = "regular"
long = "uf-ss-regions"
type = "bool"
default = "true"
read_only = true
help = "disable region-based method for discovering cliques and splits in uf strong solver"
[[option]]
name = "ufssEagerSplits"
category = "regular"
long = "uf-ss-eager-split"
type = "bool"
default = "false"
read_only = true
help = "add splits eagerly for uf strong solver"
[[option]]
name = "ufssTotality"
category = "regular"
long = "uf-ss-totality"
type = "bool"
default = "false"
read_only = true
help = "always use totality axioms for enforcing cardinality constraints"
[[option]]
name = "ufssTotalityLimited"
category = "regular"
long = "uf-ss-totality-limited=N"
type = "int"
default = "-1"
read_only = true
help = "apply totality axioms, but only up to cardinality N (-1 == do not apply totality axioms, default)"
[[option]]
name = "ufssTotalitySymBreak"
category = "regular"
long = "uf-ss-totality-sym-break"
type = "bool"
default = "false"
read_only = true
help = "apply symmetry breaking for totality axioms"
[[option]]
name = "ufssAbortCardinality"
category = "regular"
long = "uf-ss-abort-card=N"
type = "int"
default = "-1"
read_only = true
help = "tells the uf strong solver to only consider models that interpret uninterpreted sorts of cardinality at most N (-1 == no limit, default)"
[[option]]
name = "ufssMode"
category = "regular"
long = "uf-ss=MODE"
type = "CVC4::theory::uf::UfssMode"
default = "CVC4::theory::uf::UF_SS_FULL"
handler = "stringToUfssMode"
includes = ["options/ufss_mode.h"]
read_only = true
help = "mode of operation for uf strong solver."
[[option]]
name = "ufssFairness"
category = "regular"
long = "uf-ss-fair"
type = "bool"
default = "true"
read_only = true
help = "use fair strategy for finite model finding multiple sorts"
[[option]]
name = "ufssFairnessMonotone"
category = "regular"
long = "uf-ss-fair-monotone"
type = "bool"
default = "false"
help = "group monotone sorts when enforcing fairness for finite model finding"
[[option]]
name = "ufHo"
category = "regular"
long = "uf-ho"
type = "bool"
default = "false"
help = "enable support for higher-order reasoning"
[[option]]
name = "ufHoExt"
category = "regular"
long = "uf-ho-ext"
type = "bool"
default = "true"
help = "apply extensionality on function symbols"
|
