Refactored CnfStream to work with the bv theory Bitblaster:

    * separated SatSolverInput interface class into two classes:
           - TheoryProxy for the sat solver to communicate with the theories
           - SatSolverInterface abstract class to communicate with the sat solver
    * instead of using #ifdef typedef for SatClauses and SatLiterals, now there are CVC4 SatLiteral/SatClause types and mappings between them and the internal sat solver clause/literal representation
    * added abstract classes for DPLLSatSolver and BVSatSolver different interfaces 

Replaced TheoryBV with bitblasting implementation:
    * all operators bitblasted
    * only operator elimination rewrite rules so far
  

21 files changed, 2367 insertions, 1836 deletions

diff --git a/src/theory/Makefile.am b/src/theory/Makefile.am
index c1a77d988..eb289937f 100644
--- a/src/theory/Makefile.am
+++ b/src/theory/Makefile.am
@@ -16,7 +16,7 @@ libtheory_la_SOURCES = \
 	theory_test_utils.h \
 	theory.h \
 	theory.cpp \
-	registrar.h \
+	theory_registrar.h \
 	rewriter.h \
 	rewriter_attributes.h \
 	rewriter.cpp \
diff --git a/src/theory/bv/Makefile.am b/src/theory/bv/Makefile.am
index 08dde4349..1b8e902e0 100644
--- a/src/theory/bv/Makefile.am
+++ b/src/theory/bv/Makefile.am
@@ -1,22 +1,26 @@
 AM_CPPFLAGS = \
 	-D__BUILDING_CVC4LIB \
+	-D __STDC_LIMIT_MACROS \
+	-D __STDC_FORMAT_MACROS \
 	-I@srcdir@/../../include -I@srcdir@/../.. -I@builddir@/../..
 AM_CXXFLAGS = -Wall -Wno-unknown-pragmas $(FLAG_VISIBILITY_HIDDEN)
 
 noinst_LTLIBRARIES = libbv.la
 
 libbv_la_SOURCES = \
+	theory_bv_utils.h \
+	bv_sat.h \
+	bv_sat.cpp \
+	bitblast_strategies.h \
+	bitblast_strategies.cpp \
 	theory_bv.h \
 	theory_bv.cpp \
-	theory_bv_utils.h \
 	theory_bv_rewrite_rules.h \
 	theory_bv_rewrite_rules_core.h \
+	theory_bv_rewrite_rules_arith.h \
 	theory_bv_type_rules.h \
 	theory_bv_rewriter.h \
 	theory_bv_rewriter.cpp \
-	equality_engine.h \
-	equality_engine.cpp \
-	slice_manager.h \
 	cd_set_collection.h 
 
 EXTRA_DIST = kinds
diff --git a/src/theory/bv/bitblast_strategies.cpp b/src/theory/bv/bitblast_strategies.cpp
new file mode 100644
index 000000000..b0a02c0a5
--- /dev/null
+++ b/src/theory/bv/bitblast_strategies.cpp
@@ -0,0 +1,824 @@
+/*********************                                                        */
+/*! \file bitblast_strategies.cpp
+ ** \verbatim
+ ** Original author: lianah
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 prototype.
+ ** Copyright (c) 2009, 2010, 2011  The Analysis of Computer Systems Group (ACSys)
+ ** Courant Institute of Mathematical Sciences
+ ** New York University
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.\endverbatim
+ **
+ ** \brief Implementation of bitblasting functions for various operators. 
+ **
+ ** Implementation of bitblasting functions for various operators. 
+ **/
+
+#include "bitblast_strategies.h"
+#include "bv_sat.h"
+#include "prop/sat_module.h"
+#include "theory/booleans/theory_bool_rewriter.h"
+
+using namespace CVC4::prop; 
+using namespace CVC4::theory::bv::utils;
+namespace CVC4 {
+namespace theory {
+namespace bv {
+
+/*
+  Purely debugging
+ */
+
+Bits* rewriteBits(const Bits& bits) {
+  Bits* newbits = new Bits(); 
+  for (unsigned i = 0; i < bits.size(); ++i) {
+    newbits->push_back(Rewriter::rewrite(bits[i])); 
+  }
+  return newbits;
+}
+
+Node rewrite(Node node) {
+  return Rewriter::rewrite(node); 
+}
+
+/*
+ Various helper functions that get called by the bitblasting procedures
+ */
+
+void inline extractBits(const Bits& b, Bits& dest, unsigned lo, unsigned hi) {
+  Assert ( lo < b.size() && hi < b.size() && lo <= hi);
+  for (unsigned i = lo; i <= hi; ++i) {
+    dest.push_back(b[i]); 
+  }
+}
+
+void inline negateBits(const Bits& bits, Bits& negated_bits) {
+  for(int i = 0; i < bits.size(); ++i) {
+    negated_bits.push_back(utils::mkNot(bits[i])); 
+  }
+}
+
+bool inline isZero(const Bits& bits) {
+  for(int i = 0; i < bits.size(); ++i) {
+    if(bits[i] != mkFalse()) {
+      return false; 
+    }
+  }
+  return true; 
+}
+
+void inline rshift(Bits& bits, unsigned amount) {
+  for (unsigned i = 0; i < bits.size() - amount; ++i) {
+    bits[i] = bits[i+amount]; 
+  }
+  for(unsigned i = bits.size() - amount; i < bits.size(); ++i) {
+    bits[i] = mkFalse(); 
+  }
+}
+
+void inline lshift(Bits& bits, unsigned amount) {
+  for (int i = bits.size() - 1; i >= amount ; --i) {
+    bits[i] = bits[i-amount]; 
+  }
+  for(unsigned i = 0; i < amount; ++i) {
+    bits[i] = mkFalse(); 
+  }
+}
+
+void inline makeZero(Bits& bits, unsigned width) {
+  Assert(bits.size() == 0); 
+  for(unsigned i = 0; i < width; ++i) {
+    bits.push_back(mkFalse()); 
+  }
+}
+
+
+/** 
+ * Constructs a simple ripple carry adder
+ * 
+ * @param a first term to be added
+ * @param b second term to be added
+ * @param sum the sum 
+ * @param carry the carry-in bit 
+ * 
+ * @return the carry-out
+ */
+Node inline rippleCarryAdder(const Bits&a, const Bits& b, Bits& res, Node carry) {
+  Assert(res.size() == 0 && a.size() == b.size());
+  
+  for (unsigned i = 0 ; i < a.size(); ++i) {
+    Node sum = mkXor(mkXor(a[i], b[i]), carry);
+    carry = mkOr( mkAnd(a[i], b[i]),
+                  mkAnd( mkXor(a[i], b[i]),
+                         carry));
+    res.push_back(sum); 
+  }
+
+  return carry;
+}
+
+
+Node inline uLessThanBB(const Bits&a, const Bits& b, bool orEqual) {
+  Assert (a.size() && b.size());
+  
+  Node res = mkNode(kind::AND, mkNode(kind::NOT, a[0]), b[0]);
+  
+  if(orEqual) {
+    res = mkNode(kind::OR, res, mkNode(kind::IFF, a[0], b[0])); 
+  }
+  
+  for (unsigned i = 1; i < a.size(); ++i) {
+    // a < b iff ( a[i] <-> b[i] AND a[i-1:0] < b[i-1:0]) OR (~a[i] AND b[i]) 
+    res = mkNode(kind::OR,
+                 mkNode(kind::AND, mkNode(kind::IFF, a[i], b[i]), res),
+                 mkNode(kind::AND, mkNode(kind::NOT, a[i]), b[i])); 
+  }
+  return res;
+}
+
+Node inline sLessThanBB(const Bits&a, const Bits& b, bool orEqual) {
+  Assert (a.size() && b.size());
+  if (a.size() == 1) {
+    if(orEqual) {
+      return  mkNode(kind::OR,
+                     mkNode(kind::IFF, a[0], b[0]),
+                     mkNode(kind::AND, a[0], mkNode(kind::NOT, b[0]))); 
+    }
+
+    return mkNode(kind::AND, a[0], mkNode(kind::NOT, b[0]));
+  }
+  unsigned n = a.size() - 1; 
+  Bits a1, b1;
+  extractBits(a, a1, 0, n-1);
+  extractBits(b, b1, 0, n-1);
+  
+  // unsigned comparison of the first n-1 bits
+  Node ures = uLessThanBB(a1, b1, orEqual);
+  Node res = mkNode(kind::OR,
+                    // a b have the same sign
+                    mkNode(kind::AND,
+                           mkNode(kind::IFF, a[n], b[n]),
+                           ures),
+                    // a is negative and b positive
+                    mkNode(kind::AND,
+                           a[n],
+                           mkNode(kind::NOT, b[n])));
+  return res;
+}
+
+
+/*
+  Atom bitblasting strategies 
+ */
+
+
+Node UndefinedAtomBBStrategy(TNode node, Bitblaster* bb) {
+  Debug("bitvector") << "TheoryBV::Bitblaster Undefined bitblasting strategy for kind: "
+                     << node.getKind() << "\n";
+  Unreachable(); 
+}
+
+Node DefaultEqBB(TNode node, Bitblaster* bb) {
+  Debug("bitvector-bb") << "Bitblasting node " << node  << "\n";
+  
+  Assert(node.getKind() == kind::EQUAL);
+  Bits lhs, rhs; 
+  bb->bbTerm(node[0], lhs);
+  bb->bbTerm(node[1], rhs);
+
+  Assert(lhs.size() == rhs.size());
+
+  NodeManager* nm = NodeManager::currentNM();
+
+  std::vector<Node> bits_eq;
+  for (unsigned i = 0; i < lhs.size(); i++) {
+    Node bit_eq = nm->mkNode(kind::IFF, lhs[i], rhs[i]);
+    bits_eq.push_back(bit_eq); 
+  }
+  Node bv_eq = utils::mkAnd(bits_eq);
+  return bv_eq; 
+}
+
+
+Node AdderUltBB(TNode node, Bitblaster* bb) {
+  Debug("bitvector-bb") << "Bitblasting node " << node  << "\n";
+  Assert(node.getKind() == kind::BITVECTOR_ULT);
+  Bits a, b;
+  bb->bbTerm(node[0], a);
+  bb->bbTerm(node[1], b);
+  Assert(a.size() == b.size());
+  
+  // a < b <=> ~ (add(a, ~b, 1).carry_out)
+  Bits not_b;
+  negateBits(b, not_b);
+  Node carry = mkTrue();
+  
+  for (unsigned i = 0 ; i < a.size(); ++i) {
+    carry = mkOr( mkAnd(a[i], not_b[i]),
+                  mkAnd( mkXor(a[i], not_b[i]),
+                         carry));
+  }
+  return mkNot(carry); 
+}
+
+
+Node DefaultUltBB(TNode node, Bitblaster* bb) {
+  Debug("bitvector-bb") << "Bitblasting node " << node  << "\n";
+  Assert(node.getKind() == kind::BITVECTOR_ULT);
+  Bits a, b;
+  bb->bbTerm(node[0], a);
+  bb->bbTerm(node[1], b);
+  Assert(a.size() == b.size());
+  
+  // construct bitwise comparison 
+  Node res = uLessThanBB(a, b, false);
+  return res; 
+}
+
+Node DefaultUleBB(TNode node, Bitblaster* bb){
+  Debug("bitvector-bb") << "Bitblasting node " << node  << "\n";
+  Assert(node.getKind() == kind::BITVECTOR_ULE);
+  Bits a, b;
+  
+  bb->bbTerm(node[0], a);
+  bb->bbTerm(node[1], b);
+  Assert(a.size() == b.size());
+  // construct bitwise comparison 
+  Node res = uLessThanBB(a, b, true);
+  return res; 
+}
+
+Node DefaultUgtBB(TNode node, Bitblaster* bb){
+  Debug("bitvector-bb") << "Bitblasting node " << node  << "\n";
+  // should be rewritten 
+  Unimplemented(); 
+}
+Node DefaultUgeBB(TNode node, Bitblaster* bb){
+  Debug("bitvector-bb") << "Bitblasting node " << node  << "\n";
+  // should be rewritten 
+  Unimplemented(); 
+}
+
+Node DefaultSltBB(TNode node, Bitblaster* bb){
+  Debug("bitvector-bb") << "Bitblasting node " << node  << "\n";
+
+  Bits a, b;
+  bb->bbTerm(node[0], a);
+  bb->bbTerm(node[1], b);
+  Assert(a.size() == b.size());
+  
+  Node res = sLessThanBB(a, b, false); 
+  return res;
+}
+
+Node DefaultSleBB(TNode node, Bitblaster* bb){
+  Debug("bitvector-bb") << "Bitblasting node " << node  << "\n";
+
+  Bits a, b;
+  bb->bbTerm(node[0], a);
+  bb->bbTerm(node[1], b);
+  Assert(a.size() == b.size());
+  
+  Node res = sLessThanBB(a, b, true); 
+  return res;
+}
+ 
+Node DefaultSgtBB(TNode node, Bitblaster* bb){
+  Debug("bitvector-bb") << "Bitblasting node " << node  << "\n";
+  // should be rewritten 
+  Unimplemented(); 
+}
+
+Node DefaultSgeBB(TNode node, Bitblaster* bb){
+  Debug("bitvector-bb") << "Bitblasting node " << node  << "\n";
+  // should be rewritten 
+  Unimplemented(); 
+}
+
+
+/// Term bitblasting strategies 
+
+void UndefinedTermBBStrategy(TNode node, Bits& bits, Bitblaster* bb) {
+  Debug("bitvector") << "theory::bv:: Undefined bitblasting strategy for kind: "
+                     << node.getKind() << "\n";
+  Unreachable(); 
+}
+
+void DefaultVarBB (TNode node, Bits& bits, Bitblaster* bb) {
+  Assert (node.getKind() == kind::VARIABLE);
+  Assert(bits.size() == 0);
+  
+  for (unsigned i = 0; i < utils::getSize(node); ++i) {
+    bits.push_back(utils::mkBitOf(node, i));
+  }
+
+  Debug("bitvector-bb") << "theory::bv::DefaultVarBB bitblasting  " << node << "\n";
+  Debug("bitvector-bb") << "                           with bits  " << toString(bits); 
+}
+
+void DefaultConstBB (TNode node, Bits& bits, Bitblaster* bb) {
+  Debug("bitvector-bb") << "theory::bv::DefaultConstBB bitblasting " << node << "\n";
+  Assert(node.getKind() == kind::CONST_BITVECTOR);
+  Assert(bits.size() == 0);
+  
+  NodeManager* nm = NodeManager::currentNM(); 
+  for (unsigned i = 0; i < utils::getSize(node); ++i) {
+    Integer bit = node.getConst<BitVector>().extract(i, i).getValue();
+    if(bit == Integer(0)){
+      bits.push_back(utils::mkFalse());
+    } else {
+      Assert (bit == Integer(1));
+      bits.push_back(utils::mkTrue()); 
+    }
+  }
+  Debug("bitvector-bb") << "with  bits: " << toString(bits) << "\n"; 
+}
+
+
+void DefaultNotBB (TNode node, Bits& bits, Bitblaster* bb) {
+  Debug("bitvector-bb") << "theory::bv::DefaultNotBB bitblasting " << node << "\n";
+  Assert(node.getKind() == kind::BITVECTOR_NOT);
+  Assert(bits.size() == 0);
+  Bits bv; 
+  bb->bbTerm(node[0], bv);
+  negateBits(bv, bits);
+}
+
+void DefaultConcatBB (TNode node, Bits& bits, Bitblaster* bb) {
+  Debug("bitvector-bb") << "theory::bv::DefaultConcatBB bitblasting " << node << "\n";
+  Assert(bits.size() == 0);
+  
+  Assert (node.getKind() == kind::BITVECTOR_CONCAT);
+  for (int i = node.getNumChildren() -1 ; i >= 0; --i ) {
+    TNode current = node[i];
+    Bits current_bits; 
+    bb->bbTerm(current, current_bits);
+
+    for(unsigned j = 0; j < utils::getSize(current); ++j) {
+      bits.push_back(current_bits[j]);
+    }
+  }
+  Assert (bits.size() == utils::getSize(node)); 
+  Debug("bitvector-bb") << "with  bits: " << toString(bits) << "\n"; 
+}
+
+
+void DefaultAndBB (TNode node, Bits& bits, Bitblaster* bb) {
+  Debug("bitvector-bb") << "theory::bv::DefaultAndBB bitblasting " << node << "\n";
+
+  Assert(node.getNumChildren() == 2 &&
+         node.getKind() == kind::BITVECTOR_AND &&
+         bits.size() == 0);
+  
+  Bits lhs, rhs;
+  bb->bbTerm(node[0], rhs);
+  bb->bbTerm(node[1], lhs);
+
+  Assert (lhs.size() == rhs.size()); 
+  for (unsigned i = 0; i < lhs.size(); ++i) {
+    bits.push_back(utils::mkAnd(lhs[i], rhs[i])); 
+  }
+
+}
+
+void DefaultOrBB (TNode node, Bits& bits, Bitblaster* bb) {
+  Debug("bitvector-bb") << "theory::bv::DefaultOrBB bitblasting " << node << "\n";
+
+  Assert(node.getNumChildren() == 2 &&
+         node.getKind() == kind::BITVECTOR_OR &&
+         bits.size() == 0);
+  
+  Bits lhs, rhs;
+  bb->bbTerm(node[0], lhs);
+  bb->bbTerm(node[1], rhs);
+  Assert(lhs.size() == rhs.size()); 
+  
+  for (unsigned i = 0; i < lhs.size(); ++i) {
+    bits.push_back(utils::mkOr(lhs[i], rhs[i])); 
+  }
+}
+
+void DefaultXorBB (TNode node, Bits& bits, Bitblaster* bb) {
+  Debug("bitvector-bb") << "theory::bv::DefaultXorBB bitblasting " << node << "\n";
+
+  Assert(node.getNumChildren() == 2 &&
+         node.getKind() == kind::BITVECTOR_XOR &&
+         bits.size() == 0);
+  
+  Bits lhs, rhs;
+  bb->bbTerm(node[0], lhs);
+  bb->bbTerm(node[1], rhs);
+  Assert(lhs.size() == rhs.size()); 
+  
+  for (unsigned i = 0; i < lhs.size(); ++i) {
+    bits.push_back(utils::mkXor(lhs[i], rhs[i])); 
+  }
+}
+
+void DefaultXnorBB (TNode node, Bits& bits, Bitblaster* bb) {
+  Debug("bitvector-bb") << "theory::bv::DefaultXnorBB bitblasting " << node << "\n";
+
+  Assert(node.getNumChildren() == 2 &&
+         node.getKind() == kind::BITVECTOR_XNOR &&
+         bits.size() == 0);
+  Bits lhs, rhs;
+  bb->bbTerm(node[0], lhs);
+  bb->bbTerm(node[1], rhs);
+  Assert(lhs.size() == rhs.size()); 
+  
+  for (unsigned i = 0; i < lhs.size(); ++i) {
+    bits.push_back(utils::mkNode(kind::IFF, lhs[i], rhs[i])); 
+  }
+}
+
+
+void DefaultNandBB (TNode node, Bits& bits, Bitblaster* bb) {
+  Debug("bitvector") << "theory::bv:: Unimplemented kind "
+                     << node.getKind() << "\n";
+  Unimplemented(); 
+}
+void DefaultNorBB (TNode node, Bits& bits, Bitblaster* bb) {
+  Debug("bitvector") << "theory::bv:: Unimplemented kind "
+                     << node.getKind() << "\n";
+  Unimplemented(); 
+}
+void DefaultCompBB (TNode node, Bits& bits, Bitblaster* bb) {
+  Debug("bitvector") << "theory::bv:: DefaultCompBB bitblasting "<< node << "\n";
+
+  Assert(getSize(node) == 1 && bits.size() == 0 && node.getKind() == kind::BITVECTOR_COMP);
+  Bits a, b;
+  bb->bbTerm(node[0], a);
+  bb->bbTerm(node[1], b);
+
+  std::vector<Node> bit_eqs;
+  NodeManager* nm = NodeManager::currentNM(); 
+  for (unsigned i = 0; i < a.size(); ++i) {
+    Node eq = nm->mkNode(kind::IFF, a[i], b[i]);
+    bit_eqs.push_back(eq); 
+  }
+  Node a_eq_b = mkAnd(bit_eqs);
+  bits.push_back(a_eq_b);   
+}
+
+void DefaultMultBB (TNode node, Bits& res, Bitblaster* bb) {
+  Debug("bitvector") << "theory::bv:: DefaultMultBB bitblasting "<< node << "\n";
+  Assert(res.size() == 0 &&
+         node.getKind() == kind::BITVECTOR_MULT);
+  Bits a, b;
+  bb->bbTerm(node[0], a);
+  bb->bbTerm(node[1], b);
+
+  // constructs a simple shift and add multiplier building the result in
+  // in res
+  
+  for (unsigned i = 0; i < a.size(); ++i) {
+    res.push_back(mkNode(kind::AND, b[0], a[i])); 
+  }
+  
+  for(unsigned k = 1; k < res.size(); ++k) {
+  Node carry_in = mkFalse();
+  Node carry_out;
+    for(unsigned j = 0; j < res.size() -k; ++j) {
+      Node aj = mkAnd(a[j], b[k]);
+      carry_out = mkOr(mkAnd(res[j+k], aj),
+                       mkAnd( mkXor(res[j+k], aj), carry_in));
+      res[j+k] = mkXor(mkXor(res[j+k], aj), carry_in);
+      carry_in = carry_out; 
+    }
+  }
+  Debug("bitvector-bb") << "with bits: " << toString(res)  << "\n";
+}
+
+void DefaultPlusBB (TNode node, Bits& res, Bitblaster* bb) {
+  Debug("bitvector-bb") << "theory::bv::DefaulPlusBB bitblasting " << node << "\n";
+  Assert(node.getKind() == kind::BITVECTOR_PLUS &&
+         res.size() == 0);
+
+  Bits a, b;
+  bb->bbTerm(node[0], a);
+  bb->bbTerm(node[1], b); 
+
+  Assert(a.size() == b.size() && utils::getSize(node) == a.size());
+  rippleCarryAdder(a, b, res, mkFalse());
+}
+
+
+void DefaultSubBB (TNode node, Bits& bits, Bitblaster* bb) {
+  Debug("bitvector-bb") << "theory::bv::DefautSubBB bitblasting " << node << "\n";
+  Assert(node.getKind() == kind::BITVECTOR_SUB &&  bits.size() == 0);
+    
+  Bits a, b;
+  bb->bbTerm(node[0], a);
+  bb->bbTerm(node[1], b); 
+  Assert(a.size() == b.size() && utils::getSize(node) == a.size());
+
+  // bvsub a b = adder(a, ~b, 1)
+  Bits not_b;
+  negateBits(b, not_b);
+  Node carry = utils::mkTrue();
+  rippleCarryAdder(a, not_b, bits, mkTrue());
+}
+
+void DefaultNegBB (TNode node, Bits& bits, Bitblaster* bb) {
+  Debug("bitvector-bb") << "theory::bv::DefautNegBB bitblasting " << node << "\n";
+  Assert(node.getKind() == kind::BITVECTOR_NEG);
+  
+  Bits a;
+  bb->bbTerm(node[0], a);
+  Assert(utils::getSize(node) == a.size());
+
+  // -a = add(~a, 0, 1).
+  Bits not_a;
+  negateBits(a, not_a);
+  Bits zero;
+  makeZero(zero, getSize(node)); 
+  
+  rippleCarryAdder(not_a, zero, bits, mkTrue()); 
+}
+
+void uDivModRec(const Bits& a, const Bits& b, Bits& q, Bits& r, unsigned rec_width) {
+  Assert( q.size() == 0 && r.size() == 0);
+
+  if(rec_width == 0 || isZero(a)) {
+    makeZero(q, a.size());
+    makeZero(r, a.size());
+    return;
+  } 
+  
+  Bits q1, r1;
+  Bits a1 = a;
+  rshift(a1, 1); 
+
+  uDivModRec(a1, b, q1, r1, rec_width - 1);
+  // shift the quotient and remainder (i.e. multiply by two) and add 1 to remainder if a is odd
+  lshift(q1, 1);
+  lshift(r1, 1);
+
+  
+  Node is_odd = mkNode(kind::IFF, a[0], mkTrue());
+  Node one_if_odd = mkNode(kind::ITE, is_odd, mkTrue(), mkFalse()); 
+
+  Bits zero;
+  makeZero(zero, b.size());
+  
+  Bits r1_shift_add;
+  // account for a being odd
+  rippleCarryAdder(r1, zero, r1_shift_add, one_if_odd); 
+  // now check if the remainder is greater than b
+  Bits not_b;
+  negateBits(b, not_b);
+  Bits r_minus_b;
+  Node co1;
+  // use adder because we need r_minus_b anyway
+  co1 = rippleCarryAdder(r1_shift_add, not_b, r_minus_b, mkTrue()); 
+  // sign is true if r1 < b
+  Node sign = mkNode(kind::NOT, co1); 
+  
+  q1[0] = mkNode(kind::ITE, sign, q1[0], mkTrue());
+
+  // would be nice to have a high level ITE instead of bitwise
+  for(unsigned i = 0; i < a.size(); ++i) {
+    r1_shift_add[i] = mkNode(kind::ITE, sign, r1_shift_add[i], r_minus_b[i]); 
+  }
+
+  // check if a < b
+
+  Bits a_minus_b;
+  Node co2 = rippleCarryAdder(a, not_b, a_minus_b, mkTrue());
+  // Node a_lt_b = a_minus_b.back();
+  Node a_lt_b = mkNode(kind::NOT, co2); 
+  
+  for(unsigned i = 0; i < a.size(); ++i) {
+    Node qval = mkNode(kind::ITE, a_lt_b, mkFalse(), q1[i]);
+    Node rval = mkNode(kind::ITE, a_lt_b, a[i], r1_shift_add[i]);
+    q.push_back(qval);
+    r.push_back(rval); 
+  }
+
+}
+
+void DefaultUdivBB (TNode node, Bits& q, Bitblaster* bb) {
+  Debug("bitvector-bb") << "theory::bv::DefautUdivBB bitblasting " << node << "\n";
+  Assert(node.getKind() == kind::BITVECTOR_UDIV &&  q.size() == 0);
+
+  Bits a, b;
+  bb->bbTerm(node[0], a);
+  bb->bbTerm(node[1], b);
+
+  Bits r;
+  uDivModRec(a, b, q, r, getSize(node)); 
+
+  // cache the remainder in case we need it later
+  Node remainder = mkNode(kind::BITVECTOR_UREM, node[0], node[1]);
+  bb->cacheTermDef(remainder, r);
+}
+
+void DefaultUremBB (TNode node, Bits& rem, Bitblaster* bb) {
+  Debug("bitvector-bb") << "theory::bv::DefautUremBB bitblasting " << node << "\n";
+  Assert(node.getKind() == kind::BITVECTOR_UREM &&  rem.size() == 0);
+
+  Bits a, b;
+  bb->bbTerm(node[0], a);
+  bb->bbTerm(node[1], b);
+
+  Bits q;
+  uDivModRec(a, b, q, rem, getSize(node)); 
+
+  // cache the quotient in case we need it later
+  Node quotient = mkNode(kind::BITVECTOR_UDIV, node[0], node[1]);
+  bb->cacheTermDef(quotient, q);
+}
+
+
+void DefaultSdivBB (TNode node, Bits& bits, Bitblaster* bb) {
+  Debug("bitvector") << "theory::bv:: Unimplemented kind "
+                     << node.getKind() << "\n";
+  Unimplemented(); 
+}
+void DefaultSremBB (TNode node, Bits& bits, Bitblaster* bb) {
+  Debug("bitvector") << "theory::bv:: Unimplemented kind "
+                     << node.getKind() << "\n";
+  Unimplemented(); 
+}
+void DefaultSmodBB (TNode node, Bits& bits, Bitblaster* bb) {
+  Debug("bitvector") << "theory::bv:: Unimplemented kind "
+                     << node.getKind() << "\n";
+  Unimplemented(); 
+}
+
+void DefaultShlBB (TNode node, Bits& res, Bitblaster* bb) {
+  Debug("bitvector-bb") << "theory::bv::DefaultShlBB bitblasting " << node  << "\n";
+  Assert (node.getKind() == kind::BITVECTOR_SHL &&
+          res.size() == 0);
+  Bits a, b;
+  bb->bbTerm(node[0], a);
+  bb->bbTerm(node[1], b);
+
+  res = a;
+  Bits prev_res;
+  
+  for(unsigned s = 0; s < b.size(); ++s) {
+    // barrel shift stage: at each stage you can either shift by 2^s bits
+    // or leave the previous stage untouched
+    prev_res = res; 
+    unsigned threshold = pow(2, s); 
+    for(unsigned i = 0; i < a.size(); ++i) {
+      if (i < threshold) {
+        // if b[s] is true then we must have shifted by at least 2^b bits so
+        // all bits bellow 2^s will be 0, otherwise just use previous shift value
+        res[i] = mkNode(kind::ITE, b[s], mkFalse(), prev_res[i]);
+      } else {
+        // if b[s]= 0, use previous value, otherwise shift by threshold  bits
+        Assert(i >= threshold); 
+        res[i] = mkNode(kind::ITE, mkNot(b[s]), prev_res[i], prev_res[i-threshold]); 
+      }
+    }
+  }
+  Debug("bitvector-bb") << "with bits: " << toString(res)  << "\n";
+}
+
+void DefaultLshrBB (TNode node, Bits& res, Bitblaster* bb) {
+  Debug("bitvector-bb") << "theory::bv::DefaultLshrBB bitblasting " << node  << "\n";
+  Assert (node.getKind() == kind::BITVECTOR_LSHR &&
+          res.size() == 0);
+  Bits a, b;
+  bb->bbTerm(node[0], a);
+  bb->bbTerm(node[1], b);
+
+  res = a;
+  Bits prev_res;
+  
+  for(int s = 0; s < b.size(); ++s) {
+    // barrel shift stage: at each stage you can either shift by 2^s bits
+    // or leave the previous stage untouched
+    prev_res = res; 
+    int threshold = pow(2, s); 
+    for(int i = 0; i < a.size(); ++i) {
+      if (i + threshold >= a.size()) {
+        // if b[s] is true then we must have shifted by at least 2^b bits so
+        // all bits above 2^s will be 0, otherwise just use previous shift value
+        res[i] = mkNode(kind::ITE, b[s], mkFalse(), prev_res[i]);
+      } else {
+        // if b[s]= 0, use previous value, otherwise shift by threshold  bits
+        Assert (i+ threshold < a.size()); 
+        res[i] = mkNode(kind::ITE, mkNot(b[s]), prev_res[i], prev_res[i+threshold]);
+      }
+    }
+  }
+  Debug("bitvector-bb") << "with bits: " << toString(res)  << "\n";
+}
+
+void DefaultAshrBB (TNode node, Bits& res, Bitblaster* bb) {
+
+  Debug("bitvector-bb") << "theory::bv::DefaultAshrBB bitblasting " << node  << "\n";
+  Assert (node.getKind() == kind::BITVECTOR_ASHR &&
+          res.size() == 0);
+  Bits a, b;
+  bb->bbTerm(node[0], a);
+  bb->bbTerm(node[1], b);
+
+  res = a;
+  TNode sign_bit = a.back();
+  Bits prev_res;
+
+  for(int s = 0; s < b.size(); ++s) {
+    // barrel shift stage: at each stage you can either shift by 2^s bits
+    // or leave the previous stage untouched
+    prev_res = res; 
+    int threshold = pow(2, s); 
+    for(int i = 0; i < a.size(); ++i) {
+      if (i + threshold >= a.size()) {
+        // if b[s] is true then we must have shifted by at least 2^b bits so
+        // all bits above 2^s will be the sign bit, otherwise just use previous shift value
+        res[i] = mkNode(kind::ITE, b[s], sign_bit, prev_res[i]);
+      } else {
+        // if b[s]= 0, use previous value, otherwise shift by threshold  bits
+        Assert (i+ threshold < a.size()); 
+        res[i] = mkNode(kind::ITE, mkNot(b[s]), prev_res[i], prev_res[i+threshold]);
+      }
+    }
+  }
+  Debug("bitvector-bb") << "with bits: " << toString(res)  << "\n";
+
+}
+
+void DefaultExtractBB (TNode node, Bits& bits, Bitblaster* bb) {
+  Assert (node.getKind() == kind::BITVECTOR_EXTRACT);
+  Assert(bits.size() == 0);
+  
+  Bits base_bits;
+  bb->bbTerm(node[0], base_bits);
+  unsigned high = utils::getExtractHigh(node);
+  unsigned low  = utils::getExtractLow(node);
+
+  for (unsigned i = low; i <= high; ++i) {
+    bits.push_back(base_bits[i]); 
+  }
+  Assert (bits.size() == high - low + 1);   
+
+  Debug("bitvector-bb") << "theory::bv::DefaultExtractBB bitblasting " << node << "\n";
+  Debug("bitvector-bb") << "                               with bits " << toString(bits); 
+       
+}
+
+
+void DefaultRepeatBB (TNode node, Bits& bits, Bitblaster* bb) {
+  Debug("bitvector") << "theory::bv:: Unimplemented kind "
+                     << node.getKind() << "\n";
+  // this should be rewritten 
+  Unimplemented(); 
+}
+
+void DefaultZeroExtendBB (TNode node, Bits& res_bits, Bitblaster* bb) {
+
+  Debug("bitvector-bb") << "theory::bv::DefaultZeroExtendBB bitblasting " << node  << "\n";
+ 
+  // this should be rewritten 
+  Unimplemented();
+  
+}
+
+void DefaultSignExtendBB (TNode node, Bits& res_bits, Bitblaster* bb) {
+  Debug("bitvector-bb") << "theory::bv::DefaultSignExtendBB bitblasting " << node  << "\n";
+
+  Assert (node.getKind() == kind::BITVECTOR_SIGN_EXTEND &&
+          res_bits.size() == 0);
+
+  Bits bits;
+  bb->bbTerm(node[0], bits);
+  
+  TNode sign_bit = bits.back(); 
+  unsigned amount = node.getOperator().getConst<BitVectorSignExtend>().signExtendAmount; 
+
+  for (unsigned i = 0; i < bits.size(); ++i ) {
+    res_bits.push_back(bits[i]); 
+  }
+         
+  for (unsigned i = 0 ; i < amount ; ++i ) {
+    res_bits.push_back(sign_bit); 
+  }
+         
+  Assert (res_bits.size() == amount + bits.size()); 
+}
+
+void DefaultRotateRightBB (TNode node, Bits& res, Bitblaster* bb) {
+  Debug("bitvector") << "theory::bv:: Unimplemented kind "
+                     << node.getKind() << "\n";
+
+  Unimplemented(); 
+}
+
+void DefaultRotateLeftBB (TNode node, Bits& bits, Bitblaster* bb) {
+  Debug("bitvector") << "theory::bv:: Unimplemented kind "
+                     << node.getKind() << "\n";
+  Unimplemented(); 
+}
+
+
+}
+}
+}
+
+
diff --git a/src/theory/bv/bitblast_strategies.h b/src/theory/bv/bitblast_strategies.h
new file mode 100644
index 000000000..504755e6c
--- /dev/null
+++ b/src/theory/bv/bitblast_strategies.h
@@ -0,0 +1,112 @@
+/*********************                                                        */
+/*! \file bitblast_strategies.h
+ ** \verbatim
+ ** Original author: lianah
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 prototype.
+ ** Copyright (c) 2009, 2010, 2011  The Analysis of Computer Systems Group (ACSys)
+ ** Courant Institute of Mathematical Sciences
+ ** New York University
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.\endverbatim
+ **
+ ** \brief Implementation of bitblasting functions for various operators. 
+ **
+ ** Implementation of bitblasting functions for various operators. 
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef __CVC4__BITBLAST__STRATEGIES_H
+#define __CVC4__BITBLAST__STRATEGIES_H
+
+
+#include "expr/node.h"
+#include "prop/sat_module.h"
+
+namespace CVC4 {
+
+
+namespace theory {
+namespace bv {
+
+class Bitblaster;
+
+
+typedef std::vector<Node>    Bits; 
+
+
+/** 
+ * Default Atom Bitblasting strategies: 
+ * 
+ * @param node the atom to be bitblasted
+ * @param markerLit the marker literal corresponding to the atom
+ * @param bb the bitblaster
+ */
+
+Node UndefinedAtomBBStrategy (TNode node, Bitblaster* bb);                               
+Node DefaultEqBB(TNode node, Bitblaster* bb);
+
+Node DefaultUltBB(TNode node, Bitblaster* bb);
+Node DefaultUleBB(TNode node, Bitblaster* bb);
+Node DefaultUgtBB(TNode node, Bitblaster* bb);
+Node DefaultUgeBB(TNode node, Bitblaster* bb);
+
+Node DefaultSltBB(TNode node, Bitblaster* bb);
+Node DefaultSleBB(TNode node, Bitblaster* bb);
+Node DefaultSgtBB(TNode node, Bitblaster* bb);
+Node DefaultSgeBB(TNode node, Bitblaster* bb);
+
+/// other modes
+Node AdderUltBB(TNode node, Bitblaster* bb);
+
+
+
+/** 
+ * Default Term Bitblasting strategies
+ * 
+ * @param node the term to be bitblasted
+ * @param bb the bitblaster in which the clauses are added
+ * 
+ * @return the bits representing the new term 
+ */
+
+void UndefinedTermBBStrategy(TNode node, Bits& bits, Bitblaster* bb); 
+
+void DefaultVarBB         (TNode node, Bits& bits, Bitblaster* bb);
+void DefaultConstBB       (TNode node, Bits& bits, Bitblaster* bb);
+void DefaultNotBB         (TNode node, Bits& bits, Bitblaster* bb);
+void DefaultConcatBB      (TNode node, Bits& bits, Bitblaster* bb);
+void DefaultAndBB         (TNode node, Bits& bits, Bitblaster* bb);
+void DefaultOrBB          (TNode node, Bits& bits, Bitblaster* bb);
+void DefaultXorBB         (TNode node, Bits& bits, Bitblaster* bb);
+void DefaultXnorBB         (TNode node, Bits& bits, Bitblaster* bb);
+void DefaultNandBB        (TNode node, Bits& bits, Bitblaster* bb);
+void DefaultNorBB         (TNode node, Bits& bits, Bitblaster* bb);
+void DefaultCompBB        (TNode node, Bits& bits, Bitblaster* bb);
+void DefaultMultBB        (TNode node, Bits& bits, Bitblaster* bb);
+void DefaultPlusBB        (TNode node, Bits& bits, Bitblaster* bb);
+void DefaultSubBB         (TNode node, Bits& bits, Bitblaster* bb);
+void DefaultNegBB         (TNode node, Bits& bits, Bitblaster* bb);
+void DefaultUdivBB        (TNode node, Bits& bits, Bitblaster* bb);
+void DefaultUremBB        (TNode node, Bits& bits, Bitblaster* bb);
+void DefaultSdivBB        (TNode node, Bits& bits, Bitblaster* bb);
+void DefaultSremBB        (TNode node, Bits& bits, Bitblaster* bb);
+void DefaultSmodBB        (TNode node, Bits& bits, Bitblaster* bb);
+void DefaultShlBB         (TNode node, Bits& bits, Bitblaster* bb);
+void DefaultLshrBB        (TNode node, Bits& bits, Bitblaster* bb);
+void DefaultAshrBB        (TNode node, Bits& bits, Bitblaster* bb);
+void DefaultExtractBB     (TNode node, Bits& bits, Bitblaster* bb);
+void DefaultRepeatBB      (TNode node, Bits& bits, Bitblaster* bb);
+void DefaultZeroExtendBB  (TNode node, Bits& bits, Bitblaster* bb);
+void DefaultSignExtendBB  (TNode node, Bits& bits, Bitblaster* bb);
+void DefaultRotateRightBB (TNode node, Bits& bits, Bitblaster* bb);
+void DefaultRotateLeftBB  (TNode node, Bits& bits, Bitblaster* bb);
+
+
+}
+}
+}
+
+#endif
diff --git a/src/theory/bv/bv_sat.cpp b/src/theory/bv/bv_sat.cpp
new file mode 100644
index 000000000..22a679693
--- /dev/null
+++ b/src/theory/bv/bv_sat.cpp
@@ -0,0 +1,300 @@
+/*********************                                                        */
+/*! \file bv_sat.cpp
+ ** \verbatim
+ ** Original author: lianah
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 prototype.
+ ** Copyright (c) 2009, 2010, 2011  The Analysis of Computer Systems Group (ACSys)
+ ** Courant Institute of Mathematical Sciences
+ ** New York University
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.\endverbatim
+ **
+ ** \brief [[ Add one-line brief description here ]]
+ **
+ ** [[ Add lengthier description here ]]
+ ** 
+ **/
+
+#include "bv_sat.h"
+#include "theory_bv_utils.h"
+#include "theory/rewriter.h"
+#include "prop/cnf_stream.h"
+#include "prop/sat_module.h"
+
+using namespace std;
+
+using namespace CVC4::theory::bv::utils;
+using namespace CVC4::context; 
+using namespace CVC4::prop;
+
+namespace CVC4 {
+namespace theory {
+namespace bv{
+
+
+std::string toString(Bits&  bits) {
+  ostringstream os; 
+  for (int i = bits.size() - 1; i >= 0; --i) {
+    TNode bit = bits[i];
+    if (bit.getKind() == kind::CONST_BOOLEAN) {
+      os << (bit.getConst<bool>() ? "1" : "0");
+    } else {
+      os << bit<< " ";   
+    }
+  }
+  os <<"\n";
+  
+  return os.str(); 
+}
+/////// Bitblaster 
+
+Bitblaster::Bitblaster(context::Context* c) :
+    d_termCache(),
+    d_bitblastedAtoms(),
+    d_assertedAtoms(c),
+    d_statistics()
+  {
+    d_satSolver = prop::SatSolverFactory::createMinisat();
+    d_cnfStream = new TseitinCnfStream(d_satSolver, new NullRegistrar());
+
+    // initializing the bit-blasting strategies
+    initAtomBBStrategies(); 
+    initTermBBStrategies(); 
+  }
+
+
+/** 
+ * Bitblasts the atom, assigns it a marker literal, adding it to the SAT solver
+ * NOTE: duplicate clauses are not detected because of marker literal
+ * @param node the atom to be bitblasted
+ * 
+ */
+void Bitblaster::bbAtom(TNode node) {
+  if (hasBBAtom(node)) {
+    return; 
+  }
+
+  // the bitblasted definition of the atom
+  Node atom_bb = d_atomBBStrategies[node.getKind()](node, this);
+  // asserting that the atom is true iff the definition holds
+  Node atom_definition = mkNode(kind::IFF, node, atom_bb);
+  // do boolean simplifications if possible
+  Node rewritten = Rewriter::rewrite(atom_definition);
+  d_cnfStream->convertAndAssert(rewritten, true, false);
+  d_bitblastedAtoms.insert(node); 
+}
+
+
+void Bitblaster::bbTerm(TNode node, Bits& bits) {
+  if (hasBBTerm(node)) {
+    getBBTerm(node, bits);
+    return;
+  }
+
+  d_termBBStrategies[node.getKind()] (node, bits,this);
+  
+  Assert (bits.size() == utils::getSize(node)); 
+  cacheTermDef(node, bits); 
+}
+
+/// Public methods
+
+/** 
+ * Called from preregistration bitblasts the node
+ * 
+ * @param node 
+ * 
+ * @return 
+ */
+void Bitblaster::bitblast(TNode node) {
+  TimerStat::CodeTimer codeTimer(d_statistics.d_bitblastTimer);
+
+  /// strip the not
+  if (node.getKind() == kind::NOT) {
+    node = node[0];
+  }
+  
+  if (node.getKind() == kind::EQUAL ||
+      node.getKind() == kind::BITVECTOR_ULT ||
+      node.getKind() == kind::BITVECTOR_SLT ||
+      node.getKind() == kind::BITVECTOR_ULE || 
+      node.getKind() == kind::BITVECTOR_SLE )
+    {
+      bbAtom(node); 
+    }
+  else if (node.getKind() == kind::BITVECTOR_UGT ||
+           node.getKind() == kind::BITVECTOR_UGE ||
+           node.getKind() == kind::BITVECTOR_SGT ||
+           node.getKind() == kind::BITVECTOR_SGE )
+    {
+      Unhandled(node.getKind()); 
+    }
+  else
+    {
+      Bits bits;
+      bbTerm(node, bits); 
+    }
+}
+
+/** 
+ * Asserts the clauses corresponding to the atom to the Sat Solver
+ * by turning on the marker literal (i.e. setting it to false)
+ * @param node the atom to be aserted
+ * 
+ */
+ 
+void Bitblaster::assertToSat(TNode lit) {
+  // strip the not
+  TNode atom; 
+  if (lit.getKind() == kind::NOT) {
+    atom = lit[0]; 
+  } else {
+    atom = lit; 
+  }
+  
+  Assert (hasBBAtom(atom)); 
+  SatLiteral markerLit = d_cnfStream->getLiteral(atom);
+
+  if(lit.getKind() == kind::NOT) {
+    markerLit = ~markerLit;
+  }
+  
+  Debug("bitvector-bb") << "TheoryBV::Bitblaster::assertToSat asserting node: " << atom <<"\n";
+  Debug("bitvector-bb") << "TheoryBV::Bitblaster::assertToSat with literal:   " << markerLit << "\n";  
+
+  d_assertedAtoms.push_back(markerLit);
+}
+
+/** 
+ * Calls the solve method for the Sat Solver. 
+ * passing it the marker literals to be asserted
+ * 
+ * @return true for sat, and false for unsat
+ */
+ 
+bool Bitblaster::solve() {
+  return SatValTrue == d_satSolver->solve(d_assertedAtoms); 
+}
+
+void Bitblaster::getConflict(std::vector<TNode>& conflict) {
+  SatClause conflictClause;
+  d_satSolver->getUnsatCore(conflictClause);
+  
+  for (unsigned i = 0; i < conflictClause.size(); i++) {
+    SatLiteral lit = conflictClause[i]; 
+    TNode atom = d_cnfStream->getNode(lit);
+    Node  not_atom; 
+    if (atom.getKind() == kind::NOT) {
+      not_atom = atom[0];
+    } else {
+      not_atom = NodeManager::currentNM()->mkNode(kind::NOT, atom); 
+    }
+    conflict.push_back(not_atom); 
+  }
+}
+
+
+/// Helper methods
+
+
+void Bitblaster::initAtomBBStrategies() {
+  for (int i = 0 ; i < kind::LAST_KIND; ++i ) {
+    d_atomBBStrategies[i] = UndefinedAtomBBStrategy; 
+  }
+  
+  /// setting default bb strategies for atoms
+  d_atomBBStrategies [ kind::EQUAL ]           = DefaultEqBB;
+  d_atomBBStrategies [ kind::BITVECTOR_ULT ]   = DefaultUltBB;
+  d_atomBBStrategies [ kind::BITVECTOR_ULE ]   = DefaultUleBB;
+  d_atomBBStrategies [ kind::BITVECTOR_UGT ]   = DefaultUgtBB;
+  d_atomBBStrategies [ kind::BITVECTOR_UGE ]   = DefaultUgeBB;
+  d_atomBBStrategies [ kind::BITVECTOR_SLT ]   = DefaultSltBB;
+  d_atomBBStrategies [ kind::BITVECTOR_SLE ]   = DefaultSleBB;
+  d_atomBBStrategies [ kind::BITVECTOR_SGT ]   = DefaultSgtBB;
+  d_atomBBStrategies [ kind::BITVECTOR_SGE ]   = DefaultSgeBB;
+  
+}
+
+void Bitblaster::initTermBBStrategies() {
+  for (int i = 0 ; i < kind::LAST_KIND; ++i ) {
+    d_termBBStrategies[i] = UndefinedTermBBStrategy; 
+  }
+  
+  /// setting default bb strategies for terms:
+  d_termBBStrategies [ kind::VARIABLE ]               = DefaultVarBB;
+  d_termBBStrategies [ kind::CONST_BITVECTOR ]        = DefaultConstBB;
+  d_termBBStrategies [ kind::BITVECTOR_NOT ]          = DefaultNotBB;
+  d_termBBStrategies [ kind::BITVECTOR_CONCAT ]       = DefaultConcatBB;
+  d_termBBStrategies [ kind::BITVECTOR_AND ]          = DefaultAndBB;
+  d_termBBStrategies [ kind::BITVECTOR_OR ]           = DefaultOrBB;
+  d_termBBStrategies [ kind::BITVECTOR_XOR ]          = DefaultXorBB;
+  d_termBBStrategies [ kind::BITVECTOR_XNOR ]         = DefaultXnorBB;
+  d_termBBStrategies [ kind::BITVECTOR_NAND ]         = DefaultNandBB ;
+  d_termBBStrategies [ kind::BITVECTOR_NOR ]          = DefaultNorBB;
+  d_termBBStrategies [ kind::BITVECTOR_COMP ]         = DefaultCompBB ;
+  d_termBBStrategies [ kind::BITVECTOR_MULT ]         = DefaultMultBB;
+  d_termBBStrategies [ kind::BITVECTOR_PLUS ]         = DefaultPlusBB;
+  d_termBBStrategies [ kind::BITVECTOR_SUB ]          = DefaultSubBB;
+  d_termBBStrategies [ kind::BITVECTOR_NEG ]          = DefaultNegBB;
+  d_termBBStrategies [ kind::BITVECTOR_UDIV ]         = DefaultUdivBB;
+  d_termBBStrategies [ kind::BITVECTOR_UREM ]         = DefaultUremBB;
+  d_termBBStrategies [ kind::BITVECTOR_SDIV ]         = DefaultSdivBB;
+  d_termBBStrategies [ kind::BITVECTOR_SREM ]         = DefaultSremBB;
+  d_termBBStrategies [ kind::BITVECTOR_SMOD ]         = DefaultSmodBB;
+  d_termBBStrategies [ kind::BITVECTOR_SHL ]          = DefaultShlBB;
+  d_termBBStrategies [ kind::BITVECTOR_LSHR ]         = DefaultLshrBB;
+  d_termBBStrategies [ kind::BITVECTOR_ASHR ]         = DefaultAshrBB;
+  d_termBBStrategies [ kind::BITVECTOR_EXTRACT ]      = DefaultExtractBB;
+  d_termBBStrategies [ kind::BITVECTOR_REPEAT ]       = DefaultRepeatBB;
+  d_termBBStrategies [ kind::BITVECTOR_ZERO_EXTEND ]  = DefaultZeroExtendBB;
+  d_termBBStrategies [ kind::BITVECTOR_SIGN_EXTEND ]  = DefaultSignExtendBB;
+  d_termBBStrategies [ kind::BITVECTOR_ROTATE_RIGHT ] = DefaultRotateRightBB;
+  d_termBBStrategies [ kind::BITVECTOR_ROTATE_LEFT ]  = DefaultRotateLeftBB;
+
+}
+ 
+bool Bitblaster::hasBBAtom(TNode atom) {
+  return d_bitblastedAtoms.find(atom) != d_bitblastedAtoms.end();
+}
+
+void Bitblaster::cacheTermDef(TNode term, Bits def) {
+  Assert (d_termCache.find(term) == d_termCache.end());
+  d_termCache[term] = def; 
+}
+
+bool Bitblaster::hasBBTerm(TNode node) {
+  return d_termCache.find(node) != d_termCache.end(); 
+}
+
+void Bitblaster::getBBTerm(TNode node, Bits& bits) {
+  
+  Assert (hasBBTerm(node)); 
+  // copy?
+  bits = d_termCache[node]; 
+}
+
+Bitblaster::Statistics::Statistics() :
+  d_numTermClauses("theory::bv::NumberOfTermSatClauses", 0),
+  d_numAtomClauses("theory::bv::NumberOfAtomSatClauses", 0), 
+  d_bitblastTimer("theory::bv::BitblastTimer")
+{
+  StatisticsRegistry::registerStat(&d_numTermClauses);
+  StatisticsRegistry::registerStat(&d_numAtomClauses);
+  StatisticsRegistry::registerStat(&d_bitblastTimer);
+}
+
+
+Bitblaster::Statistics::~Statistics() {
+  StatisticsRegistry::unregisterStat(&d_numTermClauses);
+  StatisticsRegistry::unregisterStat(&d_numAtomClauses);
+  StatisticsRegistry::unregisterStat(&d_bitblastTimer);
+}
+
+
+
+
+} /*bv namespace */
+} /* theory namespace */
+} /* CVC4 namespace*/
diff --git a/src/theory/bv/bv_sat.h b/src/theory/bv/bv_sat.h
new file mode 100644
index 000000000..9844cd982
--- /dev/null
+++ b/src/theory/bv/bv_sat.h
@@ -0,0 +1,144 @@
+/*********************                                                        */
+/*! \file bv_sat.h
+ ** \verbatim
+ ** Original author: lianah
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 prototype.
+ ** Copyright (c) 2009, 2010, 2011  The Analysis of Computer Systems Group (ACSys)
+ ** Courant Institute of Mathematical Sciences
+ ** New York University
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.\endverbatim
+ **
+ ** \brief Wrapper around the SAT solver used for bitblasting
+ **
+ ** Wrapper around the SAT solver used for bitblasting.
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef __CVC4__BV__SAT_H
+#define __CVC4__BV__SAT_H
+
+
+#include "expr/node.h"
+#include <vector>
+#include <list>
+#include <iostream>
+#include <math.h>
+#include <ext/hash_map>
+
+#include "context/cdo.h"
+#include "context/cdset.h"
+#include "context/cdlist.h"
+
+#include "theory_bv_utils.h"
+#include "util/stats.h"
+#include "bitblast_strategies.h"
+
+#include "prop/sat_module.h"
+
+namespace CVC4 {
+
+// forward declarations
+namespace prop {
+class CnfStream;
+class BVSatSolverInterface;
+}
+
+
+namespace theory {
+namespace bv {
+
+
+std::string toString (Bits& bits); 
+
+/** 
+ * The Bitblaster that manages the mapping between Nodes 
+ * and their bitwise definition 
+ * 
+ */
+
+typedef std::vector<Node> Bits; 
+
+class Bitblaster {
+  
+  typedef __gnu_cxx::hash_map <Node, Bits, TNodeHashFunction >              TermDefMap;
+  typedef __gnu_cxx::hash_set<TNode, TNodeHashFunction>                      AtomSet; 
+  
+  typedef void   (*TermBBStrategy) (TNode, Bits&, Bitblaster*); 
+  typedef Node   (*AtomBBStrategy) (TNode, Bitblaster*); 
+
+  // sat solver used for bitblasting and associated CnfStream
+  prop::BVSatSolverInterface*        d_satSolver; 
+  prop::CnfStream*                   d_cnfStream;
+
+  // caches and mappings
+  TermDefMap                   d_termCache;
+  AtomSet                      d_bitblastedAtoms;
+  
+  context::CDList<prop::SatLiteral>  d_assertedAtoms; /**< context dependent list storing the atoms
+                                              currently asserted by the DPLL SAT solver. */
+
+  /// helper methods
+  bool          hasBBAtom(TNode node);    
+  bool          hasBBTerm(TNode node); 
+  void          getBBTerm(TNode node, Bits& bits);
+
+
+
+
+  /// function tables for the various bitblasting strategies indexed by node kind
+  TermBBStrategy d_termBBStrategies[kind::LAST_KIND];
+  AtomBBStrategy d_atomBBStrategies[kind::LAST_KIND]; 
+
+  // helper methods to initialize function tables
+  void initAtomBBStrategies();
+  void initTermBBStrategies(); 
+
+  
+  void bbAtom(TNode node);
+  // division is bitblasted in terms of constraints
+  // so it needs to use private bitblaster interface
+  void bbUdiv(TNode node, Bits& bits);
+  void bbUrem(TNode node, Bits& bits); 
+public:
+  void cacheTermDef(TNode node, Bits def); // public so we can cache remainder for division
+  void bbTerm(TNode node, Bits&  bits);
+  
+public:
+  Bitblaster(context::Context* c); 
+  ~Bitblaster() {
+    delete d_cnfStream;
+    delete d_satSolver; 
+  }
+  
+  void assertToSat(TNode node);
+  bool solve();
+  void bitblast(TNode node);
+  void getConflict(std::vector<TNode>& conflict); 
+
+private:
+
+  
+  class Statistics {
+  public:
+    IntStat  d_numTermClauses, d_numAtomClauses;
+    TimerStat d_bitblastTimer;
+    Statistics();
+    ~Statistics(); 
+  }; 
+  
+  Statistics d_statistics;
+};
+
+
+
+} /* bv namespace */ 
+
+} /* theory namespace */
+
+} /* CVC4 namespace */
+
+#endif /* __CVC4__BV__SAT_H */
diff --git a/src/theory/bv/bv_solver_types.cpp b/src/theory/bv/bv_solver_types.cpp
new file mode 100644
index 000000000..2589e5712
--- /dev/null
+++ b/src/theory/bv/bv_solver_types.cpp
@@ -0,0 +1,78 @@
+/*********************                                                        */
+/*! \file bv_sat.cpp
+ ** \verbatim
+ ** Original author: lianah
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 prototype.
+ ** Copyright (c) 2009, 2010, 2011  The Analysis of Computer Systems Group (ACSys)
+ ** Courant Institute of Mathematical Sciences
+ ** New York University
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.\endverbatim
+ **
+ ** \brief [[ Add one-line brief description here ]]
+ **
+ ** [[ Add lengthier description here ]]
+ ** 
+ **/
+
+#include "bv_solver_types.h"
+
+namespace CVC4 {
+namespace theory {
+namespace bv {
+
+#ifdef BV_MINISAT 
+using namespace BVMinisat; 
+SatLit neg(const SatLit& lit) {
+  return ~lit; 
+}
+
+SatLit mkLit(SatVar var) {
+  return BVMinisat::mkLit(var, false); 
+}
+
+SatVar mkVar(SatLit lit) {
+  return BVMinisat::var(lit); 
+}
+bool   polarity(SatLit lit) {
+  return !(BVMinisat::sign(lit)); 
+} 
+
+
+std::string toStringLit(SatLit lit) {
+  std::ostringstream os;
+  os << (polarity(lit) ? "" : "-") << var(lit) + 1;
+  return os.str(); 
+}
+#endif
+
+#ifdef BV_PICOSAT
+
+SatLit mkLit(SatVar var) {
+  return var;
+}
+SatVar mkVar(SatLit lit) {
+  return (lit > 0 ? lit : -lit); 
+}
+bool   polarity(SatLit lit) {
+  return (lit > 0); 
+}
+
+SatLit neg(const SatLit& lit) {
+   return -lit; 
+}
+
+std::string toStringLit(SatLit lit) {
+  std::ostringstream os;
+  os << (lit < 0 ? "-" : "") << lit;
+  return os.str(); 
+}
+
+
+#endif  
+
+}
+}
+}
diff --git a/src/theory/bv/bv_solver_types.h b/src/theory/bv/bv_solver_types.h
new file mode 100644
index 000000000..fb99ae4c6
--- /dev/null
+++ b/src/theory/bv/bv_solver_types.h
@@ -0,0 +1,185 @@
+//*********************                                                        */
+/*! \file bv_solver_types.h
+ ** \verbatim
+ ** Original author: lianah
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 prototype.
+ ** Copyright (c) 2009, 2010, 2011  The Analysis of Computer Systems Group (ACSys)
+ ** Courant Institute of Mathematical Sciences
+ ** New York University
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.\endverbatim
+ **
+ ** \brief Definitions of the SatSolver literal and clause types 
+ **
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef __CVC4__BV__SOLVER__TYPES_H 
+#define __CVC4__BV__SOLVER__TYPES_H 
+
+#define BV_MINISAT
+//#define BV_PICOSAT
+
+#ifdef BV_MINISAT  /* BV_MINISAT if we are using the minisat solver for the theory of bitvectors*/
+#include "theory/bv/bvminisat/core/Solver.h"
+#include "theory/bv/bvminisat/core/SolverTypes.h"
+#include "theory/bv/bvminisat/simp/SimpSolver.h"
+#endif   /* BV_MINISAT */
+
+#ifdef BV_PICOSAT  /* BV_PICOSAT */
+#include "picosat/picosat.h"
+#endif  /* BV_PICOSAT */
+
+#include "expr/node.h"
+#include <vector>
+#include <list>
+#include <iostream>
+#include <math.h>
+#include <ext/hash_map>
+#include "context/cdlist.h"
+#include "util/stats.h"
+
+
+namespace CVC4 {
+namespace theory {
+namespace bv {
+
+#endif /* BV_MINISAT */
+
+
+
+// #ifdef BV_PICOSAT /* BV_PICOSAT */
+// /** 
+//  * PICOSAT type-definitions
+//  * 
+//  * 
+//  */
+
+// typedef int SatVar; 
+// typedef int SatLit; 
+
+// std::string toStringLit(SatLit lit); 
+
+
+// SatLit neg(const SatLit& lit); 
+
+// struct SatLitHash {
+//   static size_t hash (const SatLit& lit) {
+//     return (size_t) lit;
+//   }
+  
+// };
+
+// struct SatLitHashFunction {
+//   size_t operator()(SatLit lit) const {
+//     return (size_t) lit; 
+//   }
+// };
+
+// struct SatLitLess{
+//   static bool compare(const SatLit& x, const SatLit& y)
+//   {
+//     return x < y;
+//   }
+// };
+
+// #endif /* BV_PICOSAT */
+
+// #ifdef BV_PICOSAT  /* BV_PICOSAT */
+
+// /** 
+//  * Some helper functions that should be defined for each SAT solver supported
+//  * 
+//  * 
+//  * @return 
+//  */
+
+// SatLit mkLit(SatVar var);
+// SatVar mkVar(SatLit lit);
+// bool   polarity(SatLit lit); 
+
+
+// /** 
+//  * Wrapper to create the impression of a SatSolver class for Picosat
+//  * which is written in C
+//  */
+
+// class SatSolver: public SatSolverInterface {
+//   int d_varCount;
+//   bool d_started;
+// public:
+//   SatSolver() :
+//     d_varCount(0),
+//     d_started(false)
+//   {
+//     picosat_init(); /// call constructor
+//     picosat_enable_trace_generation(); // required for unsat cores
+//   }
+  
+//   ~SatSolver() {
+//     picosat_reset(); 
+//   }
+
+//   void   addClause(const SatClause* cl) {
+//     Assert (cl);
+//     const SatClause& clause = *cl; 
+//     for (unsigned i = 0; i < clause.size(); ++i ) {
+//       picosat_add(clause[i]); 
+//     }
+//     picosat_add(0); // ends clause
+//   }
+  
+//   bool   solve () {
+//     if(d_started) {
+//       picosat_remove_learned(100);
+//     }
+//     int res = picosat_sat(-1); // no decision limit
+//     // 0 UNKNOWN, 10 SATISFIABLE and 20 UNSATISFIABLE
+//     d_started = true; 
+//     Assert (res == 10 || res == 20); 
+//     return res == 10; 
+//   }
+  
+//   bool   solve(const context::CDList<SatLit> & assumps) {
+//     context::CDList<SatLit>::const_iterator it = assumps.begin();
+//     for (; it!= assumps.end(); ++it) {
+//       picosat_assume(*it); 
+//     }
+//     return solve (); 
+//   }
+  
+//   SatVar newVar() { return ++d_varCount; }
+
+//   void   setUnremovable(SatLit lit) {}; 
+
+//   SatClause* getUnsatCore() {
+//     const int* failedAssumption = picosat_failed_assumptions();
+//     Assert(failedAssumption);
+
+//     SatClause* unsatCore = new SatClause();
+//     while (*failedAssumption != 0) {
+//       SatLit lit = *failedAssumption;
+//       unsatCore->addLiteral(neg(lit));
+//       ++failedAssumption; 
+//     }
+//     unsatCore->sort(); 
+//     return unsatCore; 
+//   }
+// }; 
+
+
+// #endif  /* BV_PICOSAT */
+
+
+
+
+} /* bv namespace */ 
+
+} /* theory namespace */
+
+} /* CVC4 namespace */
+
+#endif /* __CVC4__BV__SOLVER__TYPES_H */
diff --git a/src/theory/bv/equality_engine.cpp b/src/theory/bv/equality_engine.cpp
deleted file mode 100644
index a4d2e6329..000000000
--- a/src/theory/bv/equality_engine.cpp
+++ /dev/null
@@ -1,27 +0,0 @@
-/*********************                                                        */
-/*! \file equality_engine.cpp
- ** \verbatim
- ** Original author: dejan
- ** Major contributors: mdeters
- ** Minor contributors (to current version): none
- ** This file is part of the CVC4 prototype.
- ** Copyright (c) 2009, 2010, 2011  The Analysis of Computer Systems Group (ACSys)
- ** Courant Institute of Mathematical Sciences
- ** New York University
- ** See the file COPYING in the top-level source directory for licensing
- ** information.\endverbatim
- **
- ** \brief [[ Add one-line brief description here ]]
- **
- ** [[ Add lengthier description here ]]
- ** \todo document this file
- **/
-
-#include "theory/bv/equality_engine.h"
-
-using namespace CVC4::theory::bv;
-
-const size_t BitSizeTraits::id_null = (1u << BitSizeTraits::id_bits) - 1;
-const size_t BitSizeTraits::trigger_id_null = (1u << BitSizeTraits::trigger_id_bits) - 1;
-
-
diff --git a/src/theory/bv/equality_engine.h b/src/theory/bv/equality_engine.h
deleted file mode 100644
index 558fd2b7b..000000000
--- a/src/theory/bv/equality_engine.h
+++ /dev/null
@@ -1,844 +0,0 @@
-/*********************                                                        */
-/*! \file equality_engine.h
- ** \verbatim
- ** Original author: dejan
- ** Major contributors: none
- ** Minor contributors (to current version): mdeters
- ** This file is part of the CVC4 prototype.
- ** Copyright (c) 2009, 2010, 2011  The Analysis of Computer Systems Group (ACSys)
- ** Courant Institute of Mathematical Sciences
- ** New York University
- ** See the file COPYING in the top-level source directory for licensing
- ** information.\endverbatim
- **
- ** \brief [[ Add one-line brief description here ]]
- **
- ** [[ Add lengthier description here ]]
- ** \todo document this file
- **/
-
-#include "cvc4_private.h"
-
-#pragma once
-
-#include <vector>
-#include <ext/hash_map>
-#include <sstream>
-
-#include "expr/node.h"
-#include "context/cdo.h"
-#include "util/output.h"
-#include "util/stats.h"
-#include "theory/rewriter.h"
-#include "theory/bv/theory_bv_utils.h"
-
-namespace CVC4 {
-namespace theory {
-namespace bv {
-
-struct BitSizeTraits {
-  /** The null id */
-  static const size_t id_null; // Defined in the cpp file (GCC bug)
-  /** The null trigger id */
-  static const size_t trigger_id_null;
-
-  /** Number of bits we use for the id */
-  static const size_t id_bits   = 24;
-  /** Number of bits we use for the size the equivalence class */
-  static const size_t size_bits = 16;
-  /** Number of bits we use for the trigger id */
-  static const size_t trigger_id_bits = 24;
-};
-
-class EqualityNode {
-
-public:
-
-  /** The size of this equivalence class (if it's a representative) */
-  size_t d_size   : BitSizeTraits::size_bits;
-
-  /** The id (in the eq-manager) of the representative equality node */
-  size_t d_findId : BitSizeTraits::id_bits;
-
-  /** The next equality node in this class */
-  size_t d_nextId : BitSizeTraits::id_bits;
-
-public:
-
-  /**
-   * Creates a new node, which is in a list of it's own.
-   */
-  EqualityNode(size_t nodeId = BitSizeTraits::id_null)
-  : d_size(1), d_findId(nodeId), d_nextId(nodeId) {}
-
-  /** Initialize the equality node */
-  inline void init(size_t nodeId) {
-    d_size = 1;
-    d_findId = d_nextId = nodeId;
-  }
-
-  /**
-   * Returns the next node in the class circular list.
-   */
-  inline size_t getNext() const {
-    return d_nextId;
-  }
-
-  /**
-   * Returns the size of this equivalence class (only valid if this is the representative).
-   */
-  inline size_t getSize() const {
-    return d_size;
-  }
-
-  /**
-   * Merges the two lists. If add size is true the size of this node is increased by the size of
-   * the other node, otherwise the size is decreased by the size of the other node.
-   */
-  template<bool addSize>
-  inline void merge(EqualityNode& other) {
-    size_t tmp = d_nextId; d_nextId = other.d_nextId; other.d_nextId = tmp;
-    if (addSize) {
-      d_size += other.d_size;
-    } else {
-      d_size -= other.d_size;
-    }
-  }
-
-  /**
-   * Returns the class representative.
-   */
-  inline size_t getFind() const { return d_findId; }
-
-  /**
-   * Set the class representative.
-   */
-  inline void setFind(size_t findId) { d_findId = findId; }
-};
-
-template <typename OwnerClass, typename NotifyClass, typename UnionFindPreferences>
-class EqualityEngine {
-
-public:
-
-  /** Statistics about the equality engine instance */
-  struct Statistics {
-    /** Total number of merges */
-    IntStat mergesCount;
-    /** Number of terms managed by the system */
-    IntStat termsCount;
-    /** Number of function terms managed by the system */
-    IntStat functionTermsCount;
-    /** Number of times we performed a backtrack */
-    IntStat backtracksCount;
-
-    Statistics(std::string name)
-    : mergesCount(name + "::mergesCount", 0),
-      termsCount(name + "::termsCount", 0),
-      functionTermsCount(name + "functionTermsCoutn", 0),
-      backtracksCount(name + "::backtracksCount", 0)
-    {
-      StatisticsRegistry::registerStat(&mergesCount);
-      StatisticsRegistry::registerStat(&termsCount);
-      StatisticsRegistry::registerStat(&functionTermsCount);
-      StatisticsRegistry::registerStat(&backtracksCount);
-    }
-
-    ~Statistics() {
-      StatisticsRegistry::unregisterStat(&mergesCount);
-      StatisticsRegistry::unregisterStat(&termsCount);
-      StatisticsRegistry::unregisterStat(&functionTermsCount);
-      StatisticsRegistry::unregisterStat(&backtracksCount);
-    }
-  };
-
-private:
-
-  /** The class to notify when a representative changes for a term */
-  NotifyClass d_notify;
-
-  /** Map from nodes to their ids */
-  __gnu_cxx::hash_map<TNode, size_t, TNodeHashFunction> d_nodeIds;
-
-  /** Map from ids to the nodes */
-  std::vector<Node> d_nodes;
-
-  /** Map from ids to the equality nodes */
-  std::vector<EqualityNode> d_equalityNodes;
-
-  /** Number of asserted equalities we have so far */
-  context::CDO<size_t> d_assertedEqualitiesCount;
-
-  /**
-   * We keep a list of asserted equalities. Not among original terms, but
-   * among the class representatives.
-   */
-  struct Equality {
-    /** Left hand side of the equality */
-    size_t lhs : BitSizeTraits::id_bits;
-    /** Right hand side of the equality */
-    size_t rhs : BitSizeTraits::id_bits;
-    /** Equality constructor */
-    Equality(size_t lhs = BitSizeTraits::id_null, size_t rhs = BitSizeTraits::id_null)
-    : lhs(lhs), rhs(rhs) {}
-  };
-
-  /** The ids of the classes we have merged */
-  std::vector<Equality> d_assertedEqualities;
-
-  /** The reasons for the equalities */
-
-  /**
-   * An edge in the equality graph. This graph is an undirected graph (both edges added)
-   * containing the actual asserted equalities.
-   */
-  class EqualityEdge {
-
-    // The id of the RHS of this equality
-    size_t d_nodeId : BitSizeTraits::id_bits;
-    // The next edge
-    size_t d_nextId : BitSizeTraits::id_bits;
-
-  public:
-
-    EqualityEdge(size_t nodeId = BitSizeTraits::id_null, size_t nextId = BitSizeTraits::id_null)
-    : d_nodeId(nodeId), d_nextId(nextId) {}
-
-    /** Returns the id of the next edge */
-    inline size_t getNext() const { return d_nextId; }
-
-    /** Returns the id of the target edge node */
-    inline size_t getNodeId() const { return d_nodeId; }
-  };
-
-  /**
-   * All the equality edges (twice as many as the number of asserted equalities. If an equality
-   * t1 = t2 is asserted, the edges added are -> t2, -> t1 (in this order). Hance, having the index
-   * of one of the edges you can reconstruct the original equality.
-   */
-  std::vector<EqualityEdge> d_equalityEdges;
-
-  /**
-   * Returns the string representation of the edges.
-   */
-  std::string edgesToString(size_t edgeId) const;
-
-  /**
-   * Reasons for equalities.
-   */
-  std::vector<Node> d_equalityReasons;
-
-  /**
-   * Map from a node to it's first edge in the equality graph. Edges are added to the front of the
-   * list which makes the insertion/backtracking easy.
-   */
-  std::vector<size_t> d_equalityGraph;
-
-  /** Add an edge to the equality graph */
-  inline void addGraphEdge(size_t t1, size_t t2, Node reason);
-
-  /** Returns the equality node of the given node */
-  inline EqualityNode& getEqualityNode(TNode node);
-
-  /** Returns the equality node of the given node */
-  inline EqualityNode& getEqualityNode(size_t nodeId);
-
-  /** Returns the id of the node */
-  inline size_t getNodeId(TNode node) const;
-
-  /** Merge the class2 into class1 */
-  void merge(EqualityNode& class1, EqualityNode& class2, std::vector<size_t>& triggers);
-
-  /** Undo the mereg of class2 into class1 */
-  void undoMerge(EqualityNode& class1, EqualityNode& class2, size_t class2Id);
-
-  /** Backtrack the information if necessary */
-  void backtrack();
-
-  /**
-   * Data used in the BFS search through the equality graph.
-   */
-  struct BfsData {
-    // The current node
-    size_t nodeId : BitSizeTraits::id_bits;
-    // The index of the edge we traversed
-    size_t edgeId : BitSizeTraits::id_bits;
-    // Index in the queue of the previous node. Shouldn't be too much of them, at most the size
-    // of the biggest equivalence class
-    size_t previousIndex : BitSizeTraits::size_bits;
-
-    BfsData(size_t nodeId = BitSizeTraits::id_null, size_t edgeId = BitSizeTraits::id_null, size_t prev = 0)
-    : nodeId(nodeId), edgeId(edgeId), previousIndex(prev) {}
-  };
-
-  /**
-   * Trigger that will be updated
-   */
-  struct Trigger {
-    /** The current class id of the LHS of the trigger */
-    size_t classId : BitSizeTraits::id_bits;
-    /** Next trigger for class 1 */
-    size_t nextTrigger : BitSizeTraits::id_bits;
-
-    Trigger(size_t classId, size_t nextTrigger)
-    : classId(classId), nextTrigger(nextTrigger) {}
-  };
-
-  /**
-   * Vector of triggers (persistent and not-backtrackable). Triggers come in pairs for an
-   * equality trigger (t1, t2): one at position 2k for t1, and one at position 2k + 1 for t2. When
-   * updating triggers we always know where the other one is (^1).
-   */
-  std::vector<Trigger> d_equalityTriggers;
-
-  /**
-   * Trigger lists per node. The begin id changes as we merge, but the end always points to
-   * the actual end of the triggers for this node.
-   */
-  std::vector<size_t> d_nodeTriggers;
-
-  /**
-   * Adds the trigger with triggerId to the beginning of the trigger list of the node with id nodeId.
-   */
-  inline void addTriggerToList(size_t nodeId, size_t triggerId);
-
-  /** Statistics */
-  Statistics d_stats;
-
-public:
-
-  /**
-   * Initialize the equality engine, given the owning class. This will initialize the notifier with
-   * the owner information.
-   */
-  EqualityEngine(OwnerClass& owner, context::Context* context, std::string name)
-  : d_notify(owner), d_assertedEqualitiesCount(context, 0), d_stats(name) {
-    BVDebug("equality") << "EqualityEdge::EqualityEdge(): id_null = " << BitSizeTraits::id_null <<
-        ", trigger_id_null = " << BitSizeTraits::trigger_id_null << std::endl;
-  }
-
-  /**
-   * Adds a term to the term database. Returns the internal id of the term.
-   */
-  size_t addTerm(TNode t);
-
-  /**
-   * Check whether the node is already in the database.
-   */
-  inline bool hasTerm(TNode t) const;
-
-  /**
-   * Adds an equality t1 = t2 to the database. Returns false if any of the triggers failed, or a
-   * conflict was introduced.
-   */
-  bool addEquality(TNode t1, TNode t2, Node reason);
-
-  /**
-   * Returns the representative of the term t.
-   */
-  inline TNode getRepresentative(TNode t) const;
-
-  /**
-   * Returns true if the two nodes are in the same class.
-   */
-  inline bool areEqual(TNode t1, TNode t2) const;
-
-  /**
-   * Get an explanation of the equality t1 = t2. Returns the asserted equalities that
-   * imply t1 = t2. Returns TNodes as the assertion equalities should be hashed somewhere
-   * else. TODO: mark the phantom equalities (skolems).
-   */
-  void getExplanation(TNode t1, TNode t2, std::vector<TNode>& equalities) const;
-
-  /**
-   * Adds a notify trigger for equality t1 = t2, i.e. when t1 = t2 the notify will be called with
-   * (t1, t2).
-   */
-  size_t addTrigger(TNode t1, TNode t2);
-
-  /**
-   * Normalizes a term by finding the representative. If the representative can be decomposed (using
-   * UnionFindPreferences) it will try and recursively find the representatives, and substitute.
-   * Assumptions used in normalization are retruned in the set.
-   */
-  Node normalize(TNode node, std::set<TNode>& assumptions);
-
-private:
-
-  /** Hash of normalizations to avioid cycles */
-  typedef __gnu_cxx::hash_map<TNode, Node, TNodeHashFunction> normalization_cache;
-  normalization_cache d_normalizationCache;
-
-  /**
-   * Same as above, but does cahcing to avoid loops.
-   */
-  Node normalizeWithCache(TNode node, std::set<TNode>& assumptions);
-
-};
-
-template <typename OwnerClass, typename NotifyClass, typename UnionFindPreferences>
-size_t EqualityEngine<OwnerClass, NotifyClass, UnionFindPreferences>::addTerm(TNode t) {
-
-  BVDebug("equality") << "EqualityEngine::addTerm(" << t << ")" << std::endl;
-
-  // If term already added, retrurn it's id
-  if (hasTerm(t)) return getNodeId(t);
-
-  ++ d_stats.termsCount;
-
-  // Register the new id of the term
-  size_t newId = d_nodes.size();
-  d_nodeIds[t] = newId;
-  // Add the node to it's position
-  d_nodes.push_back(t);
-  // Add the trigger list for this node
-  d_nodeTriggers.push_back(BitSizeTraits::trigger_id_null);
-  // Add it to the equality graph
-  d_equalityGraph.push_back(BitSizeTraits::id_null);
-  // Add the equality node to the nodes
-  if (d_equalityNodes.size() <= newId) {
-    d_equalityNodes.resize(newId + 100);
-  }
-  d_equalityNodes[newId].init(newId);
-  // Return the id of the term
-  return newId;
-}
-
-template <typename OwnerClass, typename NotifyClass, typename UnionFindPreferences>
-bool EqualityEngine<OwnerClass, NotifyClass, UnionFindPreferences>::hasTerm(TNode t) const {
-  return d_nodeIds.find(t) != d_nodeIds.end();
-}
-
-template <typename OwnerClass, typename NotifyClass, typename UnionFindPreferences>
-size_t EqualityEngine<OwnerClass, NotifyClass, UnionFindPreferences>::getNodeId(TNode node) const {
-  Assert(hasTerm(node), node.toString().c_str());
-  return (*d_nodeIds.find(node)).second;
-}
-
-template <typename OwnerClass, typename NotifyClass, typename UnionFindPreferences>
-EqualityNode& EqualityEngine<OwnerClass, NotifyClass, UnionFindPreferences>::getEqualityNode(TNode t) {
-  return getEqualityNode(getNodeId(t));
-}
-
-template <typename OwnerClass, typename NotifyClass, typename UnionFindPreferences>
-EqualityNode& EqualityEngine<OwnerClass, NotifyClass, UnionFindPreferences>::getEqualityNode(size_t nodeId) {
-  Assert(nodeId < d_equalityNodes.size());
-  return d_equalityNodes[nodeId];
-}
-
-template <typename OwnerClass, typename NotifyClass, typename UnionFindPreferences>
-bool EqualityEngine<OwnerClass, NotifyClass, UnionFindPreferences>::addEquality(TNode t1, TNode t2, Node reason) {
-
-  BVDebug("equality") << "EqualityEngine::addEquality(" << t1 << "," << t2 << ")" << std::endl;
-
-  // Backtrack if necessary
-  backtrack();
-
-  // Add the terms if they are not already in the database
-  size_t t1Id = getNodeId(t1);
-  size_t t2Id = getNodeId(t2);
-
-  // Get the representatives
-  size_t t1classId = getEqualityNode(t1Id).getFind();
-  size_t t2classId = getEqualityNode(t2Id).getFind();
-
-  // If already the same, we're done
-  if (t1classId == t2classId) return true;
-
-  // Check for constants
-  if (d_nodes[t1classId].getMetaKind() == kind::metakind::CONSTANT &&
-      d_nodes[t2classId].getMetaKind() == kind::metakind::CONSTANT) {
-    std::vector<TNode> reasons;
-    getExplanation(t1, d_nodes[t1classId], reasons);
-    getExplanation(t2, d_nodes[t2classId], reasons);
-    reasons.push_back(reason);
-    d_notify.conflict(utils::mkAnd(reasons));
-    return false;
-  }
-
-  // Get the nodes of the representatives
-  EqualityNode& node1 = getEqualityNode(t1classId);
-  EqualityNode& node2 = getEqualityNode(t2classId);
-
-  Assert(node1.getFind() == t1classId);
-  Assert(node2.getFind() == t2classId);
-
-  // Depending on the merge preference (such as size), merge them
-  std::vector<size_t> triggers;
-  if (UnionFindPreferences::mergePreference(d_nodes[t2classId], node2.getSize(), d_nodes[t1classId], node1.getSize())) {
-    BVDebug("equality") << "EqualityEngine::addEquality(" << t1 << "," << t2 << "): merging " << t1 << " into " << t2 << std::endl;
-    merge(node2, node1, triggers);
-    d_assertedEqualities.push_back(Equality(t2classId, t1classId));
-  } else {
-    BVDebug("equality") << "EqualityEngine::addEquality(" << t1 << "," << t2 << "): merging " << t2 << " into " << t1 << std::endl;
-    merge(node1, node2, triggers);
-    d_assertedEqualities.push_back(Equality(t1classId, t2classId));
-  }
-
-  // Add the actuall equality to the equality graph
-  addGraphEdge(t1Id, t2Id, reason);
-
-  // One more equality added
-  d_assertedEqualitiesCount = d_assertedEqualitiesCount + 1;
-
-  Assert(2*d_assertedEqualities.size() == d_equalityEdges.size());
-  Assert(d_assertedEqualities.size() == d_assertedEqualitiesCount);
-
-  // Notify the triggers
-  for (size_t i = 0, i_end = triggers.size(); i < i_end; ++ i) {
-    // Notify the trigger and exit if it fails
-    if (!d_notify(triggers[i])) return false;
-  }
-
-  return true;
-}
-
-template <typename OwnerClass, typename NotifyClass, typename UnionFindPreferences>
-TNode EqualityEngine<OwnerClass, NotifyClass, UnionFindPreferences>::getRepresentative(TNode t) const {
-
-  BVDebug("equality") << "EqualityEngine::getRepresentative(" << t << ")" << std::endl;
-
-  Assert(hasTerm(t));
-
-  // Both following commands are semantically const
-  const_cast<EqualityEngine*>(this)->backtrack();
-  size_t representativeId = const_cast<EqualityEngine*>(this)->getEqualityNode(t).getFind();
-
-  BVDebug("equality") << "EqualityEngine::getRepresentative(" << t << ") => " << d_nodes[representativeId] << std::endl;
-
-  return d_nodes[representativeId];
-}
-
-template <typename OwnerClass, typename NotifyClass, typename UnionFindPreferences>
-bool EqualityEngine<OwnerClass, NotifyClass, UnionFindPreferences>::areEqual(TNode t1, TNode t2) const {
-  BVDebug("equality") << "EqualityEngine::areEqual(" << t1 << "," << t2 << ")" << std::endl;
-
-  Assert(hasTerm(t1));
-  Assert(hasTerm(t2));
-
-  // Both following commands are semantically const
-  const_cast<EqualityEngine*>(this)->backtrack();
-  size_t rep1 = const_cast<EqualityEngine*>(this)->getEqualityNode(t1).getFind();
-  size_t rep2 = const_cast<EqualityEngine*>(this)->getEqualityNode(t2).getFind();
-
-  BVDebug("equality") << "EqualityEngine::areEqual(" << t1 << "," << t2 << ") => " << (rep1 == rep2 ? "true" : "false") << std::endl;
-
-  return rep1 == rep2;
-}
-
-template <typename OwnerClass, typename NotifyClass, typename UnionFindPreferences>
-void EqualityEngine<OwnerClass, NotifyClass, UnionFindPreferences>::merge(EqualityNode& class1, EqualityNode& class2, std::vector<size_t>& triggers) {
-
-  BVDebug("equality") << "EqualityEngine::merge(" << class1.getFind() << "," << class2.getFind() << ")" << std::endl;
-
-  Assert(triggers.empty());
-
-  ++ d_stats.mergesCount;
-
-  size_t class1Id = class1.getFind();
-  size_t class2Id = class2.getFind();
-
-  // Update class2 representative information
-  size_t currentId = class2Id;
-  do {
-    // Get the current node
-    EqualityNode& currentNode = getEqualityNode(currentId);
-
-    // Update it's find to class1 id
-    currentNode.setFind(class1Id);
-
-    // Go through the triggers and inform if necessary
-    size_t currentTrigger = d_nodeTriggers[currentId];
-    while (currentTrigger != BitSizeTraits::trigger_id_null) {
-      Trigger& trigger = d_equalityTriggers[currentTrigger];
-      Trigger& otherTrigger = d_equalityTriggers[currentTrigger ^ 1];
-
-      // If the two are not already in the same class
-      if (otherTrigger.classId != trigger.classId) {
-        trigger.classId = class1Id;
-        // If they became the same, call the trigger
-        if (otherTrigger.classId == class1Id) {
-          // Id of the real trigger is half the internal one
-          triggers.push_back(currentTrigger >> 1);
-        }
-      }
-
-      // Go to the next trigger
-      currentTrigger = trigger.nextTrigger;
-    }
-
-    // Move to the next node
-    currentId = currentNode.getNext();
-
-  } while (currentId != class2Id);
-
-  // Now merge the lists
-  class1.merge<true>(class2);
-}
-
-template <typename OwnerClass, typename NotifyClass, typename UnionFindPreferences>
-void EqualityEngine<OwnerClass, NotifyClass, UnionFindPreferences>::undoMerge(EqualityNode& class1, EqualityNode& class2, size_t class2Id) {
-
-  BVDebug("equality") << "EqualityEngine::undoMerge(" << class1.getFind() << "," << class2Id << ")" << std::endl;
-
-  // Now unmerge the lists (same as merge)
-  class1.merge<false>(class2);
-
-  // Update class2 representative information
-  size_t currentId = class2Id;
-  do {
-    // Get the current node
-    EqualityNode& currentNode = getEqualityNode(currentId);
-
-    // Update it's find to class1 id
-    currentNode.setFind(class2Id);
-
-    // Go through the trigger list (if any) and undo the class
-    size_t currentTrigger = d_nodeTriggers[currentId];
-    while (currentTrigger != BitSizeTraits::trigger_id_null) {
-      Trigger& trigger = d_equalityTriggers[currentTrigger];
-      trigger.classId = class2Id;
-      currentTrigger = trigger.nextTrigger;
-    }
-
-    // Move to the next node
-    currentId = currentNode.getNext();
-
-  } while (currentId != class2Id);
-
-}
-
-template <typename OwnerClass, typename NotifyClass, typename UnionFindPreferences>
-void EqualityEngine<OwnerClass, NotifyClass, UnionFindPreferences>::backtrack() {
-
-  // If we need to backtrack then do it
-  if (d_assertedEqualitiesCount < d_assertedEqualities.size()) {
-
-    ++ d_stats.backtracksCount;
-
-    BVDebug("equality") << "EqualityEngine::backtrack(): nodes" << std::endl;
-
-    for (int i = (int)d_assertedEqualities.size() - 1, i_end = (int)d_assertedEqualitiesCount; i >= i_end; --i) {
-      // Get the ids of the merged classes
-      Equality& eq = d_assertedEqualities[i];
-      // Undo the merge
-      undoMerge(d_equalityNodes[eq.lhs], d_equalityNodes[eq.rhs], eq.rhs);
-    }
-
-    d_assertedEqualities.resize(d_assertedEqualitiesCount);
-
-    BVDebug("equality") << "EqualityEngine::backtrack(): edges" << std::endl;
-
-    for (int i = (int)d_equalityEdges.size() - 2, i_end = (int)(2*d_assertedEqualitiesCount); i >= i_end; i -= 2) {
-      EqualityEdge& edge1 = d_equalityEdges[i];
-      EqualityEdge& edge2 = d_equalityEdges[i | 1];
-      d_equalityGraph[edge2.getNodeId()] = edge1.getNext();
-      d_equalityGraph[edge1.getNodeId()] = edge2.getNext();
-    }
-
-    d_equalityEdges.resize(2 * d_assertedEqualitiesCount);
-    d_equalityReasons.resize(d_assertedEqualitiesCount);
-  }
-
-}
-
-template <typename OwnerClass, typename NotifyClass, typename UnionFindPreferences>
-void EqualityEngine<OwnerClass, NotifyClass, UnionFindPreferences>::addGraphEdge(size_t t1, size_t t2, Node reason) {
-  BVDebug("equality") << "EqualityEngine::addGraphEdge(" << d_nodes[t1] << "," << d_nodes[t2] << ")" << std::endl;
-  size_t edge = d_equalityEdges.size();
-  d_equalityEdges.push_back(EqualityEdge(t2, d_equalityGraph[t1]));
-  d_equalityEdges.push_back(EqualityEdge(t1, d_equalityGraph[t2]));
-  d_equalityGraph[t1] = edge;
-  d_equalityGraph[t2] = edge | 1;
-  d_equalityReasons.push_back(reason);
-}
-
-template <typename OwnerClass, typename NotifyClass, typename UnionFindPreferences>
-std::string EqualityEngine<OwnerClass, NotifyClass, UnionFindPreferences>::edgesToString(size_t edgeId) const {
-  std::stringstream out;
-  bool first = true;
-  while (edgeId != BitSizeTraits::id_null) {
-    const EqualityEdge& edge = d_equalityEdges[edgeId];
-    if (!first) out << ",";
-    out << d_nodes[edge.getNodeId()];
-    edgeId = edge.getNext();
-    first = false;
-  }
-  return out.str();
-}
-
-
-template <typename OwnerClass, typename NotifyClass, typename UnionFindPreferences>
-void EqualityEngine<OwnerClass, NotifyClass, UnionFindPreferences>::getExplanation(TNode t1, TNode t2, std::vector<TNode>& equalities) const {
-  Assert(getRepresentative(t1) == getRepresentative(t2));
-
-  BVDebug("equality") << "EqualityEngine::getExplanation(" << t1 << "," << t2 << ")" << std::endl;
-
-  // If the nodes are the same, we're done
-  if (t1 == t2) return;
-
-  const_cast<EqualityEngine*>(this)->backtrack();
-
-  // Queue for the BFS containing nodes
-  std::vector<BfsData> bfsQueue;
-
-  // The id's of the nodes
-  size_t t1Id = getNodeId(t1);
-  size_t t2Id = getNodeId(t2);
-
-  // Find a path from t1 to t2 in the graph (BFS)
-  bfsQueue.push_back(BfsData(t1Id, BitSizeTraits::id_null, 0));
-  size_t currentIndex = 0;
-  while (true) {
-    // There should always be a path, and every node can be visited only once (tree)
-    Assert(currentIndex < bfsQueue.size());
-
-    // The next node to visit
-    BfsData current = bfsQueue[currentIndex];
-    size_t currentNode = current.nodeId;
-
-    BVDebug("equality") << "EqualityEngine::getExplanation(): currentNode =  " << d_nodes[currentNode] << std::endl;
-
-    // Go through the equality edges of this node
-    size_t currentEdge = d_equalityGraph[currentNode];
-
-    BVDebug("equality") << "EqualityEngine::getExplanation(): edges =  " << edgesToString(currentEdge) << std::endl;
-
-    while (currentEdge != BitSizeTraits::id_null) {
-      // Get the edge
-      const EqualityEdge& edge = d_equalityEdges[currentEdge];
-
-      // If not just the backwards edge
-      if ((currentEdge | 1u) != (current.edgeId | 1u)) {
-
-        BVDebug("equality") << "EqualityEngine::getExplanation(): currentEdge = (" << d_nodes[currentNode] << "," << d_nodes[edge.getNodeId()] << ")" << std::endl;
-
-        // Did we find the path
-        if (edge.getNodeId() == t2Id) {
-
-          BVDebug("equality") << "EqualityEngine::getExplanation(): path found: " << std::endl;
-
-          // Reconstruct the path
-          do {
-            // Add the actual equality to the vector
-            equalities.push_back(d_equalityReasons[currentEdge >> 1]);
-            BVDebug("equality") << "EqualityEngine::getExplanation(): adding: " << d_equalityReasons[currentEdge >> 1] << std::endl;
-
-            // Go to the previous
-            currentEdge = bfsQueue[currentIndex].edgeId;
-            currentIndex = bfsQueue[currentIndex].previousIndex;
-          } while (currentEdge != BitSizeTraits::id_null);
-
-          // Done
-          return;
-        }
-
-        // Push to the visitation queue if it's not the backward edge
-        bfsQueue.push_back(BfsData(edge.getNodeId(), currentEdge, currentIndex));
-      }
-      
-      // Go to the next edge
-      currentEdge = edge.getNext();
-    }
-
-    // Go to the next node to visit
-    ++ currentIndex;
-  }
-}
-
-template <typename OwnerClass, typename NotifyClass, typename UnionFindPreferences>
-size_t EqualityEngine<OwnerClass, NotifyClass, UnionFindPreferences>::addTrigger(TNode t1, TNode t2) {
-
-  BVDebug("equality") << "EqualityEngine::addTrigger(" << t1 << "," << t2 << ")" << std::endl;
-
-  Assert(hasTerm(t1));
-  Assert(hasTerm(t2));
-
-  // Get the information about t1
-  size_t t1Id = getNodeId(t1);
-  size_t t1TriggerId = d_nodeTriggers[t1Id];
-  size_t t1classId = getEqualityNode(t1Id).getFind();
-
-  // Get the information about t2
-  size_t t2Id = getNodeId(t2);
-  size_t t2TriggerId = d_nodeTriggers[t2Id];
-  size_t t2classId = getEqualityNode(t2Id).getFind();
-
-  // Create the triggers
-  size_t t1NewTriggerId = d_equalityTriggers.size();
-  size_t t2NewTriggerId = t1NewTriggerId | 1;
-  d_equalityTriggers.push_back(Trigger(t1classId, t1TriggerId));
-  d_equalityTriggers.push_back(Trigger(t2classId, t2TriggerId));
-
-  // Add the trigger to the trigger graph
-  d_nodeTriggers[t1Id] = t1NewTriggerId;
-  d_nodeTriggers[t2Id] = t2NewTriggerId;
-
-  BVDebug("equality") << "EqualityEngine::addTrigger(" << t1 << "," << t2 << ") => " << t1NewTriggerId / 2 << std::endl;
-
-  // Return the global id of the trigger
-  return t1NewTriggerId / 2;
-}
-
-template <typename OwnerClass, typename NotifyClass, typename UnionFindPreferences>
-Node EqualityEngine<OwnerClass, NotifyClass, UnionFindPreferences>::normalize(TNode node, std::set<TNode>& assumptions) {
-  d_normalizationCache.clear();
-  Node result = Rewriter::rewrite(normalizeWithCache(node, assumptions));
-  d_normalizationCache.clear();
-  return result;
-}
-
-
-template <typename OwnerClass, typename NotifyClass, typename UnionFindPreferences>
-Node EqualityEngine<OwnerClass, NotifyClass, UnionFindPreferences>::normalizeWithCache(TNode node, std::set<TNode>& assumptions) {
-
-  BVDebug("equality") << "EqualityEngine::normalize(" << node << ")" << push << std::endl;
-
-  normalization_cache::iterator find = d_normalizationCache.find(node);
-  if (find != d_normalizationCache.end()) {
-    if (find->second.isNull()) {
-      // We are in a cycle
-      return node;
-    } else {
-      // Not in a cycle, return it
-      return find->second;
-    }
-  } else {
-    d_normalizationCache[node] = Node();
-  }
-
-  // Get the representative
-  Node result = hasTerm(node) ? getRepresentative(node) : node;
-  if (node != result) {
-    std::vector<TNode> equalities;
-    getExplanation(result, node, equalities);
-    utils::getConjuncts(equalities, assumptions);
-  }
-
-  // If asked, substitute the children with their representatives
-  if (UnionFindPreferences::descend(result)) {
-    // Make the builder for substitution
-    NodeBuilder<> builder;
-    builder << result.getKind();
-    kind::MetaKind metaKind = result.getMetaKind();
-    if (metaKind == kind::metakind::PARAMETERIZED) {
-      builder << result.getOperator();
-    }
-    for (unsigned i = 0; i < result.getNumChildren(); ++ i) {
-      builder << normalizeWithCache(result[i], assumptions);
-    }
-    result = builder;
-  }
-
-  BVDebug("equality") << "EqualityEngine::normalize(" << node << ") => " << result << pop << std::endl;
-
-  // Cache the result for real now
-  d_normalizationCache[node] = result;
-
-  return result;
-}
-
-} // Namespace bv
-} // Namespace theory
-} // Namespace CVC4
-
diff --git a/src/theory/bv/kinds b/src/theory/bv/kinds
index d502c5ecb..36d25de2a 100644
--- a/src/theory/bv/kinds
+++ b/src/theory/bv/kinds
@@ -57,6 +57,12 @@ operator BITVECTOR_SLE 2 "bit-vector signed less than or equal"
 operator BITVECTOR_SGT 2 "bit-vector signed greater than"
 operator BITVECTOR_SGE 2 "signed greater than or equal"
 
+constant BITVECTOR_BITOF_OP \
+	::CVC4::BitVectorBitOf \
+	::CVC4::BitVectorBitOfHashStrategy \
+	"util/bitvector.h" \
+	"operator for the bit-vector boolean bit extract"
+
 constant BITVECTOR_EXTRACT_OP \
 	::CVC4::BitVectorExtract \
 	::CVC4::BitVectorExtractHashStrategy \
@@ -93,6 +99,7 @@ constant BITVECTOR_ROTATE_RIGHT_OP \
 	"util/bitvector.h" \
 	"operator for the bit-vector rotate right"
 
+parameterized BITVECTOR_BITOF BITVECTOR_BITOF_OP 1 "bit-vector boolean bit extract"
 parameterized BITVECTOR_EXTRACT BITVECTOR_EXTRACT_OP 1 "bit-vector extract"
 parameterized BITVECTOR_REPEAT BITVECTOR_REPEAT_OP 1 "bit-vector repeat"
 parameterized BITVECTOR_ZERO_EXTEND BITVECTOR_ZERO_EXTEND_OP 1 "bit-vector zero-extend"
@@ -138,6 +145,7 @@ typerule BITVECTOR_SGT ::CVC4::theory::bv::BitVectorPredicateTypeRule
 typerule BITVECTOR_SGE ::CVC4::theory::bv::BitVectorPredicateTypeRule
 
 typerule BITVECTOR_EXTRACT ::CVC4::theory::bv::BitVectorExtractTypeRule
+typerule BITVECTOR_BITOF   ::CVC4::theory::bv::BitVectorBitOfTypeRule
 typerule BITVECTOR_CONCAT ::CVC4::theory::bv::BitVectorConcatRule
 typerule BITVECTOR_REPEAT ::CVC4::theory::bv::BitVectorRepeatTypeRule
 typerule BITVECTOR_ZERO_EXTEND ::CVC4::theory::bv::BitVectorExtendTypeRule
diff --git a/src/theory/bv/slice_manager.h b/src/theory/bv/slice_manager.h
deleted file mode 100644
index 80ac98001..000000000
--- a/src/theory/bv/slice_manager.h
+++ /dev/null
@@ -1,677 +0,0 @@
-/*********************                                                        */
-/*! \file slice_manager.h
- ** \verbatim
- ** Original author: dejan
- ** Major contributors: none
- ** Minor contributors (to current version): none
- ** This file is part of the CVC4 prototype.
- ** Copyright (c) 2009, 2010, 2011  The Analysis of Computer Systems Group (ACSys)
- ** Courant Institute of Mathematical Sciences
- ** New York University
- ** See the file COPYING in the top-level source directory for licensing
- ** information.\endverbatim
- **
- ** \brief [[ Add one-line brief description here ]]
- **
- ** [[ Add lengthier description here ]]
- ** \todo document this file
- **/
-
-/*
- * slice_manager.h
- *
- *  Created on: Feb 16, 2011
- *      Author: dejan
- */
-
-#include "cvc4_private.h"
-
-#pragma once
-
-#include "context/cdo.h"
-#include "theory/bv/theory_bv_utils.h"
-#include "theory/bv/equality_engine.h"
-#include "theory/bv/cd_set_collection.h"
-
-#include <map>
-#include <set>
-#include <vector>
-
-namespace CVC4 {
-namespace theory {
-namespace bv {
-
-/**
- * Representation of the slice points in tree.
- */
-class slice_point
-{
-public:
-
-  /** Number of bits we use for the index of the slice */
-  static const size_t s_slice_index_bits = 31;
-  /** Number of bits we use for the index of the slice_point in the slice memory (reference) */
-  static const size_t s_slice_point_reference_bits = 32;
-  /** The null reference (maximal number in the given bits) */
-  static const size_t null = (1llu << s_slice_point_reference_bits) - 1;
-
-  /** Type of the reference for the outside world */
-  typedef size_t reference_type;
-
-  /** Type of the value for the outside world */
-  typedef size_t value_type;
-
-private:
-
-  /** The value of the slice point (bit index) */
-  size_t d_value       : s_slice_index_bits;
-  /** Is this the left child */
-  size_t d_isLeftChild : 1;
-  /** Reference to the left in the tree */
-  size_t d_left        : s_slice_point_reference_bits;
-  /** Reference to the right of the tree */
-  size_t d_right       : s_slice_point_reference_bits;
-  /** Reference to the parent */
-  size_t d_parent      : s_slice_point_reference_bits;
-
-public:
-
-  slice_point(size_t value, size_t left, size_t right, size_t parent, bool isLeftChild)
-  : d_value(value), d_isLeftChild(isLeftChild ? 1 : 0), d_left(left), d_right(right), d_parent(parent) {}
-
-  bool isLeft() const  { return d_isLeftChild == 1; }
-  bool isRight() const { return d_isLeftChild == 0; }
-
-  bool hasLeft() const   { return d_left   != null; }
-  bool hasRight() const  { return d_right  != null; }
-  bool hasParent() const { return d_parent != null; }
-
-  reference_type getLeft() const   { return d_left;   }
-  reference_type getRight() const  { return d_right;  }
-  reference_type getParent() const { return d_parent; }
-
-  void removeLeft()  { Assert(d_left  != null); d_left = null;  }
-  void removeRight() { Assert(d_right != null); d_right = null; }
-
-  void setLeft(reference_type left)   { Assert(d_left  == null && left  != null); d_left  = left;  }
-  void setRight(reference_type right) { Assert(d_right == null && right != null); d_right = right; }
-
-  value_type getValue() const { return d_value; }
-};
-
-/**
- * Slice manager should keep the database of slices for the core theory leaf terms, for example
- *
- * term                           core leaf terms
- * ----------------------------------------------
- * (x + y)[31:0]                  x + y
- * a[10:0]@a[11:10]@(b + c)[1:0]  a, b, (b + c)
- * (a << 5)[10]                   (a << 5)
- *
- * If an (dis-)equality is added to the system, we refine the slicing in order to align the extracts, for example
- *
- * equality                       slicing
- * ----------------------------------------------
- * x = y                          x[32,0], y[32,0]
- * x@y = z                        x[32,0], y[32,0], z[64,32,0]
- * x@y = z, x[31:16] = y[15:0]    x[32,16,0], y[32,16,0], z[64,48,32,16,0]
- *
- * As a result of the slicing the slicing equalities are added to the equality engine, using the (associative)
- * concat function that is generated for the equality manager, for example
- *
- * equality                       added equalities
- * ----------------------------------------------
- * x = y                          none
- * x@y = z                        z = concat(z[63:32],z[31:0])
- * x@y = z, x[31:16] = y[15:0]    z = concat(z[63:32],z[31:0]),
- *                                z[63:32] = concat(z[63:48], z[47:32]),
- *                                z[31:0] = concat(z[31:16], z[15:0])
- *
- * In the last example, since concat is associative, the equality engine will know that z = concat(z[63:48], z[47:32],
- * z[31:16], z[15:0]).
- *
- */
-template <class TheoryBitvector>
-class SliceManager {
-
-public:
-
-  /** The references to backtrackable sets */
-  typedef slice_point::reference_type set_reference;
-
-  /** The set collection we'll be using */
-  typedef context::BacktrackableSetCollection<std::vector<slice_point>, slice_point, set_reference> set_collection;
-
-  /** The map type from nodes to their references */
-  typedef context::CDMap<Node, set_reference, NodeHashFunction> slicing_map;
-
-  /** The equality engine theory of bit-vectors is using */
-  typedef typename TheoryBitvector::BvEqualityEngine EqualityEngine;
-
-private:
-
-  /** The theory of bitvectors */
-  TheoryBitvector& d_theoryBitvector;
-
-  /** The equality engine */
-  EqualityEngine& d_equalityEngine;
-
-  /** The collection of backtrackable sets */
-  set_collection d_setCollection;
-
-  /**
-   * A map from base nodes to slice points. For each node, the slice points are
-   * 0 = i_1 < i_2 < ... < i_n = size, and the slices are
-   *            x[i_n-1:i_{n-1}]@x[i_{n-1}-1:i_{n-2}]@...@x[i_2-1:i_1]
-   * Each time we add a slict t = t1@t2@...@tn of a term (or a slice), we also notify the equality engine with an
-   * extra assertion. Since the equality engine is backtrackable, we will need to backtrack the slices accordingly.
-   */
-  slicing_map d_nodeSlicing;
-
-public:
-
-  SliceManager(TheoryBitvector& theoryBitvector, context::Context* context)
-  : d_theoryBitvector(theoryBitvector),
-    d_equalityEngine(theoryBitvector.getEqualityEngine()),
-    d_setCollection(context),
-    d_nodeSlicing(context)
-  {
-  }
-
-  /**
-   * Adds the equality (lhs = rhs) to the slice manager. The equality is first normalized according to the equality
-   * manager, i.e. each base term is taken from the equality manager, replaced in, and then the whole concatenation
-   * normalized and sliced wrt the current slicing. The method will not add the equalities to the equality manager,
-   * but instead will slice the equality according to the current slicing in order to align all the slices.
-   *
-   * The terms that get sliced get sent to the theory engine as equalities, i.e if we slice x[10:0] into x[10:5]@x[4:0]
-   * equality engine gets the assertion x[10:0] = concat(x[10:5], x[4:0]).
-   *
-   * input                                 output                            slicing
-   * --------------------------------------------------------------------------------------------------------------
-   * x@y = y@x                             x = y, y = x                      empty
-   * x[31:0]@x[64:32] = x                  x = x[31:0]@x[63:32]              x:{64,32,0}
-   * x@y = 0000@x@0000                     x = 0000@x[7:4], y = x[3:0]@0000  x:{8,4,0}
-   *
-   */
-  inline bool solveEquality(TNode lhs, TNode rhs);
-
-private:
-
-  inline bool solveEquality(TNode lhs, TNode rhs, const std::set<TNode>& assumptions);
-
-  /**
-   * Slices up lhs and rhs and returns the slices in lhsSlices and rhsSlices. The slices are not atomic,
-   * they are sliced in order to make one of lhs or rhs atomic, the other one can be a concatenation.
-   */
-  inline bool sliceAndSolve(std::vector<Node>& lhs, std::vector<Node>& rhs, const std::set<TNode>& assumptions);
-
-  /**
-   * Returns true if the term is already sliced wrt the current slicing. Note that, for example, even though
-   * the slicing is empty, x[i:j] is considered sliced. Sliced means that there is no slice points between i and j.
-   */
-  inline bool isSliced(TNode node) const;
-
-  /**
-   * Slices the term wrt the current slicing. When done, isSliced returns true
-   */
-  inline bool slice(TNode node, std::vector<Node>& sliced);
-
-  /**
-   * Returns the base term in the core theory of the given term, i.e.
-   * x            => x
-   * x[i:j]       => x
-   * (x + y)      => x+y
-   * (x + y)[i:j] => x+y
-   */
-  static inline TNode baseTerm(TNode node);
-
-  /**
-   * Adds a new slice to the slice set of the given term.
-   */
-  inline bool addSlice(Node term, unsigned slicePoint);
-};
-
-template <class TheoryBitvector>
-bool SliceManager<TheoryBitvector>::solveEquality(TNode lhs, TNode rhs) {
-  std::set<TNode> assumptions;
-  assumptions.insert(lhs.eqNode(rhs));
-  bool ok = solveEquality(lhs, rhs, assumptions);
-  return ok;
-}
-
-template <class TheoryBitvector>
-bool SliceManager<TheoryBitvector>::solveEquality(TNode lhs, TNode rhs, const std::set<TNode>& assumptions) {
-
-  BVDebug("slicing") << "SliceMagager::solveEquality(" << lhs << "," << rhs << "," << utils::setToString(assumptions) << ")" << push << std::endl;
-
-  bool ok;
-
-  // The concatenations on the left-hand side (reverse order, first is on top)
-  std::vector<Node> lhsTerms;
-  if (lhs.getKind() == kind::BITVECTOR_CONCAT) {
-    for (int i = (int) lhs.getNumChildren() - 1; i >= 0; -- i) {
-      lhsTerms.push_back(lhs[i]);
-    }
-  } else {
-    lhsTerms.push_back(lhs);
-  }
-
-  // The concatenations on the right-hand side (reverse order, first is on top)
-  std::vector<Node> rhsTerms;
-  if (rhs.getKind() == kind::BITVECTOR_CONCAT) {
-    for (int i = (int) rhs.getNumChildren() - 1; i >= 0; --i) {
-      rhsTerms.push_back(rhs[i]);
-    }
-  } else {
-    rhsTerms.push_back(rhs);
-  }
-
-  // Slice the individual terms to align them
-  ok = sliceAndSolve(lhsTerms, rhsTerms, assumptions);
-
-  BVDebug("slicing") << "SliceMagager::solveEquality(" << lhs << "," << rhs << "," << utils::setToString(assumptions) << ")" << pop << std::endl;
-
-  return ok;
-}
-
-
-template <class TheoryBitvector>
-bool SliceManager<TheoryBitvector>::sliceAndSolve(std::vector<Node>& lhs, std::vector<Node>& rhs, const std::set<TNode>& assumptions)
-{
-
-  BVDebug("slicing") << "SliceManager::sliceAndSolve()" << std::endl;
-
-  // Go through the work-list, solve and align
-  while (!lhs.empty()) {
-
-    Assert(!rhs.empty());
-
-    BVDebug("slicing") << "SliceManager::sliceAndSolve(): lhs " << utils::vectorToString(lhs) << std::endl;
-    BVDebug("slicing") << "SliceManager::sliceAndSolve(): rhs " << utils::vectorToString(rhs) << std::endl;
-
-    // The terms that we need to slice
-    Node lhsTerm = lhs.back();
-    Node rhsTerm = rhs.back();
-
-    BVDebug("slicing") << "SliceManager::sliceAndSolve(): " << lhsTerm << " : " << rhsTerm << std::endl;
-
-    // If the terms are not sliced wrt the current slicing, we have them sliced
-    lhs.pop_back();
-    if (!isSliced(lhsTerm)) {
-      if (!slice(lhsTerm, lhs)) return false;
-      BVDebug("slicing") << "SliceManager::sliceAndSolve(): lhs sliced" << std::endl;
-      continue;
-    }
-    rhs.pop_back();
-    if (!isSliced(rhsTerm)) {
-      if (!slice(rhsTerm, rhs)) return false;
-      // We also need to put lhs back
-      lhs.push_back(lhsTerm);
-      BVDebug("slicing") << "SliceManager::sliceAndSolve(): rhs sliced" << std::endl;
-      continue;
-    }
-
-    BVDebug("slicing") << "SliceManager::sliceAndSolve(): both lhs and rhs sliced already" << std::endl;
-
-    // The solving concatenation
-    std::vector<Node> concatTerms;
-
-    // If the slices are of the same size we do the additional work
-    int sizeDifference = utils::getSize(lhsTerm) - utils::getSize(rhsTerm);
-
-    // We slice constants immediately
-    if (sizeDifference > 0 && lhsTerm.getKind() == kind::CONST_BITVECTOR) {
-      Node low  = utils::mkConst(lhsTerm.getConst<BitVector>().extract(sizeDifference - 1, 0));
-      Node high = utils::mkConst(lhsTerm.getConst<BitVector>().extract(utils::getSize(lhsTerm) - 1, sizeDifference));
-      d_equalityEngine.addTerm(low); d_equalityEngine.addTerm(high);
-      lhs.push_back(low);
-      lhs.push_back(high);
-      rhs.push_back(rhsTerm);
-      continue;
-    }
-    if (sizeDifference < 0 && rhsTerm.getKind() == kind::CONST_BITVECTOR) {
-      Node low  = utils::mkConst(rhsTerm.getConst<BitVector>().extract(-sizeDifference - 1, 0));
-      Node high = utils::mkConst(rhsTerm.getConst<BitVector>().extract(utils::getSize(rhsTerm) - 1, -sizeDifference));
-      d_equalityEngine.addTerm(low); d_equalityEngine.addTerm(high);
-      rhs.push_back(low);
-      rhs.push_back(high);
-      lhs.push_back(lhsTerm);
-      continue;
-    }
-
-    enum SolvingFor {
-      SOLVING_FOR_LHS,
-      SOLVING_FOR_RHS
-    } solvingFor = sizeDifference < 0 || lhsTerm.getKind() == kind::CONST_BITVECTOR ? SOLVING_FOR_RHS : SOLVING_FOR_LHS;
-
-    BVDebug("slicing") << "SliceManager::sliceAndSolve(): " << (solvingFor == SOLVING_FOR_LHS ? "solving for LHS" : "solving for RHS") << std::endl;
-
-    // When we slice in order to align, we might have to reslice the one we are solving for
-    bool reslice = false;
-
-    switch (solvingFor) {
-    case SOLVING_FOR_RHS: {
-      concatTerms.push_back(lhsTerm);
-      // Maybe we need to add more lhs to make them equal
-      while (sizeDifference < 0 && !reslice) {
-        Assert(lhs.size() > 0);
-        // Get the next part for lhs
-        lhsTerm = lhs.back();
-        lhs.pop_back();
-        // Slice if necessary
-        if (!isSliced(lhsTerm)) {
-          if (!slice(lhsTerm, lhs)) return false;
-          continue;
-        }
-        // If we go above 0, we need to cut it
-        if (sizeDifference + (int)utils::getSize(lhsTerm) > 0) {
-          // Slice it so it fits
-          addSlice(lhsTerm, (int)utils::getSize(lhsTerm) + sizeDifference);
-          if (!slice(lhsTerm, lhs)) return false;
-          if (!isSliced(rhsTerm)) {
-            if (!slice(rhsTerm, rhs)) return false;
-            while(!concatTerms.empty()) {
-              lhs.push_back(concatTerms.back());
-              concatTerms.pop_back();
-            }
-            reslice = true;
-          }
-          continue;
-        }
-        concatTerms.push_back(lhsTerm);
-        sizeDifference += utils::getSize(lhsTerm);
-      }
-      break;
-    }
-    case SOLVING_FOR_LHS: {
-      concatTerms.push_back(rhsTerm);
-      // Maybe we need to add more rhs to make them equal
-      while (sizeDifference > 0 && !reslice) {
-        Assert(rhs.size() > 0);
-        // Get the next part for lhs
-        rhsTerm = rhs.back();
-        rhs.pop_back();
-        // Slice if necessary
-        if (!isSliced(rhsTerm)) {
-          if (!slice(rhsTerm, rhs)) return false;
-          continue;
-        }
-        // If we go below 0, we need to cut it
-        if (sizeDifference - (int)utils::getSize(rhsTerm) < 0) {
-          // Slice it so it fits
-          addSlice(rhsTerm, (int)utils::getSize(rhsTerm) - sizeDifference);
-          if (!slice(rhsTerm, rhs)) return false;
-	  if (!isSliced(lhsTerm)) {
-            if (!slice(lhsTerm, lhs)) return false;
-            while(!concatTerms.empty()) {
-              rhs.push_back(concatTerms.back());
-              concatTerms.pop_back();
-            }
-            reslice = true;
-          }
-          continue;
-        }
-        concatTerms.push_back(rhsTerm);
-        sizeDifference -= utils::getSize(rhsTerm);
-      }
-      break;
-    }
-    }
-
-    // If we need to reslice
-    if (reslice) {
-	continue;
-    }
-
-    Assert(sizeDifference == 0);
-
-    Node concat = utils::mkConcat(concatTerms);
-    BVDebug("slicing") << "SliceManager::sliceAndSolve(): concatenation " << concat << std::endl;
-
-    // We have them equal size now. If the base term of the one we are solving is solved into a
-    // non-trivial concatenation already, we have to normalize. A concatenation is non-trivial if
-    // it is not a direct slicing, i.e it is a concat, and normalize(x) != x
-    switch (solvingFor) {
-    case SOLVING_FOR_LHS: {
-      TNode lhsTermRepresentative = d_equalityEngine.getRepresentative(lhsTerm);
-      if (lhsTermRepresentative != lhsTerm &&
-          (lhsTermRepresentative.getKind() == kind::BITVECTOR_CONCAT || lhsTermRepresentative.getKind() == kind::CONST_BITVECTOR)) {
-        // We need to normalize and solve the normalized equations
-        std::vector<TNode> explanation;
-        d_equalityEngine.getExplanation(lhsTerm, lhsTermRepresentative, explanation);
-        std::set<TNode> additionalAssumptions(assumptions);
-        utils::getConjuncts(explanation, additionalAssumptions);
-        bool ok = solveEquality(lhsTermRepresentative, concat, additionalAssumptions);
-        if (!ok) return false;
-      } else {
-        // We're fine, just add the equality
-        BVDebug("slicing") << "SliceManager::sliceAndSolve(): adding " << lhsTerm << " = " << concat << " " << utils::setToString(assumptions) << std::endl;
-        d_equalityEngine.addTerm(concat);
-        bool ok = d_equalityEngine.addEquality(lhsTerm, concat, utils::mkConjunction(assumptions));
-        if (!ok) return false;
-      }
-      break;
-    }
-    case SOLVING_FOR_RHS: {
-      TNode rhsTermRepresentative = d_equalityEngine.getRepresentative(rhsTerm);
-      if (rhsTermRepresentative != rhsTerm &&
-          (rhsTermRepresentative.getKind() == kind::BITVECTOR_CONCAT || rhsTermRepresentative.getKind() == kind::CONST_BITVECTOR)) {
-        // We need to normalize and solve the normalized equations
-        std::vector<TNode> explanation;
-        d_equalityEngine.getExplanation(rhsTerm, rhsTermRepresentative, explanation);
-        std::set<TNode> additionalAssumptions(assumptions);
-        utils::getConjuncts(explanation, additionalAssumptions);
-        bool ok = solveEquality(rhsTermRepresentative, concat, additionalAssumptions);
-        if (!ok) return false;
-      } else {
-        // We're fine, just add the equality
-        BVDebug("slicing") << "SliceManager::sliceAndSolve(): adding " << rhsTerm << " = " << concat << utils::setToString(assumptions) << std::endl;
-        d_equalityEngine.addTerm(concat);
-        bool ok = d_equalityEngine.addEquality(rhsTerm, concat, utils::mkConjunction(assumptions));
-        if (!ok) return false;
-      }
-      break;
-    }
-    }
-  }
-
-  return true;
-}
-
-template <class TheoryBitvector>
-bool SliceManager<TheoryBitvector>::isSliced(TNode node) const {
-
-  BVDebug("slicing") << "SliceManager::isSliced(" << node << ")" << std::endl;
-
-  bool result = false;
-
-  // Constants are always sliced
-  if (node.getKind() == kind::CONST_BITVECTOR) {
-    result = true;
-  } else {
-    // The indices of the beginning and end
-    Kind nodeKind = node.getKind();
-    unsigned high = nodeKind == kind::BITVECTOR_EXTRACT ? utils::getExtractHigh(node) : utils::getSize(node) - 1;
-    unsigned low  = nodeKind == kind::BITVECTOR_EXTRACT ? utils::getExtractLow(node) : 0;
-
-    // Get the base term
-    TNode nodeBase = baseTerm(node);
-    Assert(nodeBase.getKind() != kind::BITVECTOR_CONCAT);
-    Assert(nodeBase.getKind() != kind::CONST_BITVECTOR);
-
-    // Get the base term slice set
-    slicing_map::const_iterator find = d_nodeSlicing.find(nodeBase);
-    // If no slices, it's just a term, so we are done, UNLESS it's an extract
-    if (find == d_nodeSlicing.end()) {
-      result = nodeKind != kind::BITVECTOR_EXTRACT;
-    } else {
-      set_reference sliceSet = (*find).second;
-      Assert(d_setCollection.size(sliceSet) >= 2);
-      // The term is not sliced if one of the borders is not in the slice set or
-      // there is a point between the borders      
-      result = 
-	d_setCollection.contains(sliceSet, low) && d_setCollection.contains(sliceSet, high + 1) &&
-        (low == high || d_setCollection.count(sliceSet, low + 1, high) == 0);
-    }
-  }
-
-  BVDebug("slicing") << "SliceManager::isSliced(" << node << ") => " << (result ? "true" : "false") << std::endl;
-  return result;
-}
-
-template <class TheoryBitvector>
-bool SliceManager<TheoryBitvector>::addSlice(Node node, unsigned slicePoint) {
-  BVDebug("slicing") << "SliceMagager::addSlice(" << node << "," << slicePoint << ")" << std::endl;
-
-  bool ok = true;
-
-  int low  = node.getKind() == kind::BITVECTOR_EXTRACT ? utils::getExtractLow(node) : 0;
-  int high = node.getKind() == kind::BITVECTOR_EXTRACT ? utils::getExtractHigh(node) + 1: utils::getSize(node);
-  slicePoint += low;
-
-  TNode nodeBase = baseTerm(node);
-
-  Assert(nodeBase.getKind() != kind::CONST_BITVECTOR);
-
-  set_reference sliceSet;
-  slicing_map::iterator find = d_nodeSlicing.find(nodeBase);
-  if (find == d_nodeSlicing.end()) {
-    d_nodeSlicing[nodeBase] = sliceSet = d_setCollection.newSet(0);
-    d_setCollection.insert(sliceSet, utils::getSize(nodeBase));
-  } else {
-    sliceSet = (*find).second;
-  }
-
-  Assert(d_setCollection.size(sliceSet) >= 2);
-
-  // What are the points surrounding the new slice point
-  int prev = d_setCollection.prev(sliceSet, slicePoint);
-  int next = d_setCollection.next(sliceSet, slicePoint);
-
-  // Add the slice to the set
-  d_setCollection.insert(sliceSet, slicePoint);
-  BVDebug("slicing") << "SliceMagager::addSlice(" << node << "," << slicePoint << "): current set " << d_setCollection.toString(sliceSet) << std::endl;
-
-  // Add the terms and the equality to the equality engine
-  Node t1 = utils::mkExtract(nodeBase, next - 1, slicePoint);
-  Node t2 = utils::mkExtract(nodeBase, slicePoint - 1, prev);
-  Node nodeSlice = (next == high && prev == low) ? node : utils::mkExtract(nodeBase, next - 1, prev);
-  Node concat = utils::mkConcat(t1, t2);
-
-  d_equalityEngine.addTerm(t1);
-  d_equalityEngine.addTerm(t2);
-  d_equalityEngine.addTerm(nodeSlice);
-  d_equalityEngine.addTerm(concat);
-
-  // We are free to add this slice, unless the slice has a representative that's already a concat
-  TNode nodeSliceRepresentative = d_equalityEngine.getRepresentative(nodeSlice);
-  if (nodeSliceRepresentative.getKind() != kind::BITVECTOR_CONCAT) {
-    // Add the slice to the equality engine
-    ok = d_equalityEngine.addEquality(nodeSlice, concat, utils::mkTrue());
-  } else {
-    // If the representative is a concat, we must solve it
-    // There is no need do add nodeSlice = concat as we will solve the representative of nodeSlice
-    std::set<TNode> assumptions;
-    std::vector<TNode> equalities;
-    d_equalityEngine.getExplanation(nodeSlice, nodeSliceRepresentative, equalities);
-    utils::getConjuncts(equalities, assumptions);
-    ok = solveEquality(nodeSliceRepresentative, concat, assumptions);
-  }
-
-  BVDebug("slicing") << "SliceMagager::addSlice(" << node << "," << slicePoint << ") => " << d_setCollection.toString(d_nodeSlicing[nodeBase]) << std::endl;
-
-  return ok;
-}
-
-template <class TheoryBitvector>
-inline bool SliceManager<TheoryBitvector>::slice(TNode node, std::vector<Node>& sliced) {
-
-  BVDebug("slicing") << "SliceManager::slice(" << node << ")" << std::endl;
-
-  Assert(!isSliced(node));
-
-  // The indices of the beginning and (one past) end
-  unsigned high = node.getKind() == kind::BITVECTOR_EXTRACT ? utils::getExtractHigh(node) + 1 : utils::getSize(node);
-  unsigned low  = node.getKind() == kind::BITVECTOR_EXTRACT ? utils::getExtractLow(node) : 0;
-  BVDebug("slicing") << "SliceManager::slice(" << node << "): low: " << low << std::endl;
-  BVDebug("slicing") << "SliceManager::slice(" << node << "): high: " << high << std::endl;
-
-  // Get the base term
-  TNode nodeBase = baseTerm(node);
-  Assert(nodeBase.getKind() != kind::BITVECTOR_CONCAT);
-  Assert(nodeBase.getKind() != kind::CONST_BITVECTOR);
-
-  // The nodes slice set
-  set_reference nodeSliceSet;
-
-  // Find the current one or construct it
-  slicing_map::iterator findSliceSet = d_nodeSlicing.find(nodeBase);
-  if (findSliceSet == d_nodeSlicing.end()) {
-    d_nodeSlicing[nodeBase] = nodeSliceSet = d_setCollection.newSet(0);
-    d_setCollection.insert(nodeSliceSet, utils::getSize(nodeBase));
-  } else {
-    nodeSliceSet = d_nodeSlicing[nodeBase];
-  }
-
-  Assert(d_setCollection.size(nodeSliceSet) >= 2);
-
-  BVDebug("slicing") << "SliceManager::slice(" << node << "): current: " << d_setCollection.toString(nodeSliceSet) << std::endl;
-  
-  // Go through all the points i_0 <= low < i_1 < ... < i_{n-1} < high <= i_n from the slice set
-  // and generate the slices [i_0:low-1][low:i_1-1] [i_1:i2] ... [i_{n-1}:high-1][high:i_n-1]. They are in reverse order,
-  // as they should be
-  
-  // The high bound already in the slicing
-  size_t i_n = high == utils::getSize(nodeBase) ? high: d_setCollection.next(nodeSliceSet, high - 1);
-  BVDebug("slicing") << "SliceManager::slice(" << node << "): i_n: " << i_n << std::endl;  
-  // Add the new point to the slice set (they might be there already)
-  if (high < i_n) {
-    if (!addSlice(nodeBase, high)) return false;
-  }
-  // The low bound already in the slicing (slicing might have changed after adding high)
-  size_t i_0 = low == 0 ? 0 : d_setCollection.prev(nodeSliceSet, low + 1);
-  BVDebug("slicing") << "SliceManager::slice(" << node << "): i_0: " << i_0 << std::endl;
-  // Add the new points to the slice set (they might be there already)
-  if (i_0 < low) {
-    if (!addSlice(nodeBase, low)) return false;
-  }
-
-  // Get the slice points
-  std::vector<size_t> slicePoints;
-  if (low + 1 < high) {
-    d_setCollection.getElements(nodeSliceSet, low + 1, high - 1, slicePoints);
-  }
-
-  // Construct the actuall slicing
-  if (slicePoints.size() > 0) {
-    BVDebug("slicing") << "SliceManager::slice(" << node << "): adding" << utils::mkExtract(nodeBase, slicePoints[0] - 1, low) << std::endl;
-    sliced.push_back(utils::mkExtract(nodeBase, slicePoints[0] - 1, low));
-    for (unsigned i = 1; i < slicePoints.size(); ++ i) {
-      BVDebug("slicing") << "SliceManager::slice(" << node << "): adding" << utils::mkExtract(nodeBase, slicePoints[i] - 1, slicePoints[i-1])<< std::endl;
-      sliced.push_back(utils::mkExtract(nodeBase, slicePoints[i] - 1, slicePoints[i-1]));
-    }
-    BVDebug("slicing") << "SliceManager::slice(" << node << "): adding" << utils::mkExtract(nodeBase, high-1, slicePoints.back()) << std::endl;
-    sliced.push_back(utils::mkExtract(nodeBase, high-1, slicePoints.back()));
-  } else {
-    sliced.push_back(utils::mkExtract(nodeBase, high - 1, low));
-  }
-  
-  return true;
-}
-
-template <class TheoryBitvector>
-TNode SliceManager<TheoryBitvector>::baseTerm(TNode node) {
-  if (node.getKind() == kind::BITVECTOR_EXTRACT) {
-    Assert(node[0].getKind() != kind::BITVECTOR_EXTRACT);
-    Assert(node[0].getKind() != kind::CONST_BITVECTOR);
-    return node[0];
-  } else {
-    Assert(node.getKind() != kind::BITVECTOR_CONCAT);
-    return node;
-  }
-}
-
-} // Namespace bv
-} // Namespace theory
-} // Namespace CVC4
diff --git a/src/theory/bv/theory_bv.cpp b/src/theory/bv/theory_bv.cpp
index c977435ec..79c065d7e 100644
--- a/src/theory/bv/theory_bv.cpp
+++ b/src/theory/bv/theory_bv.cpp
@@ -19,196 +19,82 @@
 
 #include "theory/bv/theory_bv.h"
 #include "theory/bv/theory_bv_utils.h"
-
 #include "theory/valuation.h"
 
+#include "theory/bv/bv_sat.h"
+
 using namespace CVC4;
 using namespace CVC4::theory;
 using namespace CVC4::theory::bv;
-using namespace CVC4::theory::bv::utils;
+using namespace CVC4::context;
 
 using namespace std;
+using namespace CVC4::theory::bv::utils;
 
-void TheoryBV::preRegisterTerm(TNode node) {
+TheoryBV::TheoryBV(context::Context* c, context::UserContext* u, OutputChannel& out, Valuation valuation)
+  : Theory(THEORY_BV, c, u, out, valuation), 
+    d_context(c),
+    d_assertions(c),
+    d_bitblaster(new Bitblaster(c) ),
+    d_statistics()
+  {
+    d_true = utils::mkTrue();
+  }
+TheoryBV::~TheoryBV() {
+  delete d_bitblaster; 
+}
+TheoryBV::Statistics::Statistics():
+  d_avgConflictSize("theory::bv::AvgBVConflictSize"),
+  d_solveSubstitutions("theory::bv::NumberOfSolveSubstitutions", 0)
+{
+  StatisticsRegistry::registerStat(&d_avgConflictSize);
+  StatisticsRegistry::registerStat(&d_solveSubstitutions);
+}
 
-  BVDebug("bitvector") << "TheoryBV::preRegister(" << node << ")" << std::endl;
+TheoryBV::Statistics::~Statistics() {
+  StatisticsRegistry::unregisterStat(&d_avgConflictSize);
+  StatisticsRegistry::unregisterStat(&d_solveSubstitutions);
+}
 
-  if (node.getKind() == kind::EQUAL) {
-    d_eqEngine.addTerm(node[0]);
-    if (node[0].getKind() == kind::BITVECTOR_CONCAT) {
-      for (unsigned i = 0, i_end = node[0].getNumChildren(); i < i_end; ++ i) {
-        d_eqEngine.addTerm(node[0][i]);
-      }
-    }
-    d_eqEngine.addTerm(node[1]);
-    if (node[1].getKind() == kind::BITVECTOR_CONCAT) {
-      for (unsigned i = 0, i_end = node[1].getNumChildren(); i < i_end; ++ i) {
-        d_eqEngine.addTerm(node[1][i]);
-      }
-    }
+void TheoryBV::preRegisterTerm(TNode node) {
 
-    d_normalization[node] = new Normalization(d_context, node);
-  }
+  BVDebug("bitvector-preregister") << "TheoryBV::preRegister(" << node << ")" << std::endl;
+  //marker literal: bitblast all terms before we start
+  d_bitblaster->bitblast(node); 
 }
 
 void TheoryBV::check(Effort e) {
-
   BVDebug("bitvector") << "TheoryBV::check(" << e << ")" << std::endl;
-
-  // Normalization iterators
-  NormalizationMap::iterator it = d_normalization.begin();
-  NormalizationMap::iterator it_end = d_normalization.end();
-
-  // Get all the assertions
-  std::vector<TNode> assertionsList;
-  while (!done()) {
-    // Get the assertion
-    TNode assertion = get();
-    d_assertions.insert(assertion);
-    assertionsList.push_back(assertion);
-  }
-
-  bool normalizeEqualities = false;
-
-  for (unsigned i = 0; i < assertionsList.size(); ++ i) {
-
-    TNode assertion = assertionsList[i];
-
-    BVDebug("bitvector") << "TheoryBV::check(" << e << "): asserting: " << assertion << std::endl;
-
-    // Do the right stuff
-    switch (assertion.getKind()) {
-    case kind::EQUAL: {
-      // Slice and solve the equality
-      bool ok = d_sliceManager.solveEquality(assertion[0], assertion[1]);
-      if (!ok) return;
-      // Normalize all equalities
-      normalizeEqualities = true;
-      it = d_normalization.begin();
-      it = d_normalization.end();
-      break;
+  if (fullEffort(e)) {
+    std::vector<TNode> assertions; 
+    while (!done()) {
+      TNode assertion = get();
+      Debug("bitvector") << "assertion " << assertion << "\n"; 
+      assertions.push_back(assertion);
+      d_bitblaster->bitblast(assertion); 
     }
-    case kind::NOT: {
-      if (!normalizeEqualities) {
-        // We still need to check this dis-equality, as it might have been pre-registered just now
-        // so we didn't have a chance to propagate
-        it = d_normalization.find(assertion[0]);
-        if (it->second->assumptions.size() == 1) {
-          // Just normalize this equality
-          normalizeEqualities = true;
-          it_end = it;
-          it_end ++;
-        }
-      }
-      break;
+    
+    std::vector<TNode>::const_iterator it = assertions.begin();
+    for (; it != assertions.end(); ++it) {
+      d_bitblaster->assertToSat(*it); 
     }
-    default:
-      Unhandled(assertion.getKind());
-    }
-  }
-
-  if (normalizeEqualities) {
+    bool res = d_bitblaster->solve();
+    if (res == false) {
+      std::vector<TNode> conflictAtoms;
+      d_bitblaster->getConflict(conflictAtoms);
 
-    BVDebug("bitvector") << "Checking for propagations" << std::endl;
-  
-    NormalizationMap::iterator it = d_normalization.begin();
-    NormalizationMap::iterator it_end = d_normalization.end();
-    for(; it != it_end; ++ it) {
-
-      TNode equality = it->first;
-      BVDebug("bitvector") << "Checking " << equality << std::endl;
-      Normalization& normalization = *it->second;
+      d_statistics.d_avgConflictSize.addEntry(conflictAtoms.size());
       
-      // If asserted, we don't care
-      if (d_assertions.find(equality) != d_assertions.end()) continue; 
-
-      // Assumptions
-      std::set<TNode> assumptions; 
-      TNode lhs = normalization.equalities.back()[0];
-      TNode rhs = normalization.equalities.back()[1];
-      // If already satisfied, do nothing
-      if (lhs == rhs) continue;
-
-      Node lhsNormalized = d_eqEngine.normalize(lhs, assumptions);
-      Node rhsNormalized = d_eqEngine.normalize(rhs, assumptions);
-
-      if (lhsNormalized == lhs && rhsNormalized == rhs) continue;
-
-      normalization.equalities.push_back(lhsNormalized.eqNode(rhsNormalized));
-      normalization.assumptions.push_back(assumptions);
-
-      BVDebug("bitvector") << "Adding normalization " << lhsNormalized.eqNode(rhsNormalized) << std::endl;
-      BVDebug("bitvector") << "       assumptions   " << utils::setToString(assumptions) << std::endl;
-
-
-      BVDebug("bitvector") << "TheoryBV::check(" << e << "): normalizes to " << lhsNormalized << " = " << rhsNormalized << std::endl;
-
-      // If both are equal we can propagate
-      bool propagate = lhsNormalized == rhsNormalized;
-      // otherwise if both are constants, we propagate negation (if not already there)
-      bool propagateNegation = !propagate &&
-          lhsNormalized.getKind() == kind::CONST_BITVECTOR && rhsNormalized.getKind() == kind::CONST_BITVECTOR
-          && d_assertions.find(equality.notNode()) == d_assertions.end();
-          ;
-      if (propagate || propagateNegation) {
-        Node implied = propagate        ? Node(equality)     : equality.notNode() ;
-        Node impliedNegated = propagate ? equality.notNode() : Node(equality)     ;
-        // If the negation of what's implied has been asserted, we are in conflict
-        if (d_assertions.find(impliedNegated) != d_assertions.end()) {
-          BVDebug("bitvector") << "TheoryBV::check(" << e << "): conflict with " << utils::setToString(assumptions) << std::endl;
-          // Construct the assumptions
-          for (unsigned i = 0; i < normalization.assumptions.size(); ++ i) {
-            assumptions.insert(normalization.assumptions[i].begin(), normalization.assumptions[i].end());
-          }
-          // Make the conflict
-          assumptions.insert(impliedNegated);
-          d_out->conflict(mkConjunction(assumptions));
-          return;
-        }
-        // Otherwise we propagate the implication
-        else {
-          BVDebug("bitvector") << "TheoryBV::check(" << e << "): propagating " << implied << std::endl;
-          d_out->propagate(implied);
-          d_assertions.insert(implied);
-        }
-      }
+      Node conflict = mkConjunction(conflictAtoms);
+      d_out->conflict(conflict);
+      return; 
     }
   }
 }
 
-bool TheoryBV::triggerEquality(size_t triggerId) {
-  BVDebug("bitvector") << "TheoryBV::triggerEquality(" << triggerId << ")" << std::endl;
-  Assert(triggerId < d_triggers.size());
-  BVDebug("bitvector") << "TheoryBV::triggerEquality(" << triggerId << "): " << d_triggers[triggerId] << std::endl;
-
-  return true;
-
-  TNode equality = d_triggers[triggerId];
-
-  // If we have just asserted this equality ignore it
-  if (d_assertions.contains(equality)) return true;
-
-  // If we have a negation asserted, we have a confict
-  if (d_assertions.contains(equality.notNode())) {
-
-    std::vector<TNode> explanation;
-    d_eqEngine.getExplanation(equality[0], equality[1], explanation);
-    std::set<TNode> assumptions;
-    assumptions.insert(equality.notNode());
-    utils::getConjuncts(explanation, assumptions);
-    d_out->conflict(utils::mkConjunction(assumptions));
-
-    return false;
-  }
-
-  // Otherwise we propagate this equality
-  d_out->propagate(equality);
-
-  return true;
-}
 
 Node TheoryBV::getValue(TNode n) {
-  NodeManager* nodeManager = NodeManager::currentNM();
+  //NodeManager* nodeManager = NodeManager::currentNM();
 
   switch(n.getKind()) {
 
@@ -216,8 +102,7 @@ Node TheoryBV::getValue(TNode n) {
     Unhandled(kind::VARIABLE);
 
   case kind::EQUAL: // 2 args
-    return nodeManager->
-      mkConst( d_valuation.getValue(n[0]) == d_valuation.getValue(n[1]) );
+    Unhandled(kind::VARIABLE);
 
   default:
     Unhandled(n.getKind());
@@ -229,13 +114,37 @@ Node TheoryBV::explain(TNode node) {
 
   TNode equality = node.getKind() == kind::NOT ? node[0] : node;
   Assert(equality.getKind() == kind::EQUAL);
+  Assert(0); 
+  return node; 
+
+}
 
-  context::CDList< set<TNode> >& vec = d_normalization[equality]->assumptions;
-  std::set<TNode> assumptions;
-  for (unsigned i = 0; i < vec.size(); ++ i) {
-    BVDebug("bitvector") << "Adding normalization " << d_normalization[equality]->equalities[i] << std::endl;
-    BVDebug("bitvector") << "       assumptions   " << utils::setToString(d_normalization[equality]->assumptions[i]) << std::endl;
-    assumptions.insert(vec[i].begin(), vec[i].end());
+// Node TheoryBV::preprocessTerm(TNode term) {
+//   return term; //d_staticEqManager.find(term);
+// }
+
+Theory::PPAssertStatus TheoryBV::ppAssert(TNode in, SubstitutionMap& outSubstitutions) {
+  switch(in.getKind()) {
+  case kind::EQUAL:
+    
+    if (in[0].getMetaKind() == kind::metakind::VARIABLE && !in[1].hasSubterm(in[0])) {
+      ++(d_statistics.d_solveSubstitutions); 
+      outSubstitutions.addSubstitution(in[0], in[1]);
+      return PP_ASSERT_STATUS_SOLVED;
+    }
+    if (in[1].getMetaKind() == kind::metakind::VARIABLE && !in[0].hasSubterm(in[1])) {
+      ++(d_statistics.d_solveSubstitutions); 
+      outSubstitutions.addSubstitution(in[1], in[0]);
+      return PP_ASSERT_STATUS_SOLVED;
+    }
+    // to do constant propagations
+
+    break;
+  case kind::NOT:
+    break;
+  default:
+    // TODO other predicates
+    break;
   }
-  return utils::mkConjunction(assumptions);
+  return PP_ASSERT_STATUS_UNSOLVED;
 }
diff --git a/src/theory/bv/theory_bv.h b/src/theory/bv/theory_bv.h
index 11ddceaae..5303b6595 100644
--- a/src/theory/bv/theory_bv.h
+++ b/src/theory/bv/theory_bv.h
@@ -23,119 +23,42 @@
 
 #include "theory/theory.h"
 #include "context/context.h"
-#include "context/cdset.h"
 #include "context/cdlist.h"
-#include "theory/bv/equality_engine.h"
-#include "theory/bv/slice_manager.h"
+#include "theory/bv/theory_bv_utils.h"
+#include "util/stats.h"
+
+namespace BVMinisat {
+class SimpSolver; 
+}
+
 
 namespace CVC4 {
 namespace theory {
 namespace bv {
 
+/// forward declarations 
+class Bitblaster;
+
 class TheoryBV : public Theory {
 
 public:
 
-  class EqualityNotify {
-    TheoryBV& d_theoryBV;
-  public:
-    EqualityNotify(TheoryBV& theoryBV)
-    : d_theoryBV(theoryBV) {}
-
-    bool operator () (size_t triggerId) {
-      return d_theoryBV.triggerEquality(triggerId);
-    }
-    void conflict(Node explanation) {
-      std::set<TNode> assumptions;
-      utils::getConjuncts(explanation, assumptions);
-      d_theoryBV.d_out->conflict(utils::mkConjunction(assumptions));
-    }
-  };
-
-  struct BVEqualitySettings {
-    static inline bool descend(TNode node) {
-      return node.getKind() == kind::BITVECTOR_CONCAT || node.getKind() == kind::BITVECTOR_EXTRACT;
-    }
-
-    /** Returns true if node1 has preference to node2 as a representative, otherwise node2 is used */
-    static inline bool mergePreference(TNode node1, unsigned node1size, TNode node2, unsigned node2size) {
-      if (node1.getKind() == kind::CONST_BITVECTOR) {
-        Assert(node2.getKind() != kind::CONST_BITVECTOR);
-        return true;
-      }
-      if (node2.getKind() == kind::CONST_BITVECTOR) {
-        Assert(node1.getKind() != kind::CONST_BITVECTOR);
-        return false;
-      }
-      if (node1.getKind() == kind::BITVECTOR_CONCAT) {
-        Assert(node2.getKind() != kind::BITVECTOR_CONCAT);
-        return true;
-      }
-      if (node2.getKind() == kind::BITVECTOR_CONCAT) {
-        Assert(node1.getKind() != kind::BITVECTOR_CONCAT);
-        return false;
-      }
-      return node2size < node1size;
-    }
-  };
-
-  typedef EqualityEngine<TheoryBV, EqualityNotify, BVEqualitySettings> BvEqualityEngine;
-
 private:
 
-  /** Equality reasoning engine */
-  BvEqualityEngine d_eqEngine;
-
-  /** Slice manager */
-  SliceManager<TheoryBV> d_sliceManager;
-
-  /** Equality triggers indexed by ids from the equality manager */
-  std::vector<Node> d_triggers;
-  
   /** The context we are using */
   context::Context* d_context;
 
   /** The asserted stuff */
-  context::CDSet<TNode, TNodeHashFunction> d_assertions;
-
-  /** Asserted dis-equalities */
-  context::CDList<TNode> d_disequalities;
-
-  struct Normalization {
-    context::CDList<Node> equalities;
-    context::CDList< std::set<TNode> > assumptions;
-    Normalization(context::Context* c, TNode eq)
-    : equalities(c), assumptions(c) {
-      equalities.push_back(eq);
-      assumptions.push_back(std::set<TNode>());
-    }
-  };
-
-  /** Map from equalities to their noramlization information */
-  typedef __gnu_cxx::hash_map<TNode, Normalization*, TNodeHashFunction> NormalizationMap;
-  NormalizationMap d_normalization;
-
-  /** Called by the equality managere on triggers */
-  bool triggerEquality(size_t triggerId);
-
+  context::CDList<TNode> d_assertions;
+  
+  /** Bitblaster */
+  Bitblaster* d_bitblaster; 
   Node d_true;
-
+    
 public:
 
-  TheoryBV(context::Context* c, context::UserContext* u, OutputChannel& out, Valuation valuation)
-  : Theory(THEORY_BV, c, u, out, valuation), 
-    d_eqEngine(*this, c, "theory::bv::EqualityEngine"), 
-    d_sliceManager(*this, c), 
-    d_context(c),
-    d_assertions(c), 
-    d_disequalities(c)
-  {
-    d_true = utils::mkTrue();
-  }
-
-  BvEqualityEngine& getEqualityEngine() {
-    return d_eqEngine;
-  }
+  TheoryBV(context::Context* c, context::UserContext* u, OutputChannel& out, Valuation valuation);
+  ~TheoryBV(); 
 
   void preRegisterTerm(TNode n);
 
@@ -150,6 +73,21 @@ public:
   Node getValue(TNode n);
 
   std::string identify() const { return std::string("TheoryBV"); }
+
+  //Node preprocessTerm(TNode term);
+  PPAssertStatus ppAssert(TNode in, SubstitutionMap& outSubstitutions); 
+private:
+  
+  class Statistics {
+  public:
+    AverageStat d_avgConflictSize;
+    IntStat     d_solveSubstitutions; 
+    Statistics();
+    ~Statistics(); 
+  }; 
+  
+  Statistics d_statistics;
+  
 };/* class TheoryBV */
 
 }/* CVC4::theory::bv namespace */
diff --git a/src/theory/bv/theory_bv_rewrite_rules.h b/src/theory/bv/theory_bv_rewrite_rules.h
index 32bbf973f..2e2347d3c 100644
--- a/src/theory/bv/theory_bv_rewrite_rules.h
+++ b/src/theory/bv/theory_bv_rewrite_rules.h
@@ -31,6 +31,7 @@ namespace theory {
 namespace bv {
 
 enum RewriteRuleId {
+  /// core rewrite rules
   EmptyRule,
   ConcatFlatten,
   ConcatExtractMerge,
@@ -42,7 +43,24 @@ enum RewriteRuleId {
   FailEq,
   SimplifyEq,
   ReflexivityEq,
-};
+  /// operator elimination rules
+  UgtToUlt,
+  UgeToUle,
+  SgeToSle,
+  SgtToSlt,
+  RepeatEliminate,
+  RotateLeftEliminate,
+  RotateRightEliminate,
+  NandEliminate,
+  NorEliminate,
+  SdivEliminate,
+  UdivEliminate,
+  SmodEliminate,
+  SremEliminate,
+  ZeroExtendEliminate,
+  // division by zero guards: rewrite a / b as b!=0 => a/b = ...
+  DivZeroGuard
+ };
 
 inline std::ostream& operator << (std::ostream& out, RewriteRuleId ruleId) {
   switch (ruleId) {
@@ -57,6 +75,20 @@ inline std::ostream& operator << (std::ostream& out, RewriteRuleId ruleId) {
   case FailEq:              out << "FailEq";              return out;
   case SimplifyEq:          out << "SimplifyEq";          return out;
   case ReflexivityEq:       out << "ReflexivityEq";       return out;
+  case UgtToUlt:            out << "UgtToUlt";            return out;
+  case SgtToSlt:            out << "SgtToSlt";            return out;
+  case UgeToUle:            out << "UgeToUle";            return out;
+  case SgeToSle:            out << "SgeToSle";            return out;
+  case RepeatEliminate:     out << "RepeatEliminate";     return out;
+  case RotateLeftEliminate: out << "RotateLeftEliminate"; return out;
+  case RotateRightEliminate:out << "RotateRightEliminate";return out;
+  case NandEliminate:       out << "NandEliminate";       return out;
+  case NorEliminate :       out << "NorEliminate";        return out;
+  case SdivEliminate :      out << "SdivEliminate";       return out;
+  case SremEliminate :      out << "SremEliminate";       return out;
+  case SmodEliminate :      out << "SmodEliminate";       return out;
+  case ZeroExtendEliminate :out << "ZeroExtendEliminate";       return out;
+  case DivZeroGuard :       out << "DivZeroGuard";        return out;
   default:
     Unreachable();
   }
@@ -147,6 +179,7 @@ typename RewriteRule<rule>::RuleStatistics* RewriteRule<rule>::s_statistics = NU
 
 /** Have to list all the rewrite rules to get the statistics out */
 struct AllRewriteRules {
+  
   RewriteRule<EmptyRule>            rule00;
   RewriteRule<ConcatFlatten>        rule01;
   RewriteRule<ConcatExtractMerge>   rule02;
@@ -158,6 +191,20 @@ struct AllRewriteRules {
   RewriteRule<FailEq>               rule08;
   RewriteRule<SimplifyEq>           rule09;
   RewriteRule<ReflexivityEq>        rule10;
+  RewriteRule<UgtToUlt>             rule11;
+  RewriteRule<SgtToSlt>             rule12;
+  RewriteRule<UgeToUle>             rule13;
+  RewriteRule<SgeToSle>             rule14;
+  RewriteRule<RepeatEliminate>      rule17;
+  RewriteRule<RotateLeftEliminate>  rule18;
+  RewriteRule<RotateRightEliminate> rule19;
+  RewriteRule<NandEliminate>        rule20;
+  RewriteRule<NorEliminate>         rule21;
+  RewriteRule<SdivEliminate>        rule22;
+  RewriteRule<SremEliminate>        rule23;
+  RewriteRule<SmodEliminate>        rule24;
+  RewriteRule<DivZeroGuard>         rule25;
+
 };
 
 template<>
@@ -202,7 +249,7 @@ struct ApplyRuleToChildren {
 
 template <
   typename R1,
-  typename R2,
+  typename R2 = RewriteRule<EmptyRule>,
   typename R3 = RewriteRule<EmptyRule>,
   typename R4 = RewriteRule<EmptyRule>,
   typename R5 = RewriteRule<EmptyRule>,
diff --git a/src/theory/bv/theory_bv_rewrite_rules_arith.h b/src/theory/bv/theory_bv_rewrite_rules_arith.h
new file mode 100644
index 000000000..08a571db3
--- /dev/null
+++ b/src/theory/bv/theory_bv_rewrite_rules_arith.h
@@ -0,0 +1,321 @@
+/*********************                                                        */
+/*! \file theory_bv_rewrite_rules_core.h
+ ** \verbatim
+ ** Original author: dejan
+ ** Major contributors: none
+ ** Minor contributors (to current version): mdeters
+ ** This file is part of the CVC4 prototype.
+ ** Copyright (c) 2009, 2010, 2011  The Analysis of Computer Systems Group (ACSys)
+ ** Courant Institute of Mathematical Sciences
+ ** New York University
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.\endverbatim
+ **
+ ** \brief [[ Add one-line brief description here ]]
+ **
+ ** [[ Add lengthier description here ]]
+ ** \todo document this file
+ **/
+
+#include "cvc4_private.h"
+
+#pragma once
+
+#include "theory/bv/theory_bv_rewrite_rules.h"
+#include "theory/bv/theory_bv_utils.h"
+
+namespace CVC4 {
+namespace theory {
+namespace bv {
+
+template<>
+bool RewriteRule<UgtToUlt>::applies(Node node) {
+  return (node.getKind() == kind::BITVECTOR_UGT);
+}
+
+template<>
+Node RewriteRule<UgtToUlt>::apply(Node node) {
+  BVDebug("bv-rewrite") << "RewriteRule<UgtToUlt>(" << node << ")" << std::endl;
+  TNode a = node[0];
+  TNode b = node[1];
+  Node result = utils::mkNode(kind::BITVECTOR_ULT, b, a);
+  return result;
+}
+
+
+template<>
+bool RewriteRule<UgeToUle>::applies(Node node) {
+  return (node.getKind() == kind::BITVECTOR_UGE);
+}
+
+template<>
+Node RewriteRule<UgeToUle>::apply(Node node) {
+  BVDebug("bv-rewrite") << "RewriteRule<UgeToUle>(" << node << ")" << std::endl;
+  TNode a = node[0];
+  TNode b = node[1];
+  Node result = utils::mkNode(kind::BITVECTOR_ULE, b, a);
+  return result;
+}
+
+
+template<>
+bool RewriteRule<SgtToSlt>::applies(Node node) {
+  return (node.getKind() == kind::BITVECTOR_SGT);
+}
+
+template<>
+Node RewriteRule<SgtToSlt>::apply(Node node) {
+  BVDebug("bv-rewrite") << "RewriteRule<UgtToUlt>(" << node << ")" << std::endl;
+  TNode a = node[0];
+  TNode b = node[1];
+  Node result = utils::mkNode(kind::BITVECTOR_SLT, b, a);
+  return result;
+}
+
+
+template<>
+bool RewriteRule<SgeToSle>::applies(Node node) {
+  return (node.getKind() == kind::BITVECTOR_SGE);
+}
+
+template<>
+Node RewriteRule<SgeToSle>::apply(Node node) {
+  BVDebug("bv-rewrite") << "RewriteRule<SgeToSle>(" << node << ")" << std::endl;
+  TNode a = node[0];
+  TNode b = node[1];
+  Node result = utils::mkNode(kind::BITVECTOR_SLE, b, a);
+  return result;
+}
+
+template<>
+bool RewriteRule<RepeatEliminate>::applies(Node node) {
+  return (node.getKind() == kind::BITVECTOR_REPEAT);
+}
+
+template<>
+Node RewriteRule<RepeatEliminate>::apply(Node node) {
+  BVDebug("bv-rewrite") << "RewriteRule<RepeatEliminate>(" << node << ")" << std::endl;
+  TNode a = node[0];
+  unsigned amount = node.getOperator().getConst<BitVectorRepeat>().repeatAmount;
+  Assert(amount >= 1);
+  if(amount == 1) {
+    return a; 
+  }
+  NodeBuilder<> result(kind::BITVECTOR_CONCAT);
+  for(unsigned i = 0; i < amount; ++i) {
+    result << node[0]; 
+  }
+  Node resultNode = result; 
+  return resultNode;
+}
+
+template<>
+bool RewriteRule<RotateLeftEliminate>::applies(Node node) {
+  return (node.getKind() == kind::BITVECTOR_ROTATE_LEFT);
+}
+
+template<>
+Node RewriteRule<RotateLeftEliminate>::apply(Node node) {
+  BVDebug("bv-rewrite") << "RewriteRule<RotateLeftEliminate>(" << node << ")" << std::endl;
+  TNode a = node[0];
+  unsigned amount = node.getOperator().getConst<BitVectorRotateLeft>().rotateLeftAmount;
+  amount = amount % utils::getSize(a); 
+  if (amount == 0) {
+    return a; 
+  }
+
+  Node left   = utils::mkExtract(a, utils::getSize(a)-1 - amount, 0);
+  Node right  = utils::mkExtract(a, utils::getSize(a) -1, utils::getSize(a) - amount);
+  Node result = utils::mkConcat(left, right);
+
+  return result;
+}
+
+template<>
+bool RewriteRule<RotateRightEliminate>::applies(Node node) {
+  return (node.getKind() == kind::BITVECTOR_ROTATE_RIGHT);
+}
+
+template<>
+Node RewriteRule<RotateRightEliminate>::apply(Node node) {
+  BVDebug("bv-rewrite") << "RewriteRule<RotateRightEliminate>(" << node << ")" << std::endl;
+  TNode a = node[0];
+  unsigned amount = node.getOperator().getConst<BitVectorRotateRight>().rotateRightAmount;
+  amount = amount % utils::getSize(a); 
+  if (amount == 0) {
+    return a; 
+  }
+  
+  Node left  = utils::mkExtract(a, amount - 1, 0);
+  Node right = utils::mkExtract(a, utils::getSize(a)-1, amount);
+  Node result = utils::mkConcat(left, right);
+
+  return result;
+}
+
+template<>
+bool RewriteRule<NandEliminate>::applies(Node node) {
+  return (node.getKind() == kind::BITVECTOR_NAND);
+}
+
+template<>
+Node RewriteRule<NandEliminate>::apply(Node node) {
+  BVDebug("bv-rewrite") << "RewriteRule<NandEliminate>(" << node << ")" << std::endl;
+  TNode a = node[0];
+  TNode b = node[1]; 
+  Node andNode = utils::mkNode(kind::BITVECTOR_AND, a, b);
+  Node result = utils::mkNode(kind::BITVECTOR_NOT, andNode); 
+  return result;
+}
+
+template<>
+bool RewriteRule<NorEliminate>::applies(Node node) {
+  return (node.getKind() == kind::BITVECTOR_NOR);
+}
+
+template<>
+Node RewriteRule<NorEliminate>::apply(Node node) {
+  BVDebug("bv-rewrite") << "RewriteRule<NorEliminate>(" << node << ")" << std::endl;
+  TNode a = node[0];
+  TNode b = node[1]; 
+  Node orNode = utils::mkNode(kind::BITVECTOR_OR, a, b);
+  Node result = utils::mkNode(kind::BITVECTOR_NOT, orNode); 
+  return result;
+}
+
+template<>
+bool RewriteRule<SdivEliminate>::applies(Node node) {
+  return (node.getKind() == kind::BITVECTOR_SDIV);
+}
+
+template<>
+Node RewriteRule<SdivEliminate>::apply(Node node) {
+  BVDebug("bv-rewrite") << "RewriteRule<SdivEliminate>(" << node << ")" << std::endl;
+
+  TNode a = node[0];
+  TNode b = node[1];
+  unsigned size = utils::getSize(a);
+  
+  Node one     = utils::mkConst(1, 1);
+  Node a_lt_0  = utils::mkNode(kind::EQUAL, utils::mkExtract(a, size-1, size-1), one);
+  Node b_lt_0  = utils::mkNode(kind::EQUAL, utils::mkExtract(b, size-1, size-1), one); 
+  Node abs_a   = utils::mkNode(kind::ITE, a_lt_0, utils::mkNode(kind::BITVECTOR_NEG, a), a);
+  Node abs_b   = utils::mkNode(kind::ITE, b_lt_0, utils::mkNode(kind::BITVECTOR_NEG, b), b);
+
+  Node a_udiv_b   = utils::mkNode(kind::BITVECTOR_UDIV, abs_a, abs_b);
+  Node neg_result = utils::mkNode(kind::BITVECTOR_NEG, a_udiv_b);
+  
+  Node condition = utils::mkNode(kind::XOR, a_lt_0, b_lt_0);
+  Node result    = utils::mkNode(kind::ITE, condition, neg_result, a_udiv_b);
+  
+  return result;
+}
+
+
+template<>
+bool RewriteRule<SremEliminate>::applies(Node node) {
+  return (node.getKind() == kind::BITVECTOR_SREM);
+}
+
+template<>
+Node RewriteRule<SremEliminate>::apply(Node node) {
+  BVDebug("bv-rewrite") << "RewriteRule<SremEliminate>(" << node << ")" << std::endl;
+  TNode a = node[0];
+  TNode b = node[1];
+  unsigned size = utils::getSize(a);
+  
+  Node one     = utils::mkConst(1, 1);
+  Node a_lt_0  = utils::mkNode(kind::EQUAL, utils::mkExtract(a, size-1, size-1), one);
+  Node b_lt_0  = utils::mkNode(kind::EQUAL, utils::mkExtract(b, size-1, size-1), one); 
+  Node abs_a   = utils::mkNode(kind::ITE, a_lt_0, utils::mkNode(kind::BITVECTOR_NEG, a), a);
+  Node abs_b   = utils::mkNode(kind::ITE, b_lt_0, utils::mkNode(kind::BITVECTOR_NEG, b), b);
+
+  Node a_urem_b   = utils::mkNode(kind::BITVECTOR_UREM, abs_a, abs_b);
+  Node neg_result = utils::mkNode(kind::BITVECTOR_NEG, a_urem_b);
+  
+  Node result    = utils::mkNode(kind::ITE, a_lt_0, neg_result, a_urem_b);
+
+  return result;
+}
+
+template<>
+bool RewriteRule<SmodEliminate>::applies(Node node) {
+  return (node.getKind() == kind::BITVECTOR_SMOD);
+}
+
+template<>
+Node RewriteRule<SmodEliminate>::apply(Node node) {
+  BVDebug("bv-rewrite") << "RewriteRule<SmodEliminate>(" << node << ")" << std::endl;
+  TNode a = node[0];
+  TNode b = node[1];
+  unsigned size = utils::getSize(a);
+  
+  Node one     = utils::mkConst(1, 1);
+  Node zero    = utils::mkConst(1, 0);
+  Node a_lt_0  = utils::mkNode(kind::EQUAL, utils::mkExtract(a, size-1, size-1), one);
+  Node b_lt_0  = utils::mkNode(kind::EQUAL, utils::mkExtract(b, size-1, size-1), one);
+  
+  Node a_gte_0  = utils::mkNode(kind::EQUAL, utils::mkExtract(a, size-1, size-1), zero);
+  Node b_gte_0  = utils::mkNode(kind::EQUAL, utils::mkExtract(b, size-1, size-1), zero); 
+
+  Node abs_a   = utils::mkNode(kind::ITE, a_lt_0, utils::mkNode(kind::BITVECTOR_NEG, a), a);
+  Node abs_b   = utils::mkNode(kind::ITE, b_lt_0, utils::mkNode(kind::BITVECTOR_NEG, b), b);
+
+  Node a_urem_b   = utils::mkNode(kind::BITVECTOR_UREM, abs_a, abs_b);
+  Node neg_rem = utils::mkNode(kind::BITVECTOR_NEG, a_urem_b);
+
+  
+  Node aneg_bpos = utils::mkNode(kind::AND, a_lt_0, b_gte_0);
+  Node apos_bneg = utils::mkNode(kind::AND, a_gte_0, b_lt_0);
+  Node aneg_bneg = utils::mkNode(kind::AND, a_lt_0, b_lt_0);
+                                 
+  Node result = utils::mkNode(kind::ITE, aneg_bpos, utils::mkNode(kind::BITVECTOR_PLUS, neg_rem, b), 
+                              utils::mkNode(kind::ITE, apos_bneg, utils::mkNode(kind::BITVECTOR_PLUS, a_urem_b, b),
+                                            utils::mkNode(kind::ITE, aneg_bneg, neg_rem,
+                                                             a_urem_b)));
+  return result;
+}
+
+
+template<>
+bool RewriteRule<ZeroExtendEliminate>::applies(Node node) {
+  return (node.getKind() == kind::BITVECTOR_ZERO_EXTEND); 
+}
+
+template<>
+Node RewriteRule<ZeroExtendEliminate>::apply(Node node) {
+  BVDebug("bv-rewrite") << "RewriteRule<ZeroExtendEliminate>(" << node << ")" << std::endl;
+
+  TNode bv = node[0];
+  unsigned amount = node.getOperator().getConst<BitVectorZeroExtend>().zeroExtendAmount;
+
+  Node zero = utils::mkConst(amount, 0);
+  Node result = utils::mkConcat(zero, node[0]); 
+
+  return result;
+}
+
+
+template<>
+bool RewriteRule<DivZeroGuard>::applies(Node node) {
+  return (node.getKind() == kind::BITVECTOR_UDIV ||
+          node.getKind() == kind::BITVECTOR_UREM ||
+          node.getKind() == kind::BITVECTOR_SDIV ||
+          node.getKind() == kind::BITVECTOR_SREM ||
+          node.getKind() == kind::BITVECTOR_SMOD);
+}
+
+template<>
+Node RewriteRule<DivZeroGuard>::apply(Node node) {
+  BVDebug("bv-rewrite") << "RewriteRule<DivZeroGuard>(" << node << ")" << std::endl;
+
+  Unimplemented();
+  
+}
+
+
+
+
+}
+}
+}
diff --git a/src/theory/bv/theory_bv_rewriter.cpp b/src/theory/bv/theory_bv_rewriter.cpp
index 566bf3a68..2f3538837 100644
--- a/src/theory/bv/theory_bv_rewriter.cpp
+++ b/src/theory/bv/theory_bv_rewriter.cpp
@@ -21,17 +21,17 @@
 #include "theory/bv/theory_bv_rewriter.h"
 #include "theory/bv/theory_bv_rewrite_rules.h"
 #include "theory/bv/theory_bv_rewrite_rules_core.h"
+#include "theory/bv/theory_bv_rewrite_rules_arith.h"
 
 using namespace CVC4;
 using namespace CVC4::theory;
 using namespace CVC4::theory::bv;
 
 RewriteResponse TheoryBVRewriter::postRewrite(TNode node) {
-
+  
   BVDebug("bitvector") << "TheoryBV::postRewrite(" << node << ")" << std::endl;
-
-  Node result;
-
+    
+  Node result = node;
   if (node.getKind() == kind::CONST_BITVECTOR || (node.getKind() != kind::EQUAL && Theory::isLeafOf(node, THEORY_BV))) {
     result = node;
   } else {
@@ -67,10 +67,78 @@ RewriteResponse TheoryBVRewriter::postRewrite(TNode node) {
                   RewriteRule<FailEq>,
                   // If both sides are equal equality is true
                   RewriteRule<SimplifyEq>,
-                  // Normalize the equalities
+                  // Eliminate the equalities
                   RewriteRule<ReflexivityEq>
                 >::apply(node);
       break;
+    case kind::BITVECTOR_UGT:
+      result = LinearRewriteStrategy <
+                  RewriteRule<UgtToUlt>
+               >::apply(node);
+      break;
+
+    case kind::BITVECTOR_UGE:
+      result = LinearRewriteStrategy <
+                  RewriteRule<UgeToUle>
+               >::apply(node);
+      break;
+    case kind::BITVECTOR_SGT:
+      result = LinearRewriteStrategy <
+                  RewriteRule<SgtToSlt>
+               >::apply(node);
+      break;
+    case kind::BITVECTOR_SGE:
+      result = LinearRewriteStrategy <
+                  RewriteRule<SgeToSle>
+               >::apply(node);
+      break;
+    case kind::BITVECTOR_REPEAT:
+      result = LinearRewriteStrategy <
+                  RewriteRule<RepeatEliminate>
+               >::apply(node);
+      break;
+    case kind::BITVECTOR_ROTATE_RIGHT:
+      result = LinearRewriteStrategy <
+                  RewriteRule<RotateRightEliminate>
+               >::apply(node);
+      break;
+    case kind::BITVECTOR_ROTATE_LEFT:
+      result = LinearRewriteStrategy <
+                  RewriteRule<RotateLeftEliminate>
+               >::apply(node);
+      break;
+    case kind::BITVECTOR_NAND:
+      result = LinearRewriteStrategy <
+                  RewriteRule<NandEliminate>
+               >::apply(node);
+      break;
+    case kind::BITVECTOR_NOR:
+      result = LinearRewriteStrategy <
+                  RewriteRule<NorEliminate>
+               >::apply(node);
+      break;
+
+    case kind::BITVECTOR_SDIV:
+      result = LinearRewriteStrategy <
+                  RewriteRule<SdivEliminate>
+               >::apply(node);
+      break;
+  case kind::BITVECTOR_SREM:
+      result = LinearRewriteStrategy <
+                  RewriteRule<SremEliminate>
+               >::apply(node);
+     break;
+    case kind::BITVECTOR_SMOD:
+      result = LinearRewriteStrategy <
+                  RewriteRule<SmodEliminate>
+                >::apply(node);
+      break;
+    case kind::BITVECTOR_ZERO_EXTEND:
+      result = LinearRewriteStrategy <
+                  RewriteRule<ZeroExtendEliminate>
+                >::apply(node);
+      break;
+      
     default:
       // TODO: figure out when this is an operator
       result = node;
diff --git a/src/theory/bv/theory_bv_rewriter.h b/src/theory/bv/theory_bv_rewriter.h
index f0eb621ca..1893977a8 100644
--- a/src/theory/bv/theory_bv_rewriter.h
+++ b/src/theory/bv/theory_bv_rewriter.h
@@ -39,7 +39,7 @@ public:
   static RewriteResponse postRewrite(TNode node);
 
   static inline RewriteResponse preRewrite(TNode node) {
-    return RewriteResponse(REWRITE_DONE, node);
+    return postRewrite(node);
   }
 
   static inline Node rewriteEquality(TNode node) {
diff --git a/src/theory/bv/theory_bv_type_rules.h b/src/theory/bv/theory_bv_type_rules.h
index 192295bc0..91b3a0e5d 100644
--- a/src/theory/bv/theory_bv_type_rules.h
+++ b/src/theory/bv/theory_bv_type_rules.h
@@ -35,6 +35,28 @@ public:
   }
 };
 
+
+class BitVectorBitOfTypeRule {
+public:
+  inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
+    throw (TypeCheckingExceptionPrivate) {
+    
+    if(check) {
+      BitVectorBitOf info = n.getOperator().getConst<BitVectorBitOf>();
+      TypeNode t = n[0].getType(check);
+      
+      if (!t.isBitVector()) {
+        throw TypeCheckingExceptionPrivate(n, "expecting bit-vector term");
+      }
+      if (info.bitIndex >= t.getBitVectorSize()) {
+        throw TypeCheckingExceptionPrivate(n, "extract index is larger than the bitvector size");
+      }
+    }
+    return nodeManager->booleanType(); 
+  }
+};
+
+
 class BitVectorCompRule {
 public:
   inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
diff --git a/src/theory/bv/theory_bv_utils.h b/src/theory/bv/theory_bv_utils.h
index 80c5ca7f7..6bd7368c9 100644
--- a/src/theory/bv/theory_bv_utils.h
+++ b/src/theory/bv/theory_bv_utils.h
@@ -49,6 +49,13 @@ inline unsigned getSize(TNode node) {
   return node.getType().getBitVectorSize();
 }
 
+// this seems to behave strangely
+inline const Integer& getBit(TNode node, unsigned i) {
+  Assert (0); 
+  Assert (node.getKind() == kind::CONST_BITVECTOR);
+  return node.getConst<BitVector>().extract(i, i).getValue();
+}
+
 inline Node mkTrue() {
   return NodeManager::currentNM()->mkConst<bool>(true);
 }
@@ -57,6 +64,11 @@ inline Node mkFalse() {
   return NodeManager::currentNM()->mkConst<bool>(false);
 }
 
+inline Node mkVar(unsigned size) {
+  NodeManager* nm =  NodeManager::currentNM();
+  return nm->mkVar(nm->mkBitVectorType(size)); 
+}
+
 inline Node mkAnd(std::vector<TNode>& children) {
   if (children.size() > 1) {
     return NodeManager::currentNM()->mkNode(kind::AND, children);
@@ -65,8 +77,43 @@ inline Node mkAnd(std::vector<TNode>& children) {
   }
 }
 
+
+inline Node mkNode(Kind kind, TNode child) {
+  return NodeManager::currentNM()->mkNode(kind, child);
+}
+
+inline Node mkNode(Kind kind, TNode child1, TNode child2) {
+  return NodeManager::currentNM()->mkNode(kind, child1, child2);
+}
+
+inline Node mkNode(Kind kind, TNode child1, TNode child2, TNode child3) {
+  return NodeManager::currentNM()->mkNode(kind, child1, child2, child3);
+}
+
+
+inline Node mkNot(Node child) {
+  return NodeManager::currentNM()->mkNode(kind::NOT, child);
+}
+
+inline Node mkAnd(TNode node1, TNode node2) {
+  return NodeManager::currentNM()->mkNode(kind::AND, node1, node2);
+}
+
+inline Node mkOr(TNode node1, TNode node2) {
+  return NodeManager::currentNM()->mkNode(kind::OR, node1, node2);
+}
+
+inline Node mkXor(TNode node1, TNode node2) {
+  return NodeManager::currentNM()->mkNode(kind::XOR, node1, node2);
+}
+
+
 inline Node mkAnd(std::vector<Node>& children) {
-  return NodeManager::currentNM()->mkNode(kind::AND, children);
+  if(children.size() > 1) {
+    return NodeManager::currentNM()->mkNode(kind::AND, children);
+  } else {
+    return children[0];
+  }
 }
 
 inline Node mkExtract(TNode node, unsigned high, unsigned low) {
@@ -76,6 +123,12 @@ inline Node mkExtract(TNode node, unsigned high, unsigned low) {
   return NodeManager::currentNM()->mkNode(extractOp, children);
 }
 
+inline Node mkBitOf(TNode node, unsigned index) {
+  Node bitOfOp = NodeManager::currentNM()->mkConst<BitVectorBitOf>(BitVectorBitOf(index));
+  return NodeManager::currentNM()->mkNode(bitOfOp, node); 
+                                        
+}
+
 inline Node mkConcat(std::vector<Node>& children) {
   if (children.size() > 1)
     return NodeManager::currentNM()->mkNode(kind::BITVECTOR_CONCAT, children);
@@ -88,6 +141,11 @@ inline Node mkConcat(TNode t1, TNode t2) {
 }
 
 
+inline Node mkConst(unsigned size, unsigned int value) {
+  BitVector val(size, value);
+  return NodeManager::currentNM()->mkConst<BitVector>(val); 
+}
+
 inline Node mkConst(const BitVector& value) {
   return NodeManager::currentNM()->mkConst<BitVector>(value);
 }
@@ -139,6 +197,66 @@ inline Node mkConjunction(const std::set<TNode> nodes) {
   return conjunction;
 }
 
+inline bool isBVPredicate(TNode node) {
+  if (node.getKind() == kind::EQUAL ||
+      node.getKind() == kind::BITVECTOR_ULT ||
+      node.getKind() == kind::BITVECTOR_SLT ||
+      node.getKind() == kind::BITVECTOR_UGT ||
+      node.getKind() == kind::BITVECTOR_UGE ||
+      node.getKind() == kind::BITVECTOR_SGT ||
+      node.getKind() == kind::BITVECTOR_SGE ||
+      node.getKind() == kind::BITVECTOR_ULE || 
+      node.getKind() == kind::BITVECTOR_SLE ||
+      ( node.getKind() == kind::NOT && (node[0].getKind() == kind::EQUAL ||
+                                        node[0].getKind() == kind::BITVECTOR_ULT ||
+                                        node[0].getKind() == kind::BITVECTOR_SLT ||
+                                        node[0].getKind() == kind::BITVECTOR_UGT ||
+                                        node[0].getKind() == kind::BITVECTOR_UGE ||
+                                        node[0].getKind() == kind::BITVECTOR_SGT ||
+                                        node[0].getKind() == kind::BITVECTOR_SGE ||
+                                        node[0].getKind() == kind::BITVECTOR_ULE || 
+                                        node[0].getKind() == kind::BITVECTOR_SLE)))
+    {
+      return true; 
+    }
+  else
+    {
+      return false; 
+    }
+}
+
+inline Node mkConjunction(const std::vector<TNode>& nodes) {
+  std::vector<TNode> expandedNodes;
+
+  std::vector<TNode>::const_iterator it = nodes.begin();
+  std::vector<TNode>::const_iterator it_end = nodes.end();
+  while (it != it_end) {
+    TNode current = *it;
+    if (current != mkTrue()) {
+      Assert(isBVPredicate(current));
+      expandedNodes.push_back(current);
+    }
+    ++ it;
+  }
+
+  Assert(expandedNodes.size() > 0);
+  if (expandedNodes.size() == 1) {
+    return *expandedNodes.begin();
+  }
+
+  NodeBuilder<> conjunction(kind::AND);
+
+  it = expandedNodes.begin();
+  it_end = expandedNodes.end();
+  while (it != it_end) {
+    conjunction << *it;
+    ++ it;
+  }
+
+  return conjunction;
+}
+
+
 // Turn a set into a string
 inline std::string setToString(const std::set<TNode>& nodeSet) {
   std::stringstream out;
diff --git a/src/theory/registrar.h b/src/theory/theory_registrar.h
index 19315827e..810ef1f67 100644
--- a/src/theory/registrar.h
+++ b/src/theory/theory_registrar.h
@@ -22,29 +22,30 @@
 
 #include "cvc4_private.h"
 
-#ifndef __CVC4__THEORY__REGISTRAR_H
-#define __CVC4__THEORY__REGISTRAR_H
+#ifndef __CVC4__THEORY__THEORY_REGISTRAR_H
+#define __CVC4__THEORY__THEORY_REGISTRAR_H
 
+#include "prop/registrar.h"
 #include "theory/theory_engine.h"
 
 namespace CVC4 {
 namespace theory {
 
-class Registrar {
+class TheoryRegistrar: public prop::Registrar {
 private:
   TheoryEngine* d_theoryEngine;
 
 public:
 
-  Registrar(TheoryEngine* te) : d_theoryEngine(te) { }
+  TheoryRegistrar(TheoryEngine* te) : d_theoryEngine(te) { }
 
   void preRegister(Node n) {
     d_theoryEngine->preRegister(n);
   }
 
-};/* class Registrar */
+};/* class TheoryRegistrar */
 
 }/* CVC4::theory namespace */
 }/* CVC4 namespace */
 
-#endif /* __CVC4__THEORY__REGISTRAR_H */
+#endif /* __CVC4__THEORY__THEORY_REGISTRAR_H */