Adding SMT v2 parsing support for: QF_IDL, QF_NIA, QF_RDL, QF_UFIDL

diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g
index b8557665ec90fdccfdc8b27ffb6d685673210115..11ce111a6a09085d4b8287aeffa99f14175126b9 100644 (file)
--- 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 d7da84a43683c20b92e1c07ce4f9729c9485d04b..d76d8ba387ee6f42e41f8279568008d1080ee27e 100644 (file)
--- 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 0bb3020a309c053a51047d71c1b621cad2a60bad..5eae90fa3ccde855cfb8e0ca2bf7ed2bde07f350 100644 (file)
--- 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 {