#
# Option specification file for CVC4
# See src/options/base_options for a description of this file format
#

module UF "theory/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 /--disable-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 a cardinality to abort at (-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 ufssMinimalModel /--disable-uf-ss-min-model bool :default true
 disable finding a minimal model in 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 false
 use fair strategy for finite model finding multiple sorts

endmodule