fix SMT-LIBv2 compliance mode for bitvectors (was completely broken; didn't allow...

diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp
index 45caf94a876b52a31a2cc77d9ad1e30495a13db1..695d154e1a112ae5da7f1e4e2dca770267cf8c44 100644 (file)
--- a/src/parser/smt2/smt2.cpp
+++ b/src/parser/smt2/smt2.cpp
@@ -45,6 +45,45 @@ void Smt2::addArithmeticOperators() {
   addOperator(kind::GEQ);
 }
 
+void Smt2::addBitvectorOperators() {
+  addOperator(kind::BITVECTOR_CONCAT);
+  addOperator(kind::BITVECTOR_AND);
+  addOperator(kind::BITVECTOR_OR);
+  addOperator(kind::BITVECTOR_XOR);
+  addOperator(kind::BITVECTOR_NOT);
+  addOperator(kind::BITVECTOR_NAND);
+  addOperator(kind::BITVECTOR_NOR);
+  addOperator(kind::BITVECTOR_XNOR);
+  addOperator(kind::BITVECTOR_COMP);
+  addOperator(kind::BITVECTOR_MULT);
+  addOperator(kind::BITVECTOR_PLUS);
+  addOperator(kind::BITVECTOR_SUB);
+  addOperator(kind::BITVECTOR_NEG);
+  addOperator(kind::BITVECTOR_UDIV);
+  addOperator(kind::BITVECTOR_UREM);
+  addOperator(kind::BITVECTOR_SDIV);
+  addOperator(kind::BITVECTOR_SREM);
+  addOperator(kind::BITVECTOR_SMOD);
+  addOperator(kind::BITVECTOR_SHL);
+  addOperator(kind::BITVECTOR_LSHR);
+  addOperator(kind::BITVECTOR_ASHR);
+  addOperator(kind::BITVECTOR_ULT);
+  addOperator(kind::BITVECTOR_ULE);
+  addOperator(kind::BITVECTOR_UGT);
+  addOperator(kind::BITVECTOR_UGE);
+  addOperator(kind::BITVECTOR_SLT);
+  addOperator(kind::BITVECTOR_SLE);
+  addOperator(kind::BITVECTOR_SGT);
+  addOperator(kind::BITVECTOR_SGE);
+  addOperator(kind::BITVECTOR_BITOF);
+  addOperator(kind::BITVECTOR_EXTRACT);
+  addOperator(kind::BITVECTOR_REPEAT);
+  addOperator(kind::BITVECTOR_ZERO_EXTEND);
+  addOperator(kind::BITVECTOR_SIGN_EXTEND);
+  addOperator(kind::BITVECTOR_ROTATE_LEFT);
+  addOperator(kind::BITVECTOR_ROTATE_RIGHT);
+}
+
 void Smt2::addTheory(Theory theory) {
   switch(theory) {
   case THEORY_CORE:
@@ -82,6 +121,7 @@ void Smt2::addTheory(Theory theory) {
     break;
 
   case THEORY_BITVECTORS:
+    addBitvectorOperators();
     break;
 
   case THEORY_QUANTIFIERS:

diff --git a/src/parser/smt2/smt2.h b/src/parser/smt2/smt2.h
index 72310b5a42a378583135a2487079b799c4df8231..48942265a1e2c6abfae4ac55e4f7b8f11e9f58ff 100644 (file)
--- a/src/parser/smt2/smt2.h
+++ b/src/parser/smt2/smt2.h
@@ -91,6 +91,8 @@ private:
 
   void addArithmeticOperators();
 
+  void addBitvectorOperators();
+
 };/* class Smt2 */
 
 }/* CVC4::parser namespace */