From 35cd511b65a3a5dd6ad39e75df2b4fa57061f3b5 Mon Sep 17 00:00:00 2001
From: Morgan Deters <mdeters@cs.nyu.edu>
Date: Sun, 22 Jun 2014 00:30:47 -0400
Subject: 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
---
 src/util/language.cpp | 2 ++
 src/util/language.h   | 5 +++++
 2 files changed, 7 insertions(+)

(limited to 'src/util')

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";
   }
-- 
cgit v1.2.3