diff options
| author | Morgan Deters <mdeters@cs.nyu.edu> | 2014-06-22 00:30:47 -0400 |
|---|---|---|
| committer | Morgan Deters <mdeters@cs.nyu.edu> | 2014-06-22 06:21:58 -0400 |
| commit | 35cd511b65a3a5dd6ad39e75df2b4fa57061f3b5 (patch) | |
| tree | 0b896605a0702f3f556aad5eafd5931c19d22d41 /src/util | |
| parent | 542156e0f589dfe89ca7fb5736b44b05cb653ab6 (diff) | |
Output language "cvc3" (as opposed to "cvc" or "cvc4") produces output for CVC3:
1. no decimals used for rational literals
2. queries/check-sats wrapped with PUSH/POP
Diffstat (limited to 'src/util')
| -rw-r--r-- | src/util/language.cpp | 2 | ||||
| -rw-r--r-- | src/util/language.h | 5 |
2 files changed, 7 insertions, 0 deletions
diff --git a/src/util/language.cpp b/src/util/language.cpp index 8a1ab26af..1a184e648 100644 --- a/src/util/language.cpp +++ b/src/util/language.cpp @@ -68,6 +68,8 @@ OutputLanguage toOutputLanguage(std::string language) { language == "presentation" || language == "native" || language == "LANG_CVC4") { return output::LANG_CVC4; + } else if(language == "cvc3" || language == "LANG_CVC3") { + return output::LANG_CVC3; } else if(language == "smtlib1" || language == "smt1" || language == "LANG_SMTLIB_V1") { return output::LANG_SMTLIB_V1; diff --git a/src/util/language.h b/src/util/language.h index c79c4d9aa..0d1c5486a 100644 --- a/src/util/language.h +++ b/src/util/language.h @@ -121,6 +121,8 @@ enum CVC4_PUBLIC Language { /** The AST output language */ LANG_AST = 10, + /** The CVC3-compatibility output language */ + LANG_CVC3, /** LANG_MAX is > any valid OutputLanguage id */ LANG_MAX @@ -147,6 +149,9 @@ inline std::ostream& operator<<(std::ostream& out, Language lang) { case LANG_AST: out << "LANG_AST"; break; + case LANG_CVC3: + out << "LANG_CVC3"; + break; default: out << "undefined_output_language"; } |