diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2019-09-12 18:35:57 -0500 |
---|---|---|
committer | GitHub <noreply@github.com> | 2019-09-12 18:35:57 -0500 |
commit | f62cb035e728c77facc94c5dfe3a8a2df65aa3a7 (patch) | |
tree | 20e8c8bdb3d89951596290c437266175bb30852b /src/options/options_handler.cpp | |
parent | a117e2b45539a822aa480b90558c2c0da6031dd9 (diff) |
Rename UF with cardinality extension (#3241)
Diffstat (limited to 'src/options/options_handler.cpp')
-rw-r--r-- | src/options/options_handler.cpp | 10 |
1 files changed, 6 insertions, 4 deletions
diff --git a/src/options/options_handler.cpp b/src/options/options_handler.cpp index 874c57629..e838988c9 100644 --- a/src/options/options_handler.cpp +++ b/src/options/options_handler.cpp @@ -1587,16 +1587,18 @@ void OptionsHandler::setBitblastAig(std::string option, bool arg) // theory/uf/options_handlers.h const std::string OptionsHandler::s_ufssModeHelp = "\ -UF strong solver options currently supported by the --uf-ss option:\n\ +UF with cardinality options currently supported by the --uf-ss option when\n\ +combined with finite model finding:\n\ \n\ full \n\ -+ Default, use uf strong solver to find minimal models for uninterpreted sorts.\n\ ++ Default, use UF with cardinality to find minimal models for uninterpreted\n\ +sorts.\n\ \n\ no-minimal \n\ -+ Use uf strong solver to shrink model sizes, but do no enforce minimality.\n\ ++ Use UF with cardinality to shrink models, but do no enforce minimality.\n\ \n\ none \n\ -+ Do not use uf strong solver to shrink model sizes. \n\ ++ Do not use UF with cardinality to shrink model sizes. \n\ \n\ "; |