From b600e2d1975d80a66f628a6d042164faf60959bc Mon Sep 17 00:00:00 2001 From: Kshitij Bansal Date: Wed, 15 Apr 2015 23:00:28 -0400 Subject: [PATCH] cleanup --- src/parser/smt2/Smt2.g | 30 --------------------- src/parser/smt2/smt2.cpp | 58 ++++++++++++++++++++-------------------- 2 files changed, 29 insertions(+), 59 deletions(-) diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g index 467befca5..8196a6276 100644 --- a/src/parser/smt2/Smt2.g +++ b/src/parser/smt2/Smt2.g @@ -2047,36 +2047,6 @@ builtinOp[CVC4::Kind& kind] | SELECT_TOK { $kind = CVC4::kind::SELECT; } | STORE_TOK { $kind = CVC4::kind::STORE; } - // | CONCAT_TOK { $kind = CVC4::kind::BITVECTOR_CONCAT; } - // | BVNOT_TOK { $kind = CVC4::kind::BITVECTOR_NOT; } - // | BVAND_TOK { $kind = CVC4::kind::BITVECTOR_AND; } - // | BVOR_TOK { $kind = CVC4::kind::BITVECTOR_OR; } - // | BVNEG_TOK { $kind = CVC4::kind::BITVECTOR_NEG; } - // | BVADD_TOK { $kind = CVC4::kind::BITVECTOR_PLUS; } - // | BVMUL_TOK { $kind = CVC4::kind::BITVECTOR_MULT; } - // | BVUDIV_TOK { $kind = CVC4::kind::BITVECTOR_UDIV; } - // | BVUREM_TOK { $kind = CVC4::kind::BITVECTOR_UREM; } - // | BVSHL_TOK { $kind = CVC4::kind::BITVECTOR_SHL; } - // | BVLSHR_TOK { $kind = CVC4::kind::BITVECTOR_LSHR; } - // | BVULT_TOK { $kind = CVC4::kind::BITVECTOR_ULT; } - // | BVNAND_TOK { $kind = CVC4::kind::BITVECTOR_NAND; } - // | BVNOR_TOK { $kind = CVC4::kind::BITVECTOR_NOR; } - // | BVXOR_TOK { $kind = CVC4::kind::BITVECTOR_XOR; } - // | BVXNOR_TOK { $kind = CVC4::kind::BITVECTOR_XNOR; } - // | BVCOMP_TOK { $kind = CVC4::kind::BITVECTOR_COMP; } - // | BVSUB_TOK { $kind = CVC4::kind::BITVECTOR_SUB; } - // | BVSDIV_TOK { $kind = CVC4::kind::BITVECTOR_SDIV; } - // | BVSREM_TOK { $kind = CVC4::kind::BITVECTOR_SREM; } - // | BVSMOD_TOK { $kind = CVC4::kind::BITVECTOR_SMOD; } - // | BVASHR_TOK { $kind = CVC4::kind::BITVECTOR_ASHR; } - // | BVULE_TOK { $kind = CVC4::kind::BITVECTOR_ULE; } - // | BVUGT_TOK { $kind = CVC4::kind::BITVECTOR_UGT; } - // | BVUGE_TOK { $kind = CVC4::kind::BITVECTOR_UGE; } - // | BVSLT_TOK { $kind = CVC4::kind::BITVECTOR_SLT; } - // | BVSLE_TOK { $kind = CVC4::kind::BITVECTOR_SLE; } - // | BVSGT_TOK { $kind = CVC4::kind::BITVECTOR_SGT; } - // | BVSGE_TOK { $kind = CVC4::kind::BITVECTOR_SGE; } - | BV2NAT_TOK { $kind = CVC4::kind::BITVECTOR_TO_NAT; 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"); diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp index 1f81e8ba1..bc1f94f36 100644 --- a/src/parser/smt2/smt2.cpp +++ b/src/parser/smt2/smt2.cpp @@ -50,35 +50,35 @@ void Smt2::addArithmeticOperators() { } void Smt2::addBitvectorOperators() { - addOperator(kind::BITVECTOR_CONCAT, "concat"); // | CONCAT_TOK { $kind = CVC4::; } Parser::addOperator(kind::BITVECTOR_CONCAT); - addOperator(kind::BITVECTOR_NOT, "bvnot"); // | BVNOT_TOK { $kind = CVC4::; } Parser::addOperator(kind::BITVECTOR_AND); - addOperator(kind::BITVECTOR_AND, "bvand"); // | BVAND_TOK { $kind = CVC4::; } Parser::addOperator(kind::BITVECTOR_OR); - addOperator(kind::BITVECTOR_OR, "bvor"); // | BVOR_TOK { $kind = CVC4::; } Parser::addOperator(kind::BITVECTOR_XOR); - addOperator(kind::BITVECTOR_NEG, "bvneg"); // | BVNEG_TOK { $kind = CVC4::; } Parser::addOperator(kind::BITVECTOR_NOT); - addOperator(kind::BITVECTOR_PLUS, "bvadd"); // | BVADD_TOK { $kind = CVC4::; } Parser::addOperator(kind::BITVECTOR_NAND); - addOperator(kind::BITVECTOR_MULT, "bvmul"); // | BVMUL_TOK { $kind = CVC4::; } Parser::addOperator(kind::BITVECTOR_NOR); - addOperator(kind::BITVECTOR_UDIV, "bvudiv"); // | BVUDIV_TOK { $kind = CVC4::; } Parser::addOperator(kind::BITVECTOR_XNOR); - addOperator(kind::BITVECTOR_UREM, "bvurem"); // | BVUREM_TOK { $kind = CVC4::; } Parser::addOperator(kind::BITVECTOR_COMP); - addOperator(kind::BITVECTOR_SHL, "bvshl"); // | BVSHL_TOK { $kind = CVC4::; } Parser::addOperator(kind::BITVECTOR_MULT); - addOperator(kind::BITVECTOR_LSHR, "bvlshr"); // | BVLSHR_TOK { $kind = CVC4::; } Parser::addOperator(kind::BITVECTOR_PLUS); - addOperator(kind::BITVECTOR_ULT, "bvult"); // | BVULT_TOK { $kind = CVC4::; } Parser::addOperator(kind::BITVECTOR_SUB); - addOperator(kind::BITVECTOR_NAND, "bvnand"); // | BVNAND_TOK { $kind = CVC4::; } Parser::addOperator(kind::BITVECTOR_NEG); - addOperator(kind::BITVECTOR_NOR, "bvnor"); // | BVNOR_TOK { $kind = CVC4::; } Parser::addOperator(kind::BITVECTOR_UDIV); - addOperator(kind::BITVECTOR_XOR, "bvxor"); // | BVXOR_TOK { $kind = CVC4::; } Parser::addOperator(kind::BITVECTOR_UREM); - addOperator(kind::BITVECTOR_XNOR, "bvxnor"); // | BVXNOR_TOK { $kind = CVC4::; } Parser::addOperator(kind::BITVECTOR_SDIV); - addOperator(kind::BITVECTOR_COMP, "bvcomp"); // | BVCOMP_TOK { $kind = CVC4::; } Parser::addOperator(kind::BITVECTOR_SREM); - addOperator(kind::BITVECTOR_SUB, "bvsub"); // | BVSUB_TOK { $kind = CVC4::; } Parser::addOperator(kind::BITVECTOR_SMOD); - addOperator(kind::BITVECTOR_SDIV, "bvsdiv"); // | BVSDIV_TOK { $kind = CVC4::; } Parser::addOperator(kind::BITVECTOR_SHL); - addOperator(kind::BITVECTOR_SREM, "bvsrem"); // | BVSREM_TOK { $kind = CVC4::; } Parser::addOperator(kind::BITVECTOR_LSHR); - addOperator(kind::BITVECTOR_SMOD, "bvsmod"); // | BVSMOD_TOK { $kind = CVC4::; } Parser::addOperator(kind::BITVECTOR_ASHR); - addOperator(kind::BITVECTOR_ASHR, "bvashr"); // | BVASHR_TOK { $kind = CVC4::; } Parser::addOperator(kind::BITVECTOR_ULT); - addOperator(kind::BITVECTOR_ULE, "bvule"); // | BVULE_TOK { $kind = CVC4::; } Parser::addOperator(kind::BITVECTOR_ULE); - addOperator(kind::BITVECTOR_UGT, "bvugt"); // | BVUGT_TOK { $kind = CVC4::; } Parser::addOperator(kind::BITVECTOR_UGT); - addOperator(kind::BITVECTOR_UGE, "bvuge"); // | BVUGE_TOK { $kind = CVC4::; } Parser::addOperator(kind::BITVECTOR_UGE); - addOperator(kind::BITVECTOR_SLT, "bvslt"); // | BVSLT_TOK { $kind = CVC4::; } Parser::addOperator(kind::BITVECTOR_SLT); - addOperator(kind::BITVECTOR_SLE, "bvsle"); // | BVSLE_TOK { $kind = CVC4::; } Parser::addOperator(kind::BITVECTOR_SLE); - addOperator(kind::BITVECTOR_SGT, "bvsgt"); // | BVSGT_TOK { $kind = CVC4::; } Parser::addOperator(kind::BITVECTOR_SGT); - addOperator(kind::BITVECTOR_SGE, "bvsge"); // | BVSGE_TOK { $kind = CVC4::; } Parser::addOperator(kind::BITVECTOR_SGE); + addOperator(kind::BITVECTOR_CONCAT, "concat"); + addOperator(kind::BITVECTOR_NOT, "bvnot"); + addOperator(kind::BITVECTOR_AND, "bvand"); + addOperator(kind::BITVECTOR_OR, "bvor"); + addOperator(kind::BITVECTOR_NEG, "bvneg"); + addOperator(kind::BITVECTOR_PLUS, "bvadd"); + addOperator(kind::BITVECTOR_MULT, "bvmul"); + addOperator(kind::BITVECTOR_UDIV, "bvudiv"); + addOperator(kind::BITVECTOR_UREM, "bvurem"); + addOperator(kind::BITVECTOR_SHL, "bvshl"); + addOperator(kind::BITVECTOR_LSHR, "bvlshr"); + addOperator(kind::BITVECTOR_ULT, "bvult"); + addOperator(kind::BITVECTOR_NAND, "bvnand"); + addOperator(kind::BITVECTOR_NOR, "bvnor"); + addOperator(kind::BITVECTOR_XOR, "bvxor"); + addOperator(kind::BITVECTOR_XNOR, "bvxnor"); + addOperator(kind::BITVECTOR_COMP, "bvcomp"); + addOperator(kind::BITVECTOR_SUB, "bvsub"); + addOperator(kind::BITVECTOR_SDIV, "bvsdiv"); + addOperator(kind::BITVECTOR_SREM, "bvsrem"); + addOperator(kind::BITVECTOR_SMOD, "bvsmod"); + addOperator(kind::BITVECTOR_ASHR, "bvashr"); + addOperator(kind::BITVECTOR_ULE, "bvule"); + addOperator(kind::BITVECTOR_UGT, "bvugt"); + addOperator(kind::BITVECTOR_UGE, "bvuge"); + addOperator(kind::BITVECTOR_SLT, "bvslt"); + addOperator(kind::BITVECTOR_SLE, "bvsle"); + addOperator(kind::BITVECTOR_SGT, "bvsgt"); + addOperator(kind::BITVECTOR_SGE, "bvsge"); Parser::addOperator(kind::BITVECTOR_BITOF); Parser::addOperator(kind::BITVECTOR_EXTRACT); -- 2.30.2