diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2017-11-03 21:18:01 -0500 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2017-11-03 21:18:01 -0500 |
| commit | 2ef8fe2eefaecdb62653d36c88169fe906512b9d (patch) | |
| tree | 09e1c088ba3f9e9f99a4238dd1a3528b131a9c59 /src/parser/smt1 | |
| parent | f70af84aa6ad1511963e6cec97c6096fdcc1b37d (diff) | |
Suppport SAT logic (#1310)
* Support SAT logic.
* Add lustre example.
* Add to smt1 as well.
* Fix.
* Fix.
* Fix for new option.
Diffstat (limited to 'src/parser/smt1')
| -rw-r--r-- | src/parser/smt1/smt1.cpp | 4 | ||||
| -rw-r--r-- | src/parser/smt1/smt1.h | 1 |
2 files changed, 5 insertions, 0 deletions
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, |