THEORY_INTS parser changes

diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g
index 13455506cf3d766896480b2a8222cbc702b3ffbb..dd34649405c7fcc3ea4dcd3874a935948522a405 100644 (file)
--- 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 73a5124e05c7d6dd73e9316e2f5a36801a2f5234..85f2d1ec5a66abf09a1d5b5d24681eb0caec2be9 100644 (file)
--- 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;