blob: 6916598ce7744eedb1755c13004f31d3451f2fe5 (
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
|
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 = "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 with cardinality 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 = "UfssMode"
default = "FULL"
read_only = true
help = "mode of operation for uf with cardinality solver."
help_mode = "UF with cardinality options currently supported by the --uf-ss option when combined with finite model finding."
[[option.mode.FULL]]
name = "full"
help = "Default, use UF with cardinality to find minimal models for uninterpreted sorts."
[[option.mode.NO_MINIMAL]]
name = "no-minimal"
help = "Use UF with cardinality to shrink models, but do no enforce minimality."
[[option.mode.NONE]]
name = "none"
help = "Do not use UF with cardinality to shrink model sizes."
[[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"
|