Add optimized sygus enumeration (#2677)

1 files changed, 9 insertions, 2 deletions

diff --git a/src/options/options_handler.cpp b/src/options/options_handler.cpp
index 46663ce7c..e4c0276ea 100644
--- a/src/options/options_handler.cpp
+++ b/src/options/options_handler.cpp
@@ -530,7 +530,10 @@ none  \n\
 + Do not use actively-generated sygus enumerators.\n\
 \n\
 basic  \n\
-+ Use basic type enumerator as sygus enumerator.\n\
++ Use basic type enumerator for actively-generated sygus enumerators.\n\
+\n\
+enum  \n\
++ Use optimized enumerator for actively-generated sygus enumerators.\n\
 \n\
 var-agnostic \n\
 + Use sygus solver to enumerate terms that are agnostic to variables. \n\
@@ -974,7 +977,11 @@ OptionsHandler::stringToSygusActiveGenMode(std::string option,
   }
   else if (optarg == "basic")
   {
-    return theory::quantifiers::SYGUS_ACTIVE_GEN_BASIC;
+    return theory::quantifiers::SYGUS_ACTIVE_GEN_ENUM_BASIC;
+  }
+  else if (optarg == "enum")
+  {
+    return theory::quantifiers::SYGUS_ACTIVE_GEN_ENUM;
   }
   else if (optarg == "var-agnostic")
   {