diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2014-01-03 22:36:55 -0600 |
---|---|---|
committer | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2014-01-03 22:36:55 -0600 |
commit | 2ce92038d8455637e313a1c2d0ce5d31a3d42b10 (patch) | |
tree | ce599c2e981bbd79d024e90cff6e97468b42712b /src/theory/uf/options | |
parent | 93f084750d8a76d63fc74d242944bce0635c2194 (diff) |
Removing and consolidating options for uf-ss and quantifiers. Bug fix for inst gen-style MBQI.
Diffstat (limited to 'src/theory/uf/options')
-rw-r--r-- | src/theory/uf/options | 6 |
1 files changed, 0 insertions, 6 deletions
diff --git a/src/theory/uf/options b/src/theory/uf/options index cfa6e6c04..26f87da79 100644 --- a/src/theory/uf/options +++ b/src/theory/uf/options @@ -15,20 +15,14 @@ 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 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 ufssTotalityLazy --uf-ss-totality-lazy bool :default false - apply totality axioms lazily 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 ufssSmartSplits --uf-ss-smart-split bool :default false - use smart splitting heuristic for uf strong solver 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 |