From 19b3adf57987584096ca59dc9852fb9573ee1715 Mon Sep 17 00:00:00 2001
From: Morgan Deters <mdeters@gmail.com>
Date: Thu, 20 Oct 2011 17:40:26 +0000
Subject: [PATCH] add support for QF_AUFLIA and QF_AUFLIRA logic strings in SMT
 inputs, for testing

---
 src/parser/smt/smt.cpp   | 16 +++++++++++++++-
 src/parser/smt/smt.h     |  1 +
 src/parser/smt2/smt2.cpp | 14 +++++++++++++-
 3 files changed, 29 insertions(+), 2 deletions(-)

diff --git a/src/parser/smt/smt.cpp b/src/parser/smt/smt.cpp
index e0d1922c8..0ee6944d4 100644
--- 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 11a30c2fc..a99f81998 100644
--- 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 08a824c0a..7d6f27aa5 100644
--- 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);
   }
 }
-- 
2.30.2