diff options
Diffstat (limited to 'src/theory/uf/options')
| -rw-r--r-- | src/theory/uf/options | 5 |
1 files changed, 5 insertions, 0 deletions
diff --git a/src/theory/uf/options b/src/theory/uf/options index bed535342..437e30e46 100644 --- a/src/theory/uf/options +++ b/src/theory/uf/options @@ -23,6 +23,8 @@ 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 @@ -35,5 +37,8 @@ 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 + endmodule |