From ef83f6744c1dcd1d5a90ea279cf77530d6de5b31 Mon Sep 17 00:00:00 2001
From: Morgan Deters <mdeters@gmail.com>
Date: Mon, 8 Oct 2012 16:00:58 +0000
Subject: [PATCH] fix SMT-LIBv2 compliance mode for bitvectors (was completely
 broken; didn't allow use of any BV ops

---
 src/parser/smt2/smt2.cpp | 40 ++++++++++++++++++++++++++++++++++++++++
 src/parser/smt2/smt2.h   |  2 ++
 2 files changed, 42 insertions(+)

diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp
index 45caf94a8..695d154e1 100644
--- 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 72310b5a4..48942265a 100644
--- 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 */
-- 
2.30.2