From: Morgan Deters <mdeters@gmail.com>
Date: Fri, 27 Apr 2012 23:01:29 +0000 (+0000)
Subject: fix parser logic-handling oversights: QF_UFBV should now be supported
X-Git-Tag: cvc5-1.0.0~8214
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=755c90b722f3182343f1d8603ab63a2dad1f001e;p=cvc5.git

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 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
   };
 
diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp
index a4b8647a9..dc1b47bde 100644
--- 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);
   }