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