Adding QF_SAT to SMT parsers

diff --git a/src/parser/smt/smt.cpp b/src/parser/smt/smt.cpp
index 606fc541858b06394d80a8e085b12b54309413a0..8748790f834d5114981fb490793c2dc300dc0a69 100644 (file)
--- a/src/parser/smt/smt.cpp
+++ b/src/parser/smt/smt.cpp
@@ -33,6 +33,7 @@ std::hash_map<const std::string, Smt::Logic, CVC4::StringHashFunction> Smt::newL
   logicMap["QF_LRA"] = QF_LRA;
   logicMap["QF_NIA"] = QF_NIA;
   logicMap["QF_RDL"] = QF_RDL;
+  logicMap["QF_SAT"] = QF_SAT;
   logicMap["QF_UF"] = QF_UF;
   logicMap["QF_UFIDL"] = QF_UFIDL;
   return logicMap;
@@ -127,6 +128,10 @@ void Smt::setLogic(const std::string& name) {
     addTheory(THEORY_REALS);
     break;
 
+  case QF_SAT:
+    /* no extra symbols needed */
+    break;
+
   case QF_UFIDL:
     addTheory(THEORY_INTS);
     // falling-through on purpose, to add UF part of UFIDL

diff --git a/src/parser/smt/smt.h b/src/parser/smt/smt.h
index fa20382ffd8a8094b9793c410d0dc4af8a70bade..7df25749a784fb0b11e907433a57df5f2c077754 100644 (file)
--- a/src/parser/smt/smt.h
+++ b/src/parser/smt/smt.h
@@ -47,6 +47,7 @@ public:
     QF_LRA,
     QF_NIA,
     QF_RDL,
+    QF_SAT,
     QF_UF,
     QF_UFIDL
   };

diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp
index 2776bff7e3228efb32c0955cb3133cb794b74497..871262b432841d6d214fc3a9e96b56f7ce70c9f2 100644 (file)
--- a/src/parser/smt2/smt2.cpp
+++ b/src/parser/smt2/smt2.cpp
@@ -101,6 +101,10 @@ void Smt2::setLogic(const std::string& name) {
   addTheory(THEORY_CORE);
 
   switch(d_logic) {
+  case Smt::QF_SAT:
+    /* No extra symbols necessary */
+    break;
+
   case Smt::QF_IDL:
   case Smt::QF_LIA:
   case Smt::QF_NIA: