4 files changed, 43 insertions, 6 deletions
diff --git a/src/options/options_handler.cpp b/src/options/options_handler.cpp
index 6a5f6cd39..8cd651da5 100644
--- a/src/options/options_handler.cpp
+++ b/src/options/options_handler.cpp
@@ -369,6 +369,19 @@ min-s-all \n\
 + Consider only minimal subterms that meet criteria for single triggers, all otherwise. \n\
 \n\
 ";
+const std::string OptionsHandler::s_triggerActiveSelModeHelp = "\
+Trigger active selection modes currently supported by the --trigger-sel option:\n\
+\n\
+all \n\
++ Make all triggers active. \n\
+\n\
+min \n\
++ Activate triggers with minimal ground terms.\n\
+\n\
+max \n\
++ Activate triggers with maximal ground terms. \n\
+\n\
+";
 const std::string OptionsHandler::s_prenexQuantModeHelp = "\
 Prenex quantifiers modes currently supported by the --prenex-quant option:\n\
 \n\
@@ -630,9 +643,7 @@ theory::quantifiers::UserPatMode OptionsHandler::stringToUserPatMode(std::string
 }
 
 theory::quantifiers::TriggerSelMode OptionsHandler::stringToTriggerSelMode(std::string option, std::string optarg) throw(OptionException) {
-  if(optarg ==  "default") {
-    return theory::quantifiers::TRIGGER_SEL_DEFAULT;
-  } else if(optarg == "min") {
+  if(optarg ==  "default" || optarg == "min") {
     return theory::quantifiers::TRIGGER_SEL_MIN;
   } else if(optarg == "max") {
     return theory::quantifiers::TRIGGER_SEL_MAX;
@@ -651,6 +662,21 @@ theory::quantifiers::TriggerSelMode OptionsHandler::stringToTriggerSelMode(std::
   }
 }
 
+theory::quantifiers::TriggerActiveSelMode OptionsHandler::stringToTriggerActiveSelMode(std::string option, std::string optarg) throw(OptionException) {
+  if(optarg ==  "default" || optarg == "all") {
+    return theory::quantifiers::TRIGGER_ACTIVE_SEL_ALL;
+  } else if(optarg == "min") {
+    return theory::quantifiers::TRIGGER_ACTIVE_SEL_MIN;
+  } else if(optarg == "max") {
+    return theory::quantifiers::TRIGGER_ACTIVE_SEL_MAX;
+  } else if(optarg ==  "help") {
+    puts(s_triggerActiveSelModeHelp.c_str());
+    exit(1);
+  } else {
+    throw OptionException(std::string("unknown option for --trigger-active-sel: `") +
+                          optarg + "'.  Try --trigger-active-sel help.");
+  }
+}
 
 theory::quantifiers::PrenexQuantMode OptionsHandler::stringToPrenexQuantMode(std::string option, std::string optarg) throw(OptionException) {
   if(optarg ==  "default" ) {
diff --git a/src/options/options_handler.h b/src/options/options_handler.h
index 5db2887c0..e327b9c8e 100644
--- a/src/options/options_handler.h
+++ b/src/options/options_handler.h
@@ -94,6 +94,7 @@ public:
   theory::quantifiers::QcfMode stringToQcfMode(std::string option, std::string optarg) throw(OptionException);
   theory::quantifiers::UserPatMode stringToUserPatMode(std::string option, std::string optarg) throw(OptionException);
   theory::quantifiers::TriggerSelMode stringToTriggerSelMode(std::string option, std::string optarg) throw(OptionException);
+  theory::quantifiers::TriggerActiveSelMode stringToTriggerActiveSelMode(std::string option, std::string optarg) throw(OptionException);
   theory::quantifiers::PrenexQuantMode stringToPrenexQuantMode(std::string option, std::string optarg) throw(OptionException);
   theory::quantifiers::CegqiFairMode stringToCegqiFairMode(std::string option, std::string optarg) throw(OptionException);
   theory::quantifiers::TermDbMode stringToTermDbMode(std::string option, std::string optarg) throw(OptionException);
@@ -221,6 +222,7 @@ public:
   static const std::string s_termDbModeHelp;
   static const std::string s_theoryOfModeHelp;
   static const std::string s_triggerSelModeHelp;
+  static const std::string s_triggerActiveSelModeHelp;
   static const std::string s_ufssModeHelp;
   static const std::string s_userPatModeHelp;
   static const std::string s_errorSelectionRulesHelp;
diff --git a/src/options/quantifiers_modes.h b/src/options/quantifiers_modes.h
index 65445be17..fe76f8798 100644
--- a/src/options/quantifiers_modes.h
+++ b/src/options/quantifiers_modes.h
@@ -101,8 +101,6 @@ enum UserPatMode {
 };
 
 enum TriggerSelMode {
-  /** default for trigger selection */
-  TRIGGER_SEL_DEFAULT,
   /** only consider minimal terms for triggers */
   TRIGGER_SEL_MIN,
   /** only consider maximal terms for triggers */
@@ -115,6 +113,15 @@ enum TriggerSelMode {
   TRIGGER_SEL_ALL,
 };
 
+enum TriggerActiveSelMode {
+  /** always use all triggers */
+  TRIGGER_ACTIVE_SEL_ALL,
+  /** only use triggers with minimal # of ground terms */
+  TRIGGER_ACTIVE_SEL_MIN,
+  /** only use triggers with maximal # of ground terms */
+  TRIGGER_ACTIVE_SEL_MAX,
+};
+
 enum CVC4_PUBLIC PrenexQuantMode {
   /** default : prenex quantifiers without user patterns */
   PRENEX_NO_USER_PAT,
diff --git a/src/options/quantifiers_options b/src/options/quantifiers_options
index 980179378..0b5474959 100644
--- a/src/options/quantifiers_options
+++ b/src/options/quantifiers_options
@@ -89,8 +89,10 @@ option multiTriggerWhenSingle --multi-trigger-when-single bool :default false
  select multi triggers when single triggers exist
 option multiTriggerPriority --multi-trigger-priority bool :default false
  only try multi triggers if single triggers give no instantiations
-option triggerSelMode --trigger-sel CVC4::theory::quantifiers::TriggerSelMode :default CVC4::theory::quantifiers::TRIGGER_SEL_DEFAULT :read-write :include "options/quantifiers_modes.h" :handler  stringToTriggerSelMode
+option triggerSelMode --trigger-sel CVC4::theory::quantifiers::TriggerSelMode :default CVC4::theory::quantifiers::TRIGGER_SEL_MIN :read-write :include "options/quantifiers_modes.h" :handler  stringToTriggerSelMode
  selection mode for triggers
+option triggerActiveSelMode --trigger-active-sel CVC4::theory::quantifiers::TriggerActiveSelMode :default CVC4::theory::quantifiers::TRIGGER_ACTIVE_SEL_ALL :read-write :include "options/quantifiers_modes.h" :handler stringToTriggerActiveSelMode
+ selection mode to activate triggers
 option userPatternsQuant --user-pat=MODE CVC4::theory::quantifiers::UserPatMode :default CVC4::theory::quantifiers::USER_PAT_MODE_TRUST :read-write :include "options/quantifiers_modes.h" :handler stringToUserPatMode
  policy for handling user-provided patterns for quantifier instantiation
 option incrementTriggers --increment-triggers bool :default true