fix parser logic-handling oversights: QF_UFBV should now be supported

diff --git a/src/parser/smt/smt.cpp b/src/parser/smt/smt.cpp
index 58495c650f3d1d1f29bc38b4c500bc8ccc87c8ea..edba64b7af5c55677735f139ba2e7823ad7dba8f 100644 (file)
--- 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 3a089641f7084db96d17e1a73cb4cc683c851e7a..1606d7baba98a557737b089b717a23ceca8300ec 100644 (file)
--- 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
   };
 

diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp
index a4b8647a950d4d78b01421639d7f91800bc1b989..dc1b47bdef1d5364b9c087b0994715a5f1fda18d 100644 (file)
--- a/src/parser/smt2/smt2.cpp
+++ b/src/parser/smt2/smt2.cpp
@@ -116,8 +116,9 @@ void Smt2::setLogic(const std::string& name) {
     addTheory(THEORY_INTS);
     break;
 
-  case Smt::QF_LRA:
   case Smt::QF_RDL:
+  case Smt::QF_LRA:
+  case Smt::QF_NRA:
     addTheory(THEORY_REALS);
     break;
 
@@ -154,6 +155,11 @@ void Smt2::setLogic(const std::string& name) {
     addTheory(THEORY_BITVECTORS);
     break;
 
+  case Smt::QF_UFBV:
+    addOperator(kind::APPLY_UF);
+    addTheory(THEORY_BITVECTORS);
+    break;
+
   case Smt::QF_AUFBV:
     addOperator(kind::APPLY_UF);
     addTheory(THEORY_ARRAYS);
@@ -177,6 +183,7 @@ void Smt2::setLogic(const std::string& name) {
   case Smt::AUFLIRA:
   case Smt::AUFNIRA:
   case Smt::LRA:
+  case Smt::UFLRA:
   case Smt::UFNIA:
     Unhandled(name);
   }