From cdfcddfb4afe401ea5be1214fda5020a6b59ae5d Mon Sep 17 00:00:00 2001
From: "Christopher L. Conway" <christopherleeconway@gmail.com>
Date: Fri, 4 Jun 2010 19:19:47 +0000
Subject: [PATCH] Adding QF_SAT to SMT parsers

---
 src/parser/smt/smt.cpp   | 5 +++++
 src/parser/smt/smt.h     | 1 +
 src/parser/smt2/smt2.cpp | 4 ++++
 3 files changed, 10 insertions(+)

diff --git a/src/parser/smt/smt.cpp b/src/parser/smt/smt.cpp
index 606fc5418..8748790f8 100644
--- 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 fa20382ff..7df25749a 100644
--- 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 2776bff7e..871262b43 100644
--- 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:
-- 
2.30.2