From b8f8e92c5cdd2d556d06e722e2e27b7c18a36216 Mon Sep 17 00:00:00 2001
From: "Christopher L. Conway" <christopherleeconway@gmail.com>
Date: Tue, 1 Jun 2010 20:19:30 +0000
Subject: Adding SMT v2 parsing support for: QF_IDL, QF_NIA, QF_RDL, QF_UFIDL

---
 src/parser/smt2/Smt2.g   |  1 -
 src/parser/smt2/smt2.cpp | 27 +++++++++++++++++++++++----
 src/parser/smt2/smt2.h   |  9 +++++++++
 3 files changed, 32 insertions(+), 5 deletions(-)

(limited to 'src/parser/smt2')

diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g
index b8557665e..11ce111a6 100644
--- a/src/parser/smt2/Smt2.g
+++ b/src/parser/smt2/Smt2.g
@@ -547,4 +547,3 @@ fragment SYMBOL_CHAR
  * Matches an allowed escaped character.
  */
 fragment ESCAPE : '\\' ('"' | '\\' | 'n' | 't' | 'r');
-
diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp
index d7da84a43..d76d8ba38 100644
--- a/src/parser/smt2/smt2.cpp
+++ b/src/parser/smt2/smt2.cpp
@@ -28,9 +28,13 @@ std::hash_map<const std::string, Smt2::Logic, CVC4::StringHashFunction> Smt2::ne
   std::hash_map<const std::string, Smt2::Logic, CVC4::StringHashFunction> logicMap;
   logicMap["QF_AX"] = QF_AX;
   logicMap["QF_BV"] = QF_BV;
+  logicMap["QF_IDL"] = QF_IDL;
   logicMap["QF_LIA"] = QF_LIA;
   logicMap["QF_LRA"] = QF_LRA;
+  logicMap["QF_NIA"] = QF_NIA;
+  logicMap["QF_RDL"] = QF_RDL;
   logicMap["QF_UF"] = QF_UF;
+  logicMap["QF_UFIDL"] = QF_UFIDL;
   return logicMap;
 }
 
@@ -117,15 +121,30 @@ void Smt2::setLogic(const std::string& name) {
   addTheory(THEORY_CORE);
 
   switch(d_logic) {
-  case QF_UF:
-    addOperator(kind::APPLY_UF);
+  case QF_IDL:
+  case QF_LIA:
+  case QF_NIA:
+    addTheory(THEORY_INTS);
     break;
-
+    
   case QF_LRA:
+  case QF_RDL:
     addTheory(THEORY_REALS);
     break;
 
-  default:
+  case QF_UFIDL:
+    addTheory(THEORY_INTS);
+    // falling-through on purpose, to add UF part of UFIDL
+
+  case QF_UF:
+    addOperator(kind::APPLY_UF);
+    break;
+
+  case AUFLIA:
+  case AUFLIRA:
+  case AUFNIRA:
+  case QF_AUFBV:
+  case QF_AUFLIA:
     Unhandled(name);
   }
 }
diff --git a/src/parser/smt2/smt2.h b/src/parser/smt2/smt2.h
index 0bb3020a3..5eae90fa3 100644
--- a/src/parser/smt2/smt2.h
+++ b/src/parser/smt2/smt2.h
@@ -35,11 +35,20 @@ class Smt2 : public Parser {
 
 public:
   enum Logic {
+    AUFLIA,
+    AUFLIRA,
+    AUFNIRA,
+    QF_AUFBV,
+    QF_AUFLIA,
     QF_AX,
     QF_BV,
+    QF_IDL,
     QF_LIA,
     QF_LRA,
+    QF_NIA,
+    QF_RDL,
     QF_UF,
+    QF_UFIDL
   };
 
   enum Theory {
-- 
cgit v1.2.3