merge from fmf-devel branch. more updates to models: now with collectModelInfo with fullModel argument, most theory-specific implementation out of the model class, model printer relegated to printer classes. Also updates to finite mode finding, modifications to datatypes making them compatible with theory combination, support for theory-specific handling of user attributes, refactoring of uf models

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