blob: 34d4eeefcb651af800aa6ccf70c45af0a57c763d (
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
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
|
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 = "condenseFunctionValues"
category = "regular"
long = "condense-function-values"
type = "bool"
default = "true"
read_only = true
help = "condense models for functions rather than explicitly representing them"
[[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 = "ufssExplainedCliques"
category = "regular"
long = "uf-ss-explained-cliques"
type = "bool"
default = "false"
read_only = true
help = "use explained clique lemmas for uf strong solver"
[[option]]
name = "ufssSimpleCliques"
category = "regular"
long = "uf-ss-simple-cliques"
type = "bool"
default = "true"
read_only = true
help = "always use simple clique lemmas for uf strong solver"
[[option]]
name = "ufssDiseqPropagation"
category = "regular"
long = "uf-ss-deq-prop"
type = "bool"
default = "false"
read_only = true
help = "eagerly propagate disequalities for uf strong solver"
[[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 = "ufssCliqueSplits"
category = "regular"
long = "uf-ss-clique-splits"
type = "bool"
default = "false"
read_only = true
help = "use cliques instead of splitting on demand to shrink model"
[[option]]
name = "ufssSymBreak"
category = "regular"
long = "uf-ss-sym-break"
type = "bool"
default = "false"
read_only = true
help = "finite model finding symmetry breaking techniques"
[[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"
|
