1 files changed, 43 insertions, 0 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)
 {