merge from arrays-clark branch

4 files changed, 33 insertions, 3 deletions

diff --git a/src/parser/smt/Smt.g b/src/parser/smt/Smt.g
index 5a80083b3..6dd4e78f3 100644
--- a/src/parser/smt/Smt.g
+++ b/src/parser/smt/Smt.g
@@ -511,7 +511,13 @@ sortSymbol returns [CVC4::parser::smt::myType t]
   	{ $t = PARSER_STATE->getSort(name); }
   | BITVECTOR_TOK '[' NUMERAL_TOK ']' {
   	$t = EXPR_MANAGER->mkBitVectorType(AntlrInput::tokenToUnsigned($NUMERAL_TOK));
-  }
+    }
+  /* attaching 'Array' to '[' allows us to parse regular 'Array' correctly in
+   * e.g. QF_AX, and also 'Array[m:n]' in e.g. QF_AUFBV */
+  | 'Array[' n1=NUMERAL_TOK ':' n2=NUMERAL_TOK ']' {
+        $t = EXPR_MANAGER->mkArrayType(EXPR_MANAGER->mkBitVectorType(AntlrInput::tokenToUnsigned(n1)),
+                                       EXPR_MANAGER->mkBitVectorType(AntlrInput::tokenToUnsigned(n2)));
+    }
   ;
 
 /**
diff --git a/src/parser/smt/smt.cpp b/src/parser/smt/smt.cpp
index 508bfe352..58495c650 100644
--- a/src/parser/smt/smt.cpp
+++ b/src/parser/smt/smt.cpp
@@ -44,6 +44,9 @@ std::hash_map<const std::string, Smt::Logic, CVC4::StringHashFunction> Smt::newL
   logicMap["QF_UFLIRA"] = QF_UFLIRA;
   logicMap["QF_UFNIA"] = QF_UFNIA;
   logicMap["QF_UFNIRA"] = QF_UFNIRA;
+  logicMap["QF_ABV"] = QF_ABV;
+  logicMap["QF_AUFBV"] = QF_AUFBV;
+  logicMap["QF_UFNIRA"] = QF_UFNIRA;
   logicMap["QF_AUFLIA"] = QF_AUFLIA;
   logicMap["QF_AUFLIRA"] = QF_AUFLIRA;
   return logicMap;
@@ -188,6 +191,17 @@ void Smt::setLogic(const std::string& name) {
     addTheory(THEORY_BITVECTORS);
     break;
 
+  case QF_ABV:
+    addTheory(THEORY_ARRAYS_EX);
+    addTheory(THEORY_BITVECTORS);
+    break;
+
+  case QF_AUFBV:
+    addUf();
+    addTheory(THEORY_ARRAYS_EX);
+    addTheory(THEORY_BITVECTORS);
+    break;
+
   case QF_AUFLIA:
     addTheory(THEORY_ARRAYS_EX);
     addUf();
@@ -206,7 +220,6 @@ void Smt::setLogic(const std::string& name) {
   case AUFNIRA:
   case LRA:
   case UFNIA:
-  case QF_AUFBV:
     Unhandled(name);
   }
 }
diff --git a/src/parser/smt/smt.h b/src/parser/smt/smt.h
index 62bb24336..3a089641f 100644
--- a/src/parser/smt/smt.h
+++ b/src/parser/smt/smt.h
@@ -40,6 +40,7 @@ public:
     AUFLIRA,
     AUFNIRA,
     LRA,
+    QF_ABV,
     QF_AUFBV,
     QF_AUFLIA,
     QF_AUFLIRA,
diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp
index 39eaf5b95..a4b8647a9 100644
--- a/src/parser/smt2/smt2.cpp
+++ b/src/parser/smt2/smt2.cpp
@@ -149,6 +149,17 @@ void Smt2::setLogic(const std::string& name) {
     addTheory(THEORY_BITVECTORS);
     break;
 
+  case Smt::QF_ABV:
+    addTheory(THEORY_ARRAYS);
+    addTheory(THEORY_BITVECTORS);
+    break;
+
+  case Smt::QF_AUFBV:
+    addOperator(kind::APPLY_UF);
+    addTheory(THEORY_ARRAYS);
+    addTheory(THEORY_BITVECTORS);
+    break;
+
   case Smt::QF_AUFLIA:
     addTheory(THEORY_ARRAYS);
     addOperator(kind::APPLY_UF);
@@ -167,7 +178,6 @@ void Smt2::setLogic(const std::string& name) {
   case Smt::AUFNIRA:
   case Smt::LRA:
   case Smt::UFNIA:
-  case Smt::QF_AUFBV:
     Unhandled(name);
   }
 }