From: Kshitij Bansal <kshitij@cs.nyu.edu>
Date: Thu, 16 Apr 2015 03:51:28 +0000 (-0400)
Subject: bv parserchanges cleanup
X-Git-Tag: cvc5-1.0.0~6344^2~1^2~3
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=3f5ac698f6ac51b72cab3ae0a8698a78a7fe006c;p=cvc5.git

bv parserchanges cleanup
---

diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g
index 190b43d51..2c91f3e47 100644
--- a/src/parser/smt2/Smt2.g
+++ b/src/parser/smt2/Smt2.g
@@ -2042,6 +2042,7 @@ builtinOp[CVC4::Kind& kind]
                      if(PARSER_STATE->strictModeEnabled()) {
                        PARSER_STATE->parseError("bv2nat and int2bv are not part of SMT-LIB, and aren't available in SMT-LIB strict compliance mode");
                      } }
+
   | STRCON_TOK     { $kind = CVC4::kind::STRING_CONCAT; }
   | STRLEN_TOK     { $kind = CVC4::kind::STRING_LENGTH; }
   | STRSUB_TOK     { $kind = CVC4::kind::STRING_SUBSTR; }
@@ -2445,36 +2446,6 @@ XOR_TOK           : 'xor';
 
 DIVISIBLE_TOK : 'divisible';
 
-// CONCAT_TOK : 'concat';
-// BVNOT_TOK : 'bvnot';
-// BVAND_TOK : 'bvand';
-// BVOR_TOK : 'bvor';
-// BVNEG_TOK : 'bvneg';
-// BVADD_TOK : 'bvadd';
-// BVMUL_TOK : 'bvmul';
-// BVUDIV_TOK : 'bvudiv';
-// BVUREM_TOK : 'bvurem';
-// BVSHL_TOK : 'bvshl';
-// BVLSHR_TOK : 'bvlshr';
-// BVULT_TOK : 'bvult';
-// BVNAND_TOK : 'bvnand';
-// BVNOR_TOK : 'bvnor';
-// BVXOR_TOK : 'bvxor';
-// BVXNOR_TOK : 'bvxnor';
-// BVCOMP_TOK : 'bvcomp';
-// BVSUB_TOK : 'bvsub';
-// BVSDIV_TOK : 'bvsdiv';
-// BVSREM_TOK : 'bvsrem';
-// BVSMOD_TOK : 'bvsmod';
-// BVASHR_TOK : 'bvashr';
-// BVULE_TOK : 'bvule';
-// BVUGT_TOK : 'bvugt';
-// BVUGE_TOK : 'bvuge';
-// BVSLT_TOK : 'bvslt';
-// BVSLE_TOK : 'bvsle';
-// BVSGT_TOK : 'bvsgt';
-// BVSGE_TOK : 'bvsge';
-
 BV2NAT_TOK : 'bv2nat';
 INT2BV_TOK : 'int2bv';