blob: d90d8f69302fcbc18fe8770dc8bbefde3498055d (
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
|
id = "UF"
name = "Uninterpreted Functions Theory"
[[option]]
name = "ufSymmetryBreaker"
alias = ["uf-symmetry-breaker"]
category = "regular"
long = "symmetry-breaker"
type = "bool"
default = "true"
help = "use UF symmetry breaker (Deharbe et al., CADE 2011)"
[[option]]
name = "ufssTotalityLimited"
category = "regular"
long = "uf-ss-totality-limited=N"
type = "int64_t"
default = "-1"
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"
help = "apply symmetry breaking for totality axioms"
[[option]]
name = "ufssAbortCardinality"
category = "regular"
long = "uf-ss-abort-card=N"
type = "int64_t"
default = "-1"
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"
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"
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"
|
