From 5c64edb7e3228b366b6c51e4dfd2a3dd350f9e2c Mon Sep 17 00:00:00 2001
From: Kshitij Bansal <kshitij@cs.nyu.edu>
Date: Wed, 15 Apr 2015 23:34:37 -0400
Subject: [PATCH] THEORY_INTS parser changes

---
 src/parser/smt2/Smt2.g   | 7 -------
 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;
 
-- 
2.30.2