diff options
author | ajreynol <andrew.j.reynolds@gmail.com> | 2016-07-05 15:11:28 -0500 |
---|---|---|
committer | ajreynol <andrew.j.reynolds@gmail.com> | 2016-07-05 15:11:38 -0500 |
commit | 967747b7b279256bd9368e2d392ae71dec1bb1c1 (patch) | |
tree | 18a811b16d7552c1ae52fadfe34e54acde68e6a8 /src/options | |
parent | a58abbe71fb1fc07129ff9c7568ac544145fb57c (diff) |
Add option --trigger-active-sel. Recognize simple triggers with polarity. Do not drop patterns from merged prenex (fixes bug 743).
Diffstat (limited to 'src/options')
-rw-r--r-- | src/options/options_handler.cpp | 32 | ||||
-rw-r--r-- | src/options/options_handler.h | 2 | ||||
-rw-r--r-- | src/options/quantifiers_modes.h | 11 | ||||
-rw-r--r-- | src/options/quantifiers_options | 4 |
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 |