| 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");
// 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';
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: