4 files changed, 64 insertions, 5 deletions
diff --git a/src/options/options_handler.cpp b/src/options/options_handler.cpp
index 22d944e4c..6eed732e2 100644
--- a/src/options/options_handler.cpp
+++ b/src/options/options_handler.cpp
@@ -525,6 +525,21 @@ post \n\
 \n\
 ";
 
+const std::string OptionsHandler::s_sygusActiveGenHelp =
+    "\
+Modes for actively-generated sygus enumerators, supported by --sygus-active-gen:\n\
+\n\
+none  \n\
++ Do not use actively-generated sygus enumerators.\n\
+\n\
+basic  \n\
++ Use basic type enumerator as sygus enumerator.\n\
+\n\
+var-agnostic \n\
++ Use sygus solver to enumerate terms that are agnostic to variables. \n\
+\n\
+";
+
 const std::string OptionsHandler::s_macrosQuantHelp = "\
 Modes for quantifiers macro expansion, supported by --macros-quant-mode:\n\
 \n\
@@ -952,6 +967,34 @@ OptionsHandler::stringToSygusInvTemplMode(std::string option,
   }
 }
 
+theory::quantifiers::SygusActiveGenMode
+OptionsHandler::stringToSygusActiveGenMode(std::string option,
+                                           std::string optarg)
+{
+  if (optarg == "none")
+  {
+    return theory::quantifiers::SYGUS_ACTIVE_GEN_NONE;
+  }
+  else if (optarg == "basic")
+  {
+    return theory::quantifiers::SYGUS_ACTIVE_GEN_BASIC;
+  }
+  else if (optarg == "var-agnostic")
+  {
+    return theory::quantifiers::SYGUS_ACTIVE_GEN_VAR_AGNOSTIC;
+  }
+  else if (optarg == "help")
+  {
+    puts(s_sygusActiveGenHelp.c_str());
+    exit(1);
+  }
+  else
+  {
+    throw OptionException(std::string("unknown option for --sygus-inv-templ: `")
+                          + optarg + "'.  Try --sygus-inv-templ help.");
+  }
+}
+
 theory::quantifiers::MacrosQuantMode OptionsHandler::stringToMacrosQuantMode(
     std::string option, std::string optarg)
 {
diff --git a/src/options/options_handler.h b/src/options/options_handler.h
index 1869dc6a0..0205b0b73 100644
--- a/src/options/options_handler.h
+++ b/src/options/options_handler.h
@@ -114,6 +114,8 @@ public:
       std::string option, std::string optarg);
   theory::quantifiers::SygusInvTemplMode stringToSygusInvTemplMode(
       std::string option, std::string optarg);
+  theory::quantifiers::SygusActiveGenMode stringToSygusActiveGenMode(
+      std::string option, std::string optarg);
   theory::quantifiers::MacrosQuantMode stringToMacrosQuantMode(
       std::string option, std::string optarg);
   theory::quantifiers::QuantDSplitMode stringToQuantDSplitMode(
@@ -245,6 +247,7 @@ public:
   static const std::string s_cegqiSingleInvRconsHelp;
   static const std::string s_cegisSampleHelp;
   static const std::string s_sygusInvTemplHelp;
+  static const std::string s_sygusActiveGenHelp;
   static const std::string s_termDbModeHelp;
   static const std::string s_theoryOfModeHelp;
   static const std::string s_triggerSelModeHelp;
diff --git a/src/options/quantifiers_modes.h b/src/options/quantifiers_modes.h
index 1fd29340d..42ab7bc06 100644
--- a/src/options/quantifiers_modes.h
+++ b/src/options/quantifiers_modes.h
@@ -262,6 +262,16 @@ enum SygusInvTemplMode {
   SYGUS_INV_TEMPL_MODE_POST,
 };
 
+enum SygusActiveGenMode
+{
+  /** do not use actively-generated enumerators */
+  SYGUS_ACTIVE_GEN_NONE,
+  /** use basic actively-generated enumerators */
+  SYGUS_ACTIVE_GEN_BASIC,
+  /** use variable-agnostic enumerators */
+  SYGUS_ACTIVE_GEN_VAR_AGNOSTIC,
+};
+
 enum MacrosQuantMode {
   /** infer all definitions */
   MACROS_QUANT_MODE_ALL,
diff --git a/src/options/quantifiers_options.toml b/src/options/quantifiers_options.toml
index eb32beef5..cbc380f43 100644
--- a/src/options/quantifiers_options.toml
+++ b/src/options/quantifiers_options.toml
@@ -1032,12 +1032,15 @@ header = "options/quantifiers_options.h"
   help       = "timeout (in milliseconds) for the satisfiability check to repair constants in sygus candidate solutions"
 
 [[option]]
-  name       = "sygusEnumVarAgnostic"
+  name       = "sygusActiveGenMode"
   category   = "regular"
-  long       = "sygus-var-agnostic"
-  type       = "bool"
-  default    = "false"
-  help       = "when possible, use variable-agnostic enumerators"
+  long       = "sygus-active-gen=MODE"
+  type       = "CVC4::theory::quantifiers::SygusActiveGenMode"
+  default    = "CVC4::theory::quantifiers::SYGUS_ACTIVE_GEN_NONE"
+  handler    = "stringToSygusActiveGenMode"
+  includes   = ["options/quantifiers_modes.h"]
+  read_only  = true
+  help       = "mode for actively-generated sygus enumerators"
 
 [[option]]
   name       = "sygusMinGrammar"