diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2014-01-10 10:50:56 -0600 |
---|---|---|
committer | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2014-01-10 10:50:56 -0600 |
commit | 21f8e233e46fae32eaa6d2d4d5b4d0f36c36ba7f (patch) | |
tree | 610112b7b9f621466e478f29997a8fe2d5a62ccb /src/theory/quantifiers/options_handlers.h | |
parent | 841b7951f41f399859afab13a81e04599308da61 (diff) |
Add stats to quantifiers conflict find. Added option for qcf. Working on handling non-APPLY_UF terms.
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 */ |