Improvements to trigger selection, min triggers by default. Optimizations for E-matching. Minor work to equality infer.

2 files changed, 5 insertions, 1 deletions

diff --git a/src/options/options_handler.cpp b/src/options/options_handler.cpp
index 152e22f14..8a5bacf91 100644
--- a/src/options/options_handler.cpp
+++ b/src/options/options_handler.cpp
@@ -602,12 +602,14 @@ theory::quantifiers::UserPatMode OptionsHandler::stringToUserPatMode(std::string
 }
 
 theory::quantifiers::TriggerSelMode OptionsHandler::stringToTriggerSelMode(std::string option, std::string optarg) throw(OptionException) {
-  if(optarg ==  "default" || optarg == "all" ) {
+  if(optarg ==  "default") {
     return theory::quantifiers::TRIGGER_SEL_DEFAULT;
   } else if(optarg == "min") {
     return theory::quantifiers::TRIGGER_SEL_MIN;
   } else if(optarg == "max") {
     return theory::quantifiers::TRIGGER_SEL_MAX;
+  } else if(optarg == "all") {
+    return theory::quantifiers::TRIGGER_SEL_ALL;
   } else if(optarg ==  "help") {
     puts(s_triggerSelModeHelp.c_str());
     exit(1);
diff --git a/src/options/quantifiers_modes.h b/src/options/quantifiers_modes.h
index 8aa3756cc..86a783008 100644
--- a/src/options/quantifiers_modes.h
+++ b/src/options/quantifiers_modes.h
@@ -107,6 +107,8 @@ enum TriggerSelMode {
   TRIGGER_SEL_MIN,
   /** only consider maximal terms for triggers */
   TRIGGER_SEL_MAX,
+  /** consider all terms for triggers */
+  TRIGGER_SEL_ALL,
 };
 
 enum CVC4_PUBLIC PrenexQuantMode {