From: Kshitij Bansal <kshitij@cs.nyu.edu>
Date: Thu, 16 Apr 2015 03:34:37 +0000 (-0400)
Subject: THEORY_INTS parser changes
X-Git-Tag: cvc5-1.0.0~6344^2~1^2~6
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=5c64edb7e3228b366b6c51e4dfd2a3dd350f9e2c;p=cvc5.git

THEORY_INTS parser changes
---

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;