diff options
| author | Christopher L. Conway <christopherleeconway@gmail.com> | 2010-06-04 19:19:47 +0000 |
|---|---|---|
| committer | Christopher L. Conway <christopherleeconway@gmail.com> | 2010-06-04 19:19:47 +0000 |
| commit | cdfcddfb4afe401ea5be1214fda5020a6b59ae5d (patch) | |
| tree | eb0d84bba5418c8a2c026f7c19ece449f63ce67e /src/parser | |
| parent | da3ee4d4c22c36a8978c2003af944c46fc5ad074 (diff) | |
Adding QF_SAT to SMT parsers
Diffstat (limited to 'src/parser')
| -rw-r--r-- | src/parser/smt/smt.cpp | 5 | ||||
| -rw-r--r-- | src/parser/smt/smt.h | 1 | ||||
| -rw-r--r-- | src/parser/smt2/smt2.cpp | 4 |
3 files changed, 10 insertions, 0 deletions
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: |