diff options
Diffstat (limited to 'src/theory/quantifiers/options_handlers.h')
-rw-r--r-- | src/theory/quantifiers/options_handlers.h | 28 |
1 files changed, 28 insertions, 0 deletions
diff --git a/src/theory/quantifiers/options_handlers.h b/src/theory/quantifiers/options_handlers.h index 38567d166..86d0c27e4 100644 --- a/src/theory/quantifiers/options_handlers.h +++ b/src/theory/quantifiers/options_handlers.h @@ -152,6 +152,19 @@ ignore \n\ + Ignore user-provided patterns. \n\ \n\ "; +static const std::string triggerSelModeHelp = "\ +User pattern 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\ ++ Consider only minimal subterms that meet criteria for triggers.\n\ +\n\ +max \n\ ++ Consider only maximal subterms that meet criteria for triggers. \n\ +\n\ +"; inline InstWhenMode stringToInstWhenMode(std::string option, std::string optarg, SmtEngine* smt) throw(OptionException) { if(optarg == "pre-full") { return INST_WHEN_PRE_FULL; @@ -296,6 +309,21 @@ inline UserPatMode stringToUserPatMode(std::string option, std::string optarg, S optarg + "'. Try --user-pat help."); } } +inline TriggerSelMode stringToTriggerSelMode(std::string option, std::string optarg, SmtEngine* smt) throw(OptionException) { + if(optarg == "default" || optarg == "all" ) { + return TRIGGER_SEL_DEFAULT; + } else if(optarg == "min") { + return TRIGGER_SEL_MIN; + } else if(optarg == "max") { + return TRIGGER_SEL_MAX; + } else if(optarg == "help") { + puts(triggerSelModeHelp.c_str()); + exit(1); + } else { + throw OptionException(std::string("unknown option for --trigger-sel: `") + + optarg + "'. Try --trigger-sel help."); + } +} }/* CVC4::theory::quantifiers namespace */ }/* CVC4::theory namespace */ }/* CVC4 namespace */ |