Parsing support for SMT divisions: LRA, QF_UFLIA, QF_UFLRA, QF_UFNRA, UFNIA

2 files changed, 25 insertions, 5 deletions

diff --git a/src/parser/smt/smt.cpp b/src/parser/smt/smt.cpp
index 53c58e2e6..bbec3299f 100644
--- a/src/parser/smt/smt.cpp
+++ b/src/parser/smt/smt.cpp
@@ -121,6 +121,11 @@ bool Smt::logicIsSet() {
   return d_logicSet;
 }
 
+inline void Smt::addUf() {
+  addTheory(Smt::THEORY_EMPTY);
+  addOperator(kind::APPLY_UF);
+}
+
 /**
  * Sets the logic for the current benchmark. Declares any logic and theory symbols.
  *
@@ -152,17 +157,26 @@ void Smt::setLogic(const std::string& name) {
     break;
 
   case QF_UFIDL:
+  case QF_UFLIA:
     addTheory(THEORY_INTS);
-    // falling-through on purpose, to add UF part of UFIDL
+    addUf();
+    break;
+
+  case QF_UFLRA:
+  case QF_UFNRA:
+    addTheory(THEORY_REALS);
+    addUf();
+    break;
 
   case QF_UF:
-    addTheory(THEORY_EMPTY);
-    addOperator(kind::APPLY_UF);
+    addUf();
     break;
 
   case AUFLIA:
   case AUFLIRA:
   case AUFNIRA:
+  case LRA:
+  case UFNIA:
   case QF_AUFBV:
   case QF_AUFLIA:
   case QF_BV:
diff --git a/src/parser/smt/smt.h b/src/parser/smt/smt.h
index c6a15b335..d08e25ba9 100644
--- a/src/parser/smt/smt.h
+++ b/src/parser/smt/smt.h
@@ -36,9 +36,10 @@ class Smt : public Parser {
 
 public:
   enum Logic {
-    AUFLIA,
+    AUFLIA, // +p and -p?
     AUFLIRA,
     AUFNIRA,
+    LRA,
     QF_AUFBV,
     QF_AUFLIA,
     QF_AX,
@@ -50,7 +51,11 @@ public:
     QF_RDL,
     QF_SAT,
     QF_UF,
-    QF_UFIDL
+    QF_UFIDL,
+    QF_UFLIA,
+    QF_UFLRA,
+    QF_UFNRA,
+    UFNIA
   };
 
   enum Theory {
@@ -102,6 +107,7 @@ public:
 private:
 
   void addArithmeticOperators();
+  void addUf();
   static std::hash_map<const std::string, Logic, CVC4::StringHashFunction> newLogicMap();
 };
 }/* CVC4::parser namespace */