add support for QF_AUFLIA and QF_AUFLIRA logic strings in SMT inputs, for testing

diff --git a/src/parser/smt/smt.cpp b/src/parser/smt/smt.cpp
index e0d1922c8ee0de2b2e4a5b525cf067e7bbaf7972..0ee6944d48dc79eb98173c0e28507319db0a381d 100644 (file)
--- a/src/parser/smt/smt.cpp
+++ b/src/parser/smt/smt.cpp
@@ -41,6 +41,8 @@ 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_AUFLIA"] = QF_AUFLIA;
+  logicMap["QF_AUFLIRA"] = QF_AUFLIRA;
   return logicMap;
 }
 
@@ -175,13 +177,25 @@ void Smt::setLogic(const std::string& name) {
     addTheory(THEORY_BITVECTORS);
     break;
 
+  case QF_AUFLIA:
+    addTheory(THEORY_ARRAYS_EX);
+    addUf();
+    addTheory(THEORY_INTS);
+    break;
+
+  case QF_AUFLIRA:
+    addTheory(THEORY_ARRAYS_EX);
+    addUf();
+    addTheory(THEORY_INTS);
+    addTheory(THEORY_REALS);
+    break;
+
   case AUFLIA:
   case AUFLIRA:
   case AUFNIRA:
   case LRA:
   case UFNIA:
   case QF_AUFBV:
-  case QF_AUFLIA:
     Unhandled(name);
   }
 }

diff --git a/src/parser/smt/smt.h b/src/parser/smt/smt.h
index 11a30c2fc05f40b02372839976901a783d2a1d3b..a99f8199808304ef16c6a2caae59acd7777f34f0 100644 (file)
--- a/src/parser/smt/smt.h
+++ b/src/parser/smt/smt.h
@@ -42,6 +42,7 @@ public:
     LRA,
     QF_AUFBV,
     QF_AUFLIA,
+    QF_AUFLIRA,
     QF_AX,
     QF_BV,
     QF_IDL,

diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp
index 08a824c0a40da525393ff90b499b2ea5c487e194..7d6f27aa51ae0b094098ec1966059021e153f4cc 100644 (file)
--- a/src/parser/smt2/smt2.cpp
+++ b/src/parser/smt2/smt2.cpp
@@ -141,13 +141,25 @@ void Smt2::setLogic(const std::string& name) {
     addTheory(THEORY_BITVECTORS);
     break;
 
+  case Smt::QF_AUFLIA:
+    addTheory(THEORY_ARRAYS);
+    addOperator(kind::APPLY_UF);
+    addTheory(THEORY_INTS);
+    break;
+
+  case Smt::QF_AUFLIRA:
+    addTheory(THEORY_ARRAYS);
+    addOperator(kind::APPLY_UF);
+    addTheory(THEORY_INTS);
+    addTheory(THEORY_REALS);
+    break;
+
   case Smt::AUFLIA:
   case Smt::AUFLIRA:
   case Smt::AUFNIRA:
   case Smt::LRA:
   case Smt::UFNIA:
   case Smt::QF_AUFBV:
-  case Smt::QF_AUFLIA:
     Unhandled(name);
   }
 }