cleanup

diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g
index 467befca50b7fbd2fd1280d346ab2d51c8e5e7ba..8196a6276b0e0e39f70fca14808fc627f3d96002 100644 (file)
--- 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 1f81e8ba145b9d6df59f1742ec441b3aa65dfe1a..bc1f94f36a9552639fcfa5a5e104ba240cdb23e1 100644 (file)
--- 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);