diff options
| author | Kshitij Bansal <kshitij@cs.nyu.edu> | 2015-04-15 23:34:37 -0400 |
|---|---|---|
| committer | Kshitij Bansal <kshitij@cs.nyu.edu> | 2015-04-15 23:34:37 -0400 |
| commit | 5c64edb7e3228b366b6c51e4dfd2a3dd350f9e2c (patch) | |
| tree | 127abd63e7e4b769fe843e7064d279463265d74a /src/parser/smt2 | |
| parent | 7d00e71793a0af9b5eef1951ed3208863db90855 (diff) | |
THEORY_INTS parser changes
Diffstat (limited to 'src/parser/smt2')
| -rw-r--r-- | src/parser/smt2/Smt2.g | 7 | ||||
| -rw-r--r-- | src/parser/smt2/smt2.cpp | 6 |
2 files changed, 3 insertions, 10 deletions
diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g index 13455506c..dd3464940 100644 --- a/src/parser/smt2/Smt2.g +++ b/src/parser/smt2/Smt2.g @@ -2037,9 +2037,6 @@ builtinOp[CVC4::Kind& kind] | MINUS_TOK { $kind = CVC4::kind::MINUS; } | STAR_TOK { $kind = CVC4::kind::MULT; } | DIV_TOK { $kind = CVC4::kind::DIVISION; } - | INTS_DIV_TOK { $kind = CVC4::kind::INTS_DIVISION; } - | INTS_MOD_TOK { $kind = CVC4::kind::INTS_MODULUS; } - | ABS_TOK { $kind = CVC4::kind::ABS; } | BV2NAT_TOK { $kind = CVC4::kind::BITVECTOR_TO_NAT; if(PARSER_STATE->strictModeEnabled()) { @@ -2472,10 +2469,6 @@ STAR_TOK : '*'; XOR_TOK : 'xor'; -INTS_DIV_TOK : 'div'; -INTS_MOD_TOK : 'mod'; -ABS_TOK : 'abs'; - DIVISIBLE_TOK : 'divisible'; // CONCAT_TOK : 'concat'; diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp index 73a5124e0..85f2d1ec5 100644 --- a/src/parser/smt2/smt2.cpp +++ b/src/parser/smt2/smt2.cpp @@ -168,9 +168,9 @@ void Smt2::addTheory(Theory theory) { case THEORY_INTS: defineType("Int", getExprManager()->integerType()); addArithmeticOperators(); - Parser::addOperator(kind::INTS_DIVISION); - Parser::addOperator(kind::INTS_MODULUS); - Parser::addOperator(kind::ABS); + addOperator(kind::INTS_DIVISION, "div"); + addOperator(kind::INTS_MODULUS, "mod"); + addOperator(kind::ABS, "abs"); Parser::addOperator(kind::DIVISIBLE); break; |