dont tokenize bv operators (normal ones)

diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g
index 8b7c0bda2a38fb527d64c4630adb413f2ed357dc..467befca50b7fbd2fd1280d346ab2d51c8e5e7ba 100644 (file)
--- a/src/parser/smt2/Smt2.g
+++ b/src/parser/smt2/Smt2.g
@@ -2047,35 +2047,35 @@ 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; }
+  // | 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()) {
@@ -2518,35 +2518,36 @@ ABS_TOK : 'abs';
 
 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';
 

diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp
index 20f3c364ba5af042f06b6f02bc01d675e5e381ef..1f81e8ba145b9d6df59f1742ec441b3aa65dfe1a 100644 (file)
--- a/src/parser/smt2/smt2.cpp
+++ b/src/parser/smt2/smt2.cpp
@@ -50,35 +50,36 @@ void Smt2::addArithmeticOperators() {
 }
 
 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);