summaryrefslogtreecommitdiff
path: root/src/parser/smt2/Smt2.g
diff options
context:
space:
mode:
Diffstat (limited to 'src/parser/smt2/Smt2.g')
-rw-r--r--src/parser/smt2/Smt2.g7
1 files changed, 1 insertions, 6 deletions
diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g
index dfbb79d72..13455506c 100644
--- a/src/parser/smt2/Smt2.g
+++ b/src/parser/smt2/Smt2.g
@@ -2040,9 +2040,6 @@ builtinOp[CVC4::Kind& kind]
| INTS_DIV_TOK { $kind = CVC4::kind::INTS_DIVISION; }
| INTS_MOD_TOK { $kind = CVC4::kind::INTS_MODULUS; }
| ABS_TOK { $kind = CVC4::kind::ABS; }
- | IS_INT_TOK { $kind = CVC4::kind::IS_INTEGER; }
- | TO_INT_TOK { $kind = CVC4::kind::TO_INTEGER; }
- | TO_REAL_TOK { $kind = CVC4::kind::TO_REAL; }
| BV2NAT_TOK { $kind = CVC4::kind::BITVECTOR_TO_NAT;
if(PARSER_STATE->strictModeEnabled()) {
@@ -2462,7 +2459,6 @@ FORALL_TOK : 'forall';
GREATER_THAN_TOK : '>';
GREATER_THAN_EQUAL_TOK : '>=';
IMPLIES_TOK : '=>';
-IS_INT_TOK : 'is_int';
LESS_THAN_TOK : '<';
LESS_THAN_EQUAL_TOK : '<=';
MINUS_TOK : '-';
@@ -2473,10 +2469,9 @@ PLUS_TOK : '+';
//POUND_TOK : '#';
STAR_TOK : '*';
// TILDE_TOK : '~';
-TO_INT_TOK : 'to_int';
-TO_REAL_TOK : 'to_real';
XOR_TOK : 'xor';
+
INTS_DIV_TOK : 'div';
INTS_MOD_TOK : 'mod';
ABS_TOK : 'abs';
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback