diff options
author | Morgan Deters <mdeters@gmail.com> | 2012-04-27 23:01:29 +0000 |
---|---|---|
committer | Morgan Deters <mdeters@gmail.com> | 2012-04-27 23:01:29 +0000 |
commit | 755c90b722f3182343f1d8603ab63a2dad1f001e (patch) | |
tree | 737b54493a5b67dfc424d0333bf93f3014a2e89e /src/parser/smt | |
parent | 17a64d466e42e436daf0ea24a340146fc3facfa5 (diff) |
fix parser logic-handling oversights: QF_UFBV should now be supported
Diffstat (limited to 'src/parser/smt')
-rw-r--r-- | src/parser/smt/smt.cpp | 12 | ||||
-rw-r--r-- | src/parser/smt/smt.h | 3 |
2 files changed, 14 insertions, 1 deletions
diff --git a/src/parser/smt/smt.cpp b/src/parser/smt/smt.cpp index 58495c650..edba64b7a 100644 --- a/src/parser/smt/smt.cpp +++ b/src/parser/smt/smt.cpp @@ -35,15 +35,18 @@ std::hash_map<const std::string, Smt::Logic, CVC4::StringHashFunction> Smt::newL logicMap["QF_LIA"] = QF_LIA; logicMap["QF_LRA"] = QF_LRA; logicMap["QF_NIA"] = QF_NIA; + logicMap["QF_NRA"] = QF_NRA; logicMap["QF_RDL"] = QF_RDL; logicMap["QF_SAT"] = QF_SAT; logicMap["QF_UF"] = QF_UF; logicMap["QF_UFIDL"] = QF_UFIDL; + logicMap["QF_UFBV"] = QF_UFBV; 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_UFNRA"] = QF_UFNRA; logicMap["QF_ABV"] = QF_ABV; logicMap["QF_AUFBV"] = QF_AUFBV; logicMap["QF_UFNIRA"] = QF_UFNIRA; @@ -154,8 +157,9 @@ void Smt::setLogic(const std::string& name) { addTheory(THEORY_INTS); break; - case QF_LRA: case QF_RDL: + case QF_LRA: + case QF_NRA: addTheory(THEORY_REALS); break; @@ -196,6 +200,11 @@ void Smt::setLogic(const std::string& name) { addTheory(THEORY_BITVECTORS); break; + case QF_UFBV: + addUf(); + addTheory(THEORY_BITVECTORS); + break; + case QF_AUFBV: addUf(); addTheory(THEORY_ARRAYS_EX); @@ -219,6 +228,7 @@ void Smt::setLogic(const std::string& name) { case AUFLIRA: case AUFNIRA: case LRA: + case UFLRA: case UFNIA: Unhandled(name); } diff --git a/src/parser/smt/smt.h b/src/parser/smt/smt.h index 3a089641f..1606d7bab 100644 --- a/src/parser/smt/smt.h +++ b/src/parser/smt/smt.h @@ -50,16 +50,19 @@ public: QF_LIA, QF_LRA, QF_NIA, + QF_NRA, QF_RDL, QF_SAT, QF_UF, QF_UFIDL, + QF_UFBV, QF_UFLIA, QF_UFNIA, // nonstandard QF_UFLRA, QF_UFLIRA, // nonstandard QF_UFNIRA, // nonstandard QF_UFNRA, + UFLRA, UFNIA }; |