diff options
Diffstat (limited to 'src/options/uf_options')
| -rw-r--r-- | src/options/uf_options | 42 |
1 files changed, 42 insertions, 0 deletions
diff --git a/src/options/uf_options b/src/options/uf_options new file mode 100644 index 000000000..baea1cb41 --- /dev/null +++ b/src/options/uf_options @@ -0,0 +1,42 @@ +# +# 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 /--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 ufssMode --uf-ss=MODE CVC4::theory::uf::UfssMode :default CVC4::theory::uf::UF_SS_FULL :include "options/options_handler_interface.h" :handler CVC4::options::stringToUfssMode :handler-include "options/options_handler_interface.h" + 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 + +endmodule |