blob: c93ccf864cc98e9aca421db28b245bbcb5d5c5b5 (
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
|
#
# Option specification file for CVC4
# See src/options/base_options for a description of this file format
#
module UF "options/uf_options.h" Uninterpreted functions theory
option ufSymmetryBreaker uf-symmetry-breaker --symmetry-breaker bool :read-write :default true
use UF symmetry breaker (Deharbe et al., CADE 2011)
option condenseFunctionValues condense-function-values --condense-function-values bool :default true
condense models for functions rather than explicitly representing them
option ufssRegions --uf-ss-regions bool :default true
disable region-based method for discovering cliques and splits in uf strong solver
option ufssEagerSplits --uf-ss-eager-split bool :default false
add splits eagerly for uf strong solver
option ufssTotality --uf-ss-totality bool :default false
always use totality axioms for enforcing cardinality constraints
option ufssTotalityLimited --uf-ss-totality-limited=N int :default -1
apply totality axioms, but only up to cardinality N (-1 == do not apply totality axioms, default)
option ufssTotalitySymBreak --uf-ss-totality-sym-break bool :default false
apply symmetry breaking for totality axioms
option ufssAbortCardinality --uf-ss-abort-card=N int :default -1
tells the uf strong solver to only consider models that interpret uninterpreted sorts of cardinality at most N (-1 == no limit, default)
option ufssExplainedCliques --uf-ss-explained-cliques bool :default false
use explained clique lemmas for uf strong solver
option ufssSimpleCliques --uf-ss-simple-cliques bool :default true
always use simple clique lemmas for uf strong solver
option ufssDiseqPropagation --uf-ss-deq-prop bool :default false
eagerly propagate disequalities for uf strong solver
option ufssMode --uf-ss=MODE CVC4::theory::uf::UfssMode :default CVC4::theory::uf::UF_SS_FULL :include "options/ufss_mode.h" :handler stringToUfssMode
mode of operation for uf strong solver.
option ufssCliqueSplits --uf-ss-clique-splits bool :default false
use cliques instead of splitting on demand to shrink model
option ufssSymBreak --uf-ss-sym-break bool :default false
finite model finding symmetry breaking techniques
option ufssFairness --uf-ss-fair bool :default true
use fair strategy for finite model finding multiple sorts
option ufssFairnessMonotone --uf-ss-fair-monotone bool :read-write :default false
group monotone sorts when enforcing fairness for finite model finding
option ufHo --uf-ho bool :read-write :default false
enable support for higher-order reasoning
option ufHoExt --uf-ho-ext bool :read-write :default true
apply extensionality on function symbols
endmodule
|
