diff options
author | ajreynol <andrew.j.reynolds@gmail.com> | 2016-04-04 17:18:36 -0500 |
---|---|---|
committer | ajreynol <andrew.j.reynolds@gmail.com> | 2016-04-04 17:18:47 -0500 |
commit | 576d50ac7c13233a589771401537b587eb36361e (patch) | |
tree | 3f044ce37d5b3dc0f20db52339b3f1ae8cb59c8d /src/options/options_handler.cpp | |
parent | 0f69a8ba2286bd5d9b807c10ad350705952e93d6 (diff) |
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.
Diffstat (limited to 'src/options/options_handler.cpp')
-rw-r--r-- | src/options/options_handler.cpp | 18 |
1 files changed, 14 insertions, 4 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") { |