New options for trigger selection, add option --strict-triggers. Do not infer alpha equivalence for quantifiers with annotations, limit rewrite operations when triggers are trusted.

3 files changed, 21 insertions, 7 deletions

diff --git a/src/options/options_handler.cpp b/src/options/options_handler.cpp
index 90202d6f5..d08f5f533 100644
--- a/src/options/options_handler.cpp
+++ b/src/options/options_handler.cpp
@@ -347,15 +347,21 @@ interleave \n\
 const std::string OptionsHandler::s_triggerSelModeHelp = "\
 Trigger selection modes currently supported by the --trigger-sel option:\n\
 \n\
-default \n\
-+ Default, consider all subterms of quantified formulas for trigger selection.\n\
-\n\
-min \n\
+min | default \n\
 + Consider only minimal subterms that meet criteria for triggers.\n\
 \n\
 max \n\
 + Consider only maximal subterms that meet criteria for triggers. \n\
 \n\
+all \n\
++ Consider all subterms that meet criteria for triggers. \n\
+\n\
+min-s-max \n\
++ Consider only minimal subterms that meet criteria for single triggers, maximal otherwise. \n\
+\n\
+min-s-all \n\
++ Consider only minimal subterms that meet criteria for single triggers, all otherwise. \n\
+\n\
 ";
 const std::string OptionsHandler::s_prenexQuantModeHelp = "\
 Prenex quantifiers modes currently supported by the --prenex-quant option:\n\
@@ -608,6 +614,10 @@ theory::quantifiers::TriggerSelMode OptionsHandler::stringToTriggerSelMode(std::
     return theory::quantifiers::TRIGGER_SEL_MIN;
   } else if(optarg == "max") {
     return theory::quantifiers::TRIGGER_SEL_MAX;
+  } else if(optarg == "min-s-max") {
+    return theory::quantifiers::TRIGGER_SEL_MIN_SINGLE_MAX;
+  } else if(optarg == "min-s-all") {
+    return theory::quantifiers::TRIGGER_SEL_MIN_SINGLE_ALL;
   } else if(optarg == "all") {
     return theory::quantifiers::TRIGGER_SEL_ALL;
   } else if(optarg ==  "help") {
diff --git a/src/options/quantifiers_modes.h b/src/options/quantifiers_modes.h
index 8ecf65a33..a437cfc97 100644
--- a/src/options/quantifiers_modes.h
+++ b/src/options/quantifiers_modes.h
@@ -107,6 +107,10 @@ enum TriggerSelMode {
   TRIGGER_SEL_MIN,
   /** only consider maximal terms for triggers */
   TRIGGER_SEL_MAX,
+  /** consider minimal terms for single triggers, maximal for non-single */
+  TRIGGER_SEL_MIN_SINGLE_MAX,
+  /** consider minimal terms for single triggers, all for non-single */
+  TRIGGER_SEL_MIN_SINGLE_ALL,
   /** consider all terms for triggers */
   TRIGGER_SEL_ALL,
 };
diff --git a/src/options/quantifiers_options b/src/options/quantifiers_options
index 5f23a02e0..8ed4f24c0 100644
--- a/src/options/quantifiers_options
+++ b/src/options/quantifiers_options
@@ -69,8 +69,8 @@ option inferArithTriggerEq --infer-arith-trigger-eq bool :default false
 option inferArithTriggerEqExp --infer-arith-trigger-eq-exp bool :default false
  record explanations for inferArithTriggerEq
  
-option smartTriggers --smart-triggers bool :default true
- enable smart triggers
+option strictTriggers --strict-triggers bool :default false
+ only instantiate quantifiers with user patterns based on triggers
 option relevantTriggers --relevant-triggers bool :default false
  prefer triggers that are more relevant based on SInE style analysis
 option relationalTriggers --relational-triggers bool :default false
@@ -89,7 +89,7 @@ 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
  selection mode for triggers
-option userPatternsQuant --user-pat=MODE CVC4::theory::quantifiers::UserPatMode :default CVC4::theory::quantifiers::USER_PAT_MODE_TRUST :include "options/quantifiers_modes.h" :handler stringToUserPatMode
+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
  generate additional triggers as needed during search