diff options
Diffstat (limited to 'src/theory/quantifiers/options_handlers.h')
| -rw-r--r-- | src/theory/quantifiers/options_handlers.h | 29 |
1 files changed, 29 insertions, 0 deletions
diff --git a/src/theory/quantifiers/options_handlers.h b/src/theory/quantifiers/options_handlers.h index 4929fa60b..e0b1e30e8 100644 --- a/src/theory/quantifiers/options_handlers.h +++ b/src/theory/quantifiers/options_handlers.h @@ -97,6 +97,19 @@ interval \n\ + Use algorithm that abstracts domain elements as intervals. \n\ \n\ "; +static const std::string qcfWhenModeHelp = "\ +Quantifier conflict find modes currently supported by the --quant-cf-when option:\n\ +\n\ +default \n\ ++ Default, apply conflict finding at full effort.\n\ +\n\ +std \n\ ++ Apply conflict finding at standard effort.\n\ +\n\ +std-h \n\ ++ Apply conflict finding at standard effort when heuristic says to. \n\ +\n\ +"; inline InstWhenMode stringToInstWhenMode(std::string option, std::string optarg, SmtEngine* smt) throw(OptionException) { if(optarg == "pre-full") { @@ -186,6 +199,22 @@ inline void checkMbqiMode(std::string option, MbqiMode mode, SmtEngine* smt) thr } +inline QcfWhenMode stringToQcfWhenMode(std::string option, std::string optarg, SmtEngine* smt) throw(OptionException) { + if(optarg == "default") { + return QCF_WHEN_MODE_DEFAULT; + } else if(optarg == "std") { + return QCF_WHEN_MODE_STD; + } else if(optarg == "std-h") { + return QCF_WHEN_MODE_STD_H; + } else if(optarg == "help") { + puts(qcfWhenModeHelp.c_str()); + exit(1); + } else { + throw OptionException(std::string("unknown option for --quant-cf-when: `") + + optarg + "'. Try --quant-cf-when help."); + } +} + }/* CVC4::theory::quantifiers namespace */ }/* CVC4::theory namespace */ }/* CVC4 namespace */ |