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/base_options_handlers.h | |
parent | 1b916866274cc238c708f25fbb8c17add33d3376 (diff) |
New translation work, support Z3-str-style string constraints.
Diffstat (limited to 'src/options/base_options_handlers.h')
-rw-r--r-- | src/options/base_options_handlers.h | 55 |
1 files changed, 15 insertions, 40 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) { |