diff options
author | Morgan Deters <mdeters@cs.nyu.edu> | 2014-02-10 21:05:16 -0500 |
---|---|---|
committer | Morgan Deters <mdeters@cs.nyu.edu> | 2014-02-25 15:02:34 -0500 |
commit | f5f7ecf3ddd9ed23e5e44f2eefd41c1b11f2a70a (patch) | |
tree | ebf5304156cbc6242cf10329e658d95d810d3360 /src/options | |
parent | 1b916866274cc238c708f25fbb8c17add33d3376 (diff) |
New translation work, support Z3-str-style string constraints.
Diffstat (limited to 'src/options')
-rw-r--r-- | src/options/base_options_handlers.h | 55 | ||||
-rw-r--r-- | src/options/options_template.cpp | 9 |
2 files changed, 20 insertions, 44 deletions
diff --git a/src/options/base_options_handlers.h b/src/options/base_options_handlers.h index a161b6c07..2298f5880 100644 --- a/src/options/base_options_handlers.h +++ b/src/options/base_options_handlers.h @@ -25,6 +25,7 @@ #include <sstream> #include "expr/command.h" +#include "util/language.h" namespace CVC4 { namespace options { @@ -69,59 +70,33 @@ inline void decreaseVerbosity(std::string option, SmtEngine* smt) { } inline OutputLanguage stringToOutputLanguage(std::string option, std::string optarg, SmtEngine* smt) throw(OptionException) { - if(optarg == "cvc4" || optarg == "pl" || - optarg == "presentation" || optarg == "native" || - optarg == "LANG_CVC4") { - return language::output::LANG_CVC4; - } else if(optarg == "smtlib1" || optarg == "smt1" || - optarg == "LANG_SMTLIB_V1") { - return language::output::LANG_SMTLIB_V1; - } else if(optarg == "smtlib" || optarg == "smt" || - optarg == "smtlib2" || optarg == "smt2" || - optarg == "LANG_SMTLIB_V2") { - return language::output::LANG_SMTLIB_V2; - } else if(optarg == "tptp" || optarg == "LANG_TPTP") { - return language::output::LANG_TPTP; - } else if(optarg == "ast" || optarg == "LANG_AST") { - return language::output::LANG_AST; - } else if(optarg == "auto" || optarg == "LANG_AUTO") { + if(optarg == "help") { + options::languageHelp.set(true); return language::output::LANG_AUTO; } - if(optarg != "help") { - throw OptionException(std::string("unknown language for ") + option + - ": `" + optarg + "'. Try --output-lang help."); + try { + return language::toOutputLanguage(optarg); + } catch(OptionException& oe) { + throw OptionException("Error in " + option + ": " + oe.getMessage() + "\nTry --output-language help"); } - options::languageHelp.set(true); - return language::output::LANG_AUTO; + Unreachable(); } inline InputLanguage stringToInputLanguage(std::string option, std::string optarg, SmtEngine* smt) throw(OptionException) { - if(optarg == "cvc4" || optarg == "pl" || - optarg == "presentation" || optarg == "native" || - optarg == "LANG_CVC4") { - return language::input::LANG_CVC4; - } else if(optarg == "smtlib1" || optarg == "smt1" || - optarg == "LANG_SMTLIB_V1") { - return language::input::LANG_SMTLIB_V1; - } else if(optarg == "smtlib" || optarg == "smt" || - optarg == "smtlib2" || optarg == "smt2" || - optarg == "LANG_SMTLIB_V2") { - return language::input::LANG_SMTLIB_V2; - } else if(optarg == "tptp" || optarg == "LANG_TPTP") { - return language::input::LANG_TPTP; - } else if(optarg == "auto" || optarg == "LANG_AUTO") { + if(optarg == "help") { + options::languageHelp.set(true); return language::input::LANG_AUTO; } - if(optarg != "help") { - throw OptionException(std::string("unknown language for ") + option + - ": `" + optarg + "'. Try --lang help."); + try { + return language::toInputLanguage(optarg); + } catch(OptionException& oe) { + throw OptionException("Error in " + option + ": " + oe.getMessage() + "\nTry --language help"); } - options::languageHelp.set(true); - return language::input::LANG_AUTO; + Unreachable(); } inline void addTraceTag(std::string option, std::string optarg, SmtEngine* smt) { diff --git a/src/options/options_template.cpp b/src/options/options_template.cpp index 9c2d5aaa4..02bfc6ca0 100644 --- a/src/options/options_template.cpp +++ b/src/options/options_template.cpp @@ -260,6 +260,7 @@ Languages currently supported as arguments to the --output-lang option:\n\ cvc4 | presentation | pl CVC4 presentation language\n\ smt1 | smtlib1 SMT-LIB format 1.2\n\ smt | smtlib | smt2 | smtlib2 SMT-LIB format 2.0\n\ + z3str SMT-LIB 2.0 with Z3-str string constraints\n\ tptp TPTP format\n\ ast internal format (simple syntax trees)\n\ "; @@ -311,7 +312,7 @@ static struct option cmdlineOptions[] = {${all_modules_long_options} { NULL, no_argument, NULL, '\0' } };/* cmdlineOptions */ -#line 315 "${template}" +#line 316 "${template}" static void preemptGetopt(int& argc, char**& argv, const char* opt) { const size_t maxoptlen = 128; @@ -504,7 +505,7 @@ std::vector<std::string> Options::parseOptions(int argc, char* main_argv[]) thro switch(c) { ${all_modules_option_handlers} -#line 508 "${template}" +#line 509 "${template}" case ':': // This can be a long or short option, and the way to get at the @@ -572,7 +573,7 @@ std::vector<std::string> Options::suggestCommandLineOptions(const std::string& o static const char* smtOptions[] = { ${all_modules_smt_options}, -#line 576 "${template}" +#line 577 "${template}" NULL };/* smtOptions[] */ @@ -594,7 +595,7 @@ SExpr Options::getOptions() const throw() { ${all_modules_get_options} -#line 598 "${template}" +#line 599 "${template}" return SExpr(opts); } |