From 2ef8fe2eefaecdb62653d36c88169fe906512b9d Mon Sep 17 00:00:00 2001
From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Fri, 3 Nov 2017 21:18:01 -0500
Subject: Suppport SAT logic (#1310)

* Support SAT logic.

* Add lustre example.

* Add to smt1 as well.

* Fix.

* Fix.

* Fix for new option.
---
 src/parser/smt1/smt1.cpp | 4 ++++
 src/parser/smt1/smt1.h   | 1 +
 2 files changed, 5 insertions(+)

(limited to 'src/parser')

diff --git a/src/parser/smt1/smt1.cpp b/src/parser/smt1/smt1.cpp
index c4e670f6d..9a6d880e9 100644
--- a/src/parser/smt1/smt1.cpp
+++ b/src/parser/smt1/smt1.cpp
@@ -53,6 +53,7 @@ std::unordered_map<std::string, Smt1::Logic> Smt1::newLogicMap() {
   logicMap["QF_UFNIRA"] = QF_UFNIRA;
   logicMap["QF_AUFLIA"] = QF_AUFLIA;
   logicMap["QF_AUFLIRA"] = QF_AUFLIRA;
+  logicMap["SAT"] = SAT;
   logicMap["UFNIA"] = UFNIA;
   logicMap["UFNIRA"] = UFNIRA;
   logicMap["UFLRA"] = UFLRA;
@@ -205,6 +206,9 @@ void Smt1::setLogic(const std::string& name) {
   case QF_SAT:
     /* no extra symbols needed */
     break;
+  case SAT:
+    addTheory(THEORY_QUANTIFIERS);
+    break;
 
   case QF_UFIDL:
   case QF_UFLIA:
diff --git a/src/parser/smt1/smt1.h b/src/parser/smt1/smt1.h
index e9dbea1a9..036453675 100644
--- a/src/parser/smt1/smt1.h
+++ b/src/parser/smt1/smt1.h
@@ -62,6 +62,7 @@ public:
     QF_UFLIRA, // nonstandard
     QF_UFNIRA, // nonstandard
     QF_UFNRA,
+    SAT,
     UFLRA,
     UFNIRA, // nonstandard
     UFNIA,
-- 
cgit v1.2.3