#
# 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 --enable-symmetry-breaker/--disable-symmetry-breaker bool :read-write :default true
 use UF symmetry breaker (Deharbe et al., CADE 2011)
/turns off UF symmetry breaker (Deharbe et al., CADE 2011)

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 ufssColoringSat --uf-ss-coloring-sat bool :default false
 use coloring-based SAT heuristic for uf strong solver
option ufssTotality --uf-ss-totality bool :default false
 use totality axioms for enforcing cardinality constraints
option ufssTotalityLazy --uf-ss-totality-lazy bool :default false
 apply totality axioms lazily
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 ufssSmartSplits --uf-ss-smart-split bool :default false
 use smart splitting heuristic for uf strong solver
option ufssModelInference --uf-ss-model-infer bool :default false
 use model inference method for uf strong solver
option ufssSimpleCliques --uf-ss-simple-cliques bool :default false
 add simple clique lemmas for uf strong solver

endmodule