summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorKshitij Bansal <kshitij@cs.nyu.edu>2015-04-15 23:51:28 -0400
committerKshitij Bansal <kshitij@cs.nyu.edu>2015-04-15 23:51:28 -0400
commit3f5ac698f6ac51b72cab3ae0a8698a78a7fe006c (patch)
tree0ee417bd1879ccf70623b85255c3beccce8b5e19
parentacfc100e9c2fe2f03b12f547ae8ee48fa13902de (diff)
bv parserchanges cleanup
-rw-r--r--src/parser/smt2/Smt2.g31
1 files changed, 1 insertions, 30 deletions
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';
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback