diff options
Diffstat (limited to 'src/parser/smt')
-rw-r--r-- | src/parser/smt/smt.cpp | 11 | ||||
-rw-r--r-- | src/parser/smt/smt.h | 3 |
2 files changed, 14 insertions, 0 deletions
diff --git a/src/parser/smt/smt.cpp b/src/parser/smt/smt.cpp index 0ee6944d4..508bfe352 100644 --- a/src/parser/smt/smt.cpp +++ b/src/parser/smt/smt.cpp @@ -41,6 +41,9 @@ std::hash_map<const std::string, Smt::Logic, CVC4::StringHashFunction> Smt::newL logicMap["QF_UFIDL"] = QF_UFIDL; logicMap["QF_UFLRA"] = QF_UFLRA; logicMap["QF_UFLIA"] = QF_UFLIA; + logicMap["QF_UFLIRA"] = QF_UFLIRA; + logicMap["QF_UFNIA"] = QF_UFNIA; + logicMap["QF_UFNIRA"] = QF_UFNIRA; logicMap["QF_AUFLIA"] = QF_AUFLIA; logicMap["QF_AUFLIRA"] = QF_AUFLIRA; return logicMap; @@ -159,6 +162,7 @@ void Smt::setLogic(const std::string& name) { case QF_UFIDL: case QF_UFLIA: + case QF_UFNIA:// nonstandard logic addTheory(THEORY_INTS); addUf(); break; @@ -169,6 +173,13 @@ void Smt::setLogic(const std::string& name) { addUf(); break; + case QF_UFLIRA:// nonstandard logic + case QF_UFNIRA:// nonstandard logic + addTheory(THEORY_INTS); + addTheory(THEORY_REALS); + addUf(); + break; + case QF_UF: addUf(); break; diff --git a/src/parser/smt/smt.h b/src/parser/smt/smt.h index a99f81998..62bb24336 100644 --- a/src/parser/smt/smt.h +++ b/src/parser/smt/smt.h @@ -54,7 +54,10 @@ public: QF_UF, QF_UFIDL, QF_UFLIA, + QF_UFNIA, // nonstandard QF_UFLRA, + QF_UFLIRA, // nonstandard + QF_UFNIRA, // nonstandard QF_UFNRA, UFNIA }; |