| 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; }
+ // | 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()) {
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';
+// 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';
}
void Smt2::addBitvectorOperators() {
- Parser::addOperator(kind::BITVECTOR_CONCAT);
- Parser::addOperator(kind::BITVECTOR_AND);
- Parser::addOperator(kind::BITVECTOR_OR);
- Parser::addOperator(kind::BITVECTOR_XOR);
- Parser::addOperator(kind::BITVECTOR_NOT);
- Parser::addOperator(kind::BITVECTOR_NAND);
- Parser::addOperator(kind::BITVECTOR_NOR);
- Parser::addOperator(kind::BITVECTOR_XNOR);
- Parser::addOperator(kind::BITVECTOR_COMP);
- Parser::addOperator(kind::BITVECTOR_MULT);
- Parser::addOperator(kind::BITVECTOR_PLUS);
- Parser::addOperator(kind::BITVECTOR_SUB);
- Parser::addOperator(kind::BITVECTOR_NEG);
- Parser::addOperator(kind::BITVECTOR_UDIV);
- Parser::addOperator(kind::BITVECTOR_UREM);
- Parser::addOperator(kind::BITVECTOR_SDIV);
- Parser::addOperator(kind::BITVECTOR_SREM);
- Parser::addOperator(kind::BITVECTOR_SMOD);
- Parser::addOperator(kind::BITVECTOR_SHL);
- Parser::addOperator(kind::BITVECTOR_LSHR);
- Parser::addOperator(kind::BITVECTOR_ASHR);
- Parser::addOperator(kind::BITVECTOR_ULT);
- Parser::addOperator(kind::BITVECTOR_ULE);
- Parser::addOperator(kind::BITVECTOR_UGT);
- Parser::addOperator(kind::BITVECTOR_UGE);
- Parser::addOperator(kind::BITVECTOR_SLT);
- Parser::addOperator(kind::BITVECTOR_SLE);
- Parser::addOperator(kind::BITVECTOR_SGT);
- Parser::addOperator(kind::BITVECTOR_SGE);
+ 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);
+
Parser::addOperator(kind::BITVECTOR_BITOF);
Parser::addOperator(kind::BITVECTOR_EXTRACT);
Parser::addOperator(kind::BITVECTOR_REPEAT);