From 41bb6f0c0c4eed4011793bdb802dac68c1e73b04 Mon Sep 17 00:00:00 2001
From: "Christopher L. Conway" <christopherleeconway@gmail.com>
Date: Mon, 14 Jun 2010 20:45:11 +0000
Subject: [PATCH] Adding array select/store to SMT v1 and v2 parsers

---
 src/parser/smt/Smt.g     |  8 ++++++--
 src/parser/smt/smt.cpp   | 19 ++++++++++++++++++-
 src/parser/smt2/Smt2.g   |  4 ++++
 src/parser/smt2/smt2.cpp | 13 ++++++++++++-
 src/theory/arrays/kinds  |  2 ++
 5 files changed, 42 insertions(+), 4 deletions(-)

diff --git a/src/parser/smt/Smt.g b/src/parser/smt/Smt.g
index 4247dba7a..575f691a5 100644
--- a/src/parser/smt/Smt.g
+++ b/src/parser/smt/Smt.g
@@ -261,7 +261,7 @@ builtinOp[CVC4::Kind& kind]
   | IFF_TOK      { $kind = CVC4::kind::IFF;     }
   | EQUAL_TOK    { $kind = CVC4::kind::EQUAL;   }
   | DISTINCT_TOK { $kind = CVC4::kind::DISTINCT; }
-    // NOTE: Theory operators go here
+    // Arithmetic
   | GREATER_THAN_TOK
                  { $kind = CVC4::kind::GT; }
   | GREATER_THAN_TOK EQUAL_TOK
@@ -305,7 +305,9 @@ builtinOp[CVC4::Kind& kind]
   | BVSLE_TOK    { $kind = CVC4::kind::BITVECTOR_SLE;    }
   | BVSGT_TOK    { $kind = CVC4::kind::BITVECTOR_SGT;    }
   | BVSGE_TOK    { $kind = CVC4::kind::BITVECTOR_SGE;    }
-    /* TODO: lt, gt, plus, minus, etc. */
+    // NOTE: Theory operators go here
+  | SELECT_TOK   { $kind = CVC4::kind::SELECT; }
+  | STORE_TOK    { $kind = CVC4::kind::STORE; }
   ;
 
 /**
@@ -542,7 +544,9 @@ PERCENT_TOK       : '%';
 PIPE_TOK          : '|';
 PLUS_TOK          : '+';
 POUND_TOK         : '#';
+SELECT_TOK        : 'select';
 STAR_TOK          : '*';
+STORE_TOK         : 'store';
 TILDE_TOK         : '~';
 XOR_TOK           : 'xor';
 
diff --git a/src/parser/smt/smt.cpp b/src/parser/smt/smt.cpp
index 8748790f8..4851c8737 100644
--- a/src/parser/smt/smt.cpp
+++ b/src/parser/smt/smt.cpp
@@ -79,6 +79,20 @@ void Smt::addArithmeticOperators() {
  */
 void Smt::addTheory(Theory theory) {
   switch(theory) {
+  case THEORY_ARRAYS:
+  case THEORY_ARRAYS_EX: {
+    Type indexType = mkSort("Index");
+    Type elementTYpe = mkSort("Element");
+    
+    // FIXME: should be defineType("Array",arrayType(indexType,elementType))
+    // but arrayType isn't defined
+    mkSort("Array");
+
+    addOperator(kind::SELECT);
+    addOperator(kind::STORE);
+    break;
+  }
+
   case THEORY_EMPTY:
     mkSort("U");
     break;
@@ -117,6 +131,10 @@ void Smt::setLogic(const std::string& name) {
   d_logic = toLogic(name);
 
   switch(d_logic) {
+  case QF_AX:
+    addTheory(THEORY_ARRAYS_EX);
+    break;
+
   case QF_IDL:
   case QF_LIA:
   case QF_NIA:
@@ -146,7 +164,6 @@ void Smt::setLogic(const std::string& name) {
   case AUFNIRA:
   case QF_AUFBV:
   case QF_AUFLIA:
-  case QF_AX:
   case QF_BV:
     Unhandled(name);
   }
diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g
index 37612901e..0abc4c4c6 100644
--- a/src/parser/smt2/Smt2.g
+++ b/src/parser/smt2/Smt2.g
@@ -312,6 +312,8 @@ builtinOp[CVC4::Kind& kind]
   | STAR_TOK     { $kind = CVC4::kind::MULT; }
   | TILDE_TOK    { $kind = CVC4::kind::UMINUS; }
   | MINUS_TOK    { $kind = CVC4::kind::MINUS; }
+  | SELECT_TOK   { $kind = CVC4::kind::SELECT; }
+  | STORE_TOK    { $kind = CVC4::kind::STORE; }
     // NOTE: Theory operators go here
   ;
 
@@ -421,7 +423,9 @@ PERCENT_TOK       : '%';
 PIPE_TOK          : '|';
 PLUS_TOK          : '+';
 POUND_TOK         : '#';
+SELECT_TOK        : 'select';
 STAR_TOK          : '*';
+STORE_TOK         : 'store';
 TILDE_TOK         : '~';
 XOR_TOK           : 'xor';
 
diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp
index 871262b43..34245669e 100644
--- a/src/parser/smt2/smt2.cpp
+++ b/src/parser/smt2/smt2.cpp
@@ -64,6 +64,14 @@ void Smt2::addTheory(Theory theory) {
     addOperator(kind::XOR);
     break;
 
+  case THEORY_ARRAYS:
+    // FIXME: should define a paramterized type 'Array' with 2 arguments
+    mkSort("Array");
+
+    addOperator(kind::SELECT);
+    addOperator(kind::STORE);
+    break;
+
   case THEORY_REALS_INTS:
     defineType("Real", getExprManager()->realType());
     // falling-through on purpose, to add Ints part of RealsInts
@@ -105,6 +113,10 @@ void Smt2::setLogic(const std::string& name) {
     /* No extra symbols necessary */
     break;
 
+  case Smt::QF_AX:
+    addTheory(THEORY_ARRAYS);
+    break;
+
   case Smt::QF_IDL:
   case Smt::QF_LIA:
   case Smt::QF_NIA:
@@ -129,7 +141,6 @@ void Smt2::setLogic(const std::string& name) {
   case Smt::AUFNIRA:
   case Smt::QF_AUFBV:
   case Smt::QF_AUFLIA:
-  case Smt::QF_AX:
   case Smt::QF_BV:
     Unhandled(name);
   }
diff --git a/src/theory/arrays/kinds b/src/theory/arrays/kinds
index f27a49e4b..742b924c6 100644
--- a/src/theory/arrays/kinds
+++ b/src/theory/arrays/kinds
@@ -5,3 +5,5 @@
 #
 
 theory ::CVC4::theory::arrays::TheoryArrays "theory_arrays.h"
+operator SELECT 2 "array select"
+operator STORE 3 "array store"
-- 
2.30.2