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

THEORY_REAL_INTS parser changes
---

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';
diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp
index a782bf1ba..73a5124e0 100644
--- a/src/parser/smt2/smt2.cpp
+++ b/src/parser/smt2/smt2.cpp
@@ -161,9 +161,9 @@ void Smt2::addTheory(Theory theory) {
   case THEORY_REALS_INTS:
     defineType("Real", getExprManager()->realType());
     Parser::addOperator(kind::DIVISION);
-    Parser::addOperator(kind::TO_INTEGER);
-    Parser::addOperator(kind::IS_INTEGER);
-    Parser::addOperator(kind::TO_REAL);
+    addOperator(kind::TO_INTEGER, "to_int");
+    addOperator(kind::IS_INTEGER, "is_int");
+    addOperator(kind::TO_REAL, "to_real");
     // falling through on purpose, to add Ints part of Reals_Ints
   case THEORY_INTS:
     defineType("Int", getExprManager()->integerType());