diff options
| author | ajreynol <andrew.j.reynolds@gmail.com> | 2014-09-24 14:35:39 +0200 |
|---|---|---|
| committer | ajreynol <andrew.j.reynolds@gmail.com> | 2014-09-24 14:35:39 +0200 |
| commit | 4d7329f72720e884a6161dcdeb8d377d19031930 (patch) | |
| tree | a7abfb27090710a45a2b86c7654afd95fbfc0028 /src/theory/uf/options | |
| parent | cb1c193049fc8ac1bf5522fc6a114e9a804039a3 (diff) | |
Refactor option for uf+cardinality constraints solver.
Diffstat (limited to 'src/theory/uf/options')
| -rw-r--r-- | src/theory/uf/options | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/src/theory/uf/options b/src/theory/uf/options index 26f87da79..d9e4c9477 100644 --- a/src/theory/uf/options +++ b/src/theory/uf/options @@ -29,8 +29,8 @@ 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 ufssMinimalModel /--disable-uf-ss-min-model bool :default true - disable finding a minimal model in 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 |