From: Christopher L. Conway <christopherleeconway@gmail.com>
Date: Fri, 4 Jun 2010 19:19:47 +0000 (+0000)
Subject: Adding QF_SAT to SMT parsers
X-Git-Tag: cvc5-1.0.0~8997
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=cdfcddfb4afe401ea5be1214fda5020a6b59ae5d;p=cvc5.git

Adding QF_SAT to SMT parsers
---

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: