diff options
Diffstat (limited to 'src/theory/uf/options')
| -rw-r--r-- | src/theory/uf/options | 18 |
1 files changed, 18 insertions, 0 deletions
diff --git a/src/theory/uf/options b/src/theory/uf/options index 6f6900da0..8185f0b3d 100644 --- a/src/theory/uf/options +++ b/src/theory/uf/options @@ -9,4 +9,22 @@ option ufSymmetryBreaker uf-symmetry-breaker --enable-symmetry-breaker/--disable 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 + + endmodule |