diff options
| author | Kshitij Bansal <kshitij@cs.nyu.edu> | 2015-04-15 23:21:52 -0400 |
|---|---|---|
| committer | Kshitij Bansal <kshitij@cs.nyu.edu> | 2015-04-15 23:21:52 -0400 |
| commit | 2df5b1632d48df1d526bb14ea31f3cb84defb5a6 (patch) | |
| tree | c8fcd46ddda4cc523f2a016165d2c78877873ce4 /src | |
| parent | b600e2d1975d80a66f628a6d042164faf60959bc (diff) | |
array theory builtinop
Diffstat (limited to 'src')
| -rw-r--r-- | src/parser/smt2/Smt2.g | 5 | ||||
| -rw-r--r-- | src/parser/smt2/smt2.cpp | 4 |
2 files changed, 2 insertions, 7 deletions
diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g index 8196a6276..dfbb79d72 100644 --- 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 bc1f94f36..a782bf1ba 100644 --- 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: |