array theory builtinop

diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g
index 8196a6276b0e0e39f70fca14808fc627f3d96002..dfbb79d726116be73c5a5d1bda6c751c7bf59459 100644 (file)
--- a/src/parser/smt2/Smt2.g
+++ b/src/parser/smt2/Smt2.g
@@ -2044,9 +2044,6 @@ builtinOp[CVC4::Kind& kind]
   | TO_INT_TOK   { $kind = CVC4::kind::TO_INTEGER; }
   | TO_REAL_TOK  { $kind = CVC4::kind::TO_REAL; }
 
-  | SELECT_TOK   { $kind = CVC4::kind::SELECT; }
-  | STORE_TOK    { $kind = CVC4::kind::STORE; }
-
   | BV2NAT_TOK     { $kind = CVC4::kind::BITVECTOR_TO_NAT;
                      if(PARSER_STATE->strictModeEnabled()) {
                        PARSER_STATE->parseError("bv2nat and int2bv are not part of SMT-LIB, and aren't available in SMT-LIB strict compliance mode");
@@ -2474,9 +2471,7 @@ OR_TOK            : 'or';
 // PERCENT_TOK       : '%';
 PLUS_TOK          : '+';
 //POUND_TOK         : '#';
-SELECT_TOK        : 'select';
 STAR_TOK          : '*';
-STORE_TOK         : 'store';
 // TILDE_TOK         : '~';
 TO_INT_TOK        : 'to_int';
 TO_REAL_TOK       : 'to_real';

diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp
index bc1f94f36a9552639fcfa5a5e104ba240cdb23e1..a782bf1baaef659d674acaf2d1b1b53129ba05f0 100644 (file)
--- a/src/parser/smt2/smt2.cpp
+++ b/src/parser/smt2/smt2.cpp
@@ -135,8 +135,8 @@ void Smt2::addFloatingPointOperators() {
 void Smt2::addTheory(Theory theory) {
   switch(theory) {
   case THEORY_ARRAYS:
-    Parser::addOperator(kind::SELECT);
-    Parser::addOperator(kind::STORE);
+    addOperator(kind::SELECT, "select");
+    addOperator(kind::STORE, "store");
     break;
 
   case THEORY_BITVECTORS: