Rename UF with cardinality extension (#3241)

3 files changed, 23 insertions, 28 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\
 ";
 
diff --git a/src/options/uf_options.toml b/src/options/uf_options.toml
index e0c34127a..8790e4ec3 100644
--- a/src/options/uf_options.toml
+++ b/src/options/uf_options.toml
@@ -12,24 +12,6 @@ header = "options/uf_options.h"
   help       = "use UF symmetry breaker (Deharbe et al., CADE 2011)"
 
 [[option]]
-  name       = "ufssRegions"
-  category   = "regular"
-  long       = "uf-ss-regions"
-  type       = "bool"
-  default    = "true"
-  read_only  = true
-  help       = "disable region-based method for discovering cliques and splits in uf strong solver"
-
-[[option]]
-  name       = "ufssEagerSplits"
-  category   = "regular"
-  long       = "uf-ss-eager-split"
-  type       = "bool"
-  default    = "false"
-  read_only  = true
-  help       = "add splits eagerly for uf strong solver"
-
-[[option]]
   name       = "ufssTotality"
   category   = "regular"
   long       = "uf-ss-totality"
@@ -63,7 +45,7 @@ header = "options/uf_options.h"
   type       = "int"
   default    = "-1"
   read_only  = true
-  help       = "tells the uf strong solver to only consider models that interpret uninterpreted sorts of cardinality at most N (-1 == no limit, default)"
+  help       = "tells the uf with cardinality to only consider models that interpret uninterpreted sorts of cardinality at most N (-1 == no limit, default)"
 
 [[option]]
   name       = "ufssMode"
@@ -74,7 +56,7 @@ header = "options/uf_options.h"
   handler    = "stringToUfssMode"
   includes   = ["options/ufss_mode.h"]
   read_only  = true
-  help       = "mode of operation for uf strong solver."
+  help       = "mode of operation for uf with cardinality solver."
 
 [[option]]
   name       = "ufssFairness"
diff --git a/src/options/ufss_mode.h b/src/options/ufss_mode.h
index d6a106ecf..452317b8f 100644
--- a/src/options/ufss_mode.h
+++ b/src/options/ufss_mode.h
@@ -23,12 +23,23 @@ namespace CVC4 {
 namespace theory {
 namespace uf {
 
-enum UfssMode{
-  /** default, use uf strong solver to find minimal models for uninterpreted sorts */
+/**
+ * These modes determine the role of UF with cardinality when using finite model
+ * finding (--finite-model-find).
+ */
+enum UfssMode
+{
+  /**
+   * Default, use UF with cardinality to find minimal models for uninterpreted
+   * sorts.
+   */
   UF_SS_FULL,
-  /** use uf strong solver to shrink model sizes, but do no enforce minimality */
+  /**
+   * Use UF with cardinality to shrink model sizes, but do no enforce
+   * minimality.
+   */
   UF_SS_NO_MINIMAL,
-  /** do not use uf strong solver */
+  /** do not use UF with cardinality */
   UF_SS_NONE,
 };