refactored TheoryBV bitblaster and equality engine into subtheories (similar to TheoryEngine

6 files changed, 451 insertions, 270 deletions

diff --git a/src/theory/bv/Makefile.am b/src/theory/bv/Makefile.am
index 3bb7e3056..8f524c8fc 100644
--- a/src/theory/bv/Makefile.am
+++ b/src/theory/bv/Makefile.am
@@ -11,6 +11,8 @@ libbv_la_SOURCES = \
 	theory_bv_utils.h \
 	bitblaster.h \
 	bitblaster.cpp \
+	bv_subtheory.h \
+	bv_subtheory.cpp \
 	bitblast_strategies.h \
 	bitblast_strategies.cpp \
 	theory_bv.h \
diff --git a/src/theory/bv/bitblaster.cpp b/src/theory/bv/bitblaster.cpp
index 60fc8f9c1..6b59b9b00 100644
--- a/src/theory/bv/bitblaster.cpp
+++ b/src/theory/bv/bitblaster.cpp
@@ -350,7 +350,7 @@ Bitblaster::Statistics::~Statistics() {
 }
 
 bool Bitblaster::MinisatNotify::notify(prop::SatLiteral lit) {
-  return d_bv->storePropagation(d_cnf->getNode(lit), TheoryBV::SUB_BITBLASTER);
+  return d_bv->storePropagation(d_cnf->getNode(lit), TheoryBV::SUB_BITBLAST);
 };
 
 void Bitblaster::MinisatNotify::notify(prop::SatClause& clause) {
diff --git a/src/theory/bv/bv_subtheory.cpp b/src/theory/bv/bv_subtheory.cpp
new file mode 100644
index 000000000..f55d231b2
--- /dev/null
+++ b/src/theory/bv/bv_subtheory.cpp
@@ -0,0 +1,247 @@
+/*********************                                                        */
+/*! \file bv_subtheory.cpp
+ ** \verbatim
+ ** Original author: lianah
+ ** Major contributors: 
+ ** 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/bv_subtheory.h"
+#include "theory/bv/theory_bv.h"
+#include "theory/bv/theory_bv_utils.h"
+#include "theory/bv/bitblaster.h"
+
+
+using namespace CVC4;
+using namespace CVC4::theory;
+using namespace CVC4::theory::bv;
+using namespace CVC4::context;
+
+using namespace std;
+using namespace CVC4::theory::bv::utils;
+
+
+BitblastSolver::BitblastSolver(context::Context* c, TheoryBV* bv)
+  : SubtheorySolver(c, bv), 
+    d_bitblaster(new Bitblaster(c, bv)),
+    d_bitblastQueue(c)
+{}
+
+BitblastSolver::~BitblastSolver() {
+  delete d_bitblaster; 
+}
+
+void BitblastSolver::preRegister(TNode node) {
+  if ((node.getKind() == kind::EQUAL ||
+       node.getKind() == kind::BITVECTOR_ULT ||
+       node.getKind() == kind::BITVECTOR_ULE ||
+       node.getKind() == kind::BITVECTOR_SLT ||
+       node.getKind() == kind::BITVECTOR_SLE) &&
+      !d_bitblaster->hasBBAtom(node)) {
+    d_bitblastQueue.push_back(node); 
+  }
+}
+
+void BitblastSolver::explain(TNode literal, std::vector<TNode>& assumptions) {
+  d_bitblaster->explain(literal, assumptions); 
+}
+
+bool BitblastSolver::addAssertions(const std::vector<TNode>& assertions, Theory::Effort e) {
+  BVDebug("bitvector::bitblaster") << "BitblastSolver::addAssertions (" << e << ")" << std::endl;
+
+  //// Eager bit-blasting
+  if (Options::current()->bitvectorEagerBitblast) {
+    for (unsigned i = 0; i < assertions.size(); ++i) {
+      TNode atom = assertions[i].getKind() == kind::NOT ? assertions[i][0] : assertions[i];
+      if (atom.getKind() != kind::BITVECTOR_BITOF) {
+        d_bitblaster->bbAtom(atom);
+      }
+    }
+    return true; 
+  }
+
+  //// Lazy bit-blasting
+    
+  // bit-blast enqueued nodes
+  while (!d_bitblastQueue.empty()) {
+    TNode atom = d_bitblastQueue.front();
+    d_bitblaster->bbAtom(atom);
+    d_bitblastQueue.pop(); 
+  }
+
+  // propagation
+  for (unsigned i = 0; i < assertions.size(); ++i) {
+    TNode fact = assertions[i];
+    if (!d_bv->inConflict() && !d_bv->propagatedBy(fact, TheoryBV::SUB_BITBLAST)) {
+      // Some atoms have not been bit-blasted yet
+      d_bitblaster->bbAtom(fact);
+      // Assert to sat
+      bool ok = d_bitblaster->assertToSat(fact, d_useSatPropagation);
+      if (!ok) {
+        std::vector<TNode> conflictAtoms;
+        d_bitblaster->getConflict(conflictAtoms);
+        d_bv->setConflict(mkConjunction(conflictAtoms)); 
+        return false; 
+      }
+    }
+  }
+
+  // solving
+  if (e == Theory::EFFORT_FULL || Options::current()->bitvectorEagerFullcheck) {
+    Assert(!d_bv->inConflict());
+    BVDebug("bitvector::bitblaster") << "BitblastSolver::addAssertions solving. \n"; 
+    bool ok = d_bitblaster->solve();
+    if (!ok) {
+      std::vector<TNode> conflictAtoms;
+      d_bitblaster->getConflict(conflictAtoms);
+      Node conflict = mkConjunction(conflictAtoms);
+      d_bv->setConflict(conflict); 
+      return false; 
+    }
+  }
+
+  return true; 
+}
+
+EqualitySolver::EqualitySolver(context::Context* c, TheoryBV* bv)
+  : SubtheorySolver(c, bv),
+    d_notify(bv),
+    d_equalityEngine(d_notify, c, "theory::bv::TheoryBV")
+{
+  if (d_useEqualityEngine) {
+
+    // The kinds we are treating as function application in congruence
+    d_equalityEngine.addFunctionKind(kind::BITVECTOR_CONCAT);
+    //    d_equalityEngine.addFunctionKind(kind::BITVECTOR_AND);
+    //    d_equalityEngine.addFunctionKind(kind::BITVECTOR_OR);
+    //    d_equalityEngine.addFunctionKind(kind::BITVECTOR_XOR);
+    //    d_equalityEngine.addFunctionKind(kind::BITVECTOR_NOT);
+    //    d_equalityEngine.addFunctionKind(kind::BITVECTOR_NAND);
+    //    d_equalityEngine.addFunctionKind(kind::BITVECTOR_NOR);
+    //    d_equalityEngine.addFunctionKind(kind::BITVECTOR_XNOR);
+    //    d_equalityEngine.addFunctionKind(kind::BITVECTOR_COMP);
+    d_equalityEngine.addFunctionKind(kind::BITVECTOR_MULT);
+    d_equalityEngine.addFunctionKind(kind::BITVECTOR_PLUS);
+    //    d_equalityEngine.addFunctionKind(kind::BITVECTOR_SUB);
+    //    d_equalityEngine.addFunctionKind(kind::BITVECTOR_NEG);
+    //    d_equalityEngine.addFunctionKind(kind::BITVECTOR_UDIV);
+    //    d_equalityEngine.addFunctionKind(kind::BITVECTOR_UREM);
+    //    d_equalityEngine.addFunctionKind(kind::BITVECTOR_SDIV);
+    //    d_equalityEngine.addFunctionKind(kind::BITVECTOR_SREM);
+    //    d_equalityEngine.addFunctionKind(kind::BITVECTOR_SMOD);
+    //    d_equalityEngine.addFunctionKind(kind::BITVECTOR_SHL);
+    //    d_equalityEngine.addFunctionKind(kind::BITVECTOR_LSHR);
+    //    d_equalityEngine.addFunctionKind(kind::BITVECTOR_ASHR);
+    //    d_equalityEngine.addFunctionKind(kind::BITVECTOR_ULT);
+    //    d_equalityEngine.addFunctionKind(kind::BITVECTOR_ULE);
+    //    d_equalityEngine.addFunctionKind(kind::BITVECTOR_UGT);
+    //    d_equalityEngine.addFunctionKind(kind::BITVECTOR_UGE);
+    //    d_equalityEngine.addFunctionKind(kind::BITVECTOR_SLT);
+    //    d_equalityEngine.addFunctionKind(kind::BITVECTOR_SLE);
+    //    d_equalityEngine.addFunctionKind(kind::BITVECTOR_SGT);
+    //    d_equalityEngine.addFunctionKind(kind::BITVECTOR_SGE);
+  }
+}
+
+void EqualitySolver::preRegister(TNode node) {
+  if (!d_useEqualityEngine)
+    return;
+
+  if (node.getKind() == kind::EQUAL) {
+      d_equalityEngine.addTriggerEquality(node);
+  } else {
+    d_equalityEngine.addTerm(node);
+  }
+}
+
+void EqualitySolver::explain(TNode literal, std::vector<TNode>& assumptions) {
+  bool polarity = literal.getKind() != kind::NOT;
+  TNode atom = polarity ? literal : literal[0];
+  if (atom.getKind() == kind::EQUAL) {
+    d_equalityEngine.explainEquality(atom[0], atom[1], polarity, assumptions);
+  } else {
+    d_equalityEngine.explainPredicate(atom, polarity, assumptions);
+  }
+}
+
+bool EqualitySolver::addAssertions(const std::vector<TNode>& assertions, Theory::Effort e) {
+  BVDebug("bitvector::equality") << "EqualitySolver::addAssertions \n"; 
+  Assert (!d_bv->inConflict());
+  
+  for (unsigned i = 0; i < assertions.size(); ++i) {
+    TNode fact = assertions[i];
+    
+    // Notify the equality engine
+    if (d_useEqualityEngine && !d_bv->inConflict() && !d_bv->propagatedBy(fact, TheoryBV::TheoryBV::SUB_EQUALITY) ) {
+      bool negated = fact.getKind() == kind::NOT;
+      TNode predicate = negated ? fact[0] : fact;
+      if (predicate.getKind() == kind::EQUAL) {
+        if (negated) {
+          // dis-equality
+          d_equalityEngine.assertEquality(predicate, false, fact);
+        } else {
+          // equality
+          d_equalityEngine.assertEquality(predicate, true, fact);
+        }
+      } else {
+        // Adding predicate if the congruence over it is turned on
+        if (d_equalityEngine.isFunctionKind(predicate.getKind())) {
+          d_equalityEngine.assertPredicate(predicate, !negated, fact);
+        }
+      }
+    }
+
+    // checking for a conflict 
+    if (d_bv->inConflict()) {
+      return false;
+    }
+  }
+  
+  return true; 
+}
+
+bool EqualitySolver::NotifyClass::eqNotifyTriggerEquality(TNode equality, bool value) {
+  BVDebug("bitvector::equality") << "NotifyClass::eqNotifyTriggerEquality(" << equality << ", " << (value ? "true" : "false" )<< ")" << std::endl;
+  if (value) {
+    return d_bv->storePropagation(equality, TheoryBV::SUB_EQUALITY);
+  } else {
+    return d_bv->storePropagation(equality.notNode(), TheoryBV::SUB_EQUALITY);
+  }
+}
+
+bool EqualitySolver::NotifyClass::eqNotifyTriggerPredicate(TNode predicate, bool value) {
+  BVDebug("bitvector::equality") << "NotifyClass::eqNotifyTriggerPredicate(" << predicate << ", " << (value ? "true" : "false" )<< ")" << std::endl;
+  if (value) {
+    return d_bv->storePropagation(predicate, TheoryBV::SUB_EQUALITY);
+  } else {
+    return d_bv->storePropagation(predicate.notNode(), TheoryBV::SUB_EQUALITY);
+  }
+}
+
+bool EqualitySolver::NotifyClass::eqNotifyTriggerTermEquality(TNode t1, TNode t2, bool value) {
+  Debug("bitvector::equality") << "NotifyClass::eqNotifyTriggerTermMerge(" << t1 << ", " << t2 << std::endl;
+  if (value) {
+    return d_bv->storePropagation(t1.eqNode(t2), TheoryBV::SUB_EQUALITY);
+  } else {
+    return d_bv->storePropagation(t1.eqNode(t2).notNode(), TheoryBV::SUB_EQUALITY);
+  }
+}
+
+bool EqualitySolver::NotifyClass::eqNotifyConstantTermMerge(TNode t1, TNode t2) {
+  Debug("bitvector::equality") << "NotifyClass::eqNotifyConstantTermMerge(" << t1 << ", " << t2 << std::endl;
+  if (Theory::theoryOf(t1) == THEORY_BOOL) {
+    return d_bv->storePropagation(t1.iffNode(t2), TheoryBV::SUB_EQUALITY);
+  }
+  return d_bv->storePropagation(t1.eqNode(t2), TheoryBV::SUB_EQUALITY);
+}
diff --git a/src/theory/bv/bv_subtheory.h b/src/theory/bv/bv_subtheory.h
new file mode 100644
index 000000000..cc62013fd
--- /dev/null
+++ b/src/theory/bv/bv_subtheory.h
@@ -0,0 +1,152 @@
+/*********************                                                        */
+/*! \file bv_subtheory.h
+ ** \verbatim
+ ** Original author: lianah
+ ** Major contributors: dejan
+ ** 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 Algebraic solver. 
+ **
+ ** Algebraic solver.
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef __CVC4__THEORY__BV__BV_SUBTHEORY_H
+#define __CVC4__THEORY__BV__BV_SUBTHEORY_H
+
+#include "context/context.h"
+#include "context/cdqueue.h"
+#include "theory/uf/equality_engine.h"
+#include "theory/theory.h"
+
+namespace CVC4 {
+namespace theory {
+namespace bv {
+
+const bool d_useEqualityEngine = true;
+const bool d_useSatPropagation = true;
+
+// forward declaration 
+class TheoryBV; 
+class Bitblaster;
+
+/**
+ * Abstract base class for bit-vector subtheory solvers
+ *
+ */
+class SubtheorySolver {
+
+protected:
+
+  /** The context we are using */
+  context::Context* d_context;
+
+  /** The bit-vector theory */
+  TheoryBV* d_bv;
+
+public:
+  
+  SubtheorySolver(context::Context* c, TheoryBV* bv) :
+    d_context(c),
+    d_bv(bv)
+  {}
+  virtual ~SubtheorySolver() {}
+
+  virtual bool  addAssertions(const std::vector<TNode>& assertions, Theory::Effort e) = 0;
+  virtual void  explain(TNode literal, std::vector<TNode>& assumptions) = 0;
+  virtual void  preRegister(TNode node) {}
+
+}; 
+
+
+/**
+ * BitblastSolver
+ *
+ */
+
+class BitblastSolver : public SubtheorySolver {
+
+  /** Bitblaster */
+  Bitblaster* d_bitblaster; 
+
+  /** Nodes that still need to be bit-blasted */
+  context::CDQueue<TNode> d_bitblastQueue; 
+
+public:
+  BitblastSolver(context::Context* c, TheoryBV* bv);
+  ~BitblastSolver(); 
+
+  void  preRegister(TNode node);
+  bool  addAssertions(const std::vector<TNode>& assertions, Theory::Effort e);
+  void  explain(TNode literal, std::vector<TNode>& assumptions);
+};
+
+
+/**
+ * EqualitySolver
+ *
+ */
+
+class EqualitySolver : public SubtheorySolver {
+
+  // NotifyClass: handles call-back from congruence closure module
+
+  class NotifyClass : public eq::EqualityEngineNotify {
+    TheoryBV* d_bv;
+
+  public:
+    NotifyClass(TheoryBV* bv): d_bv(bv) {}
+    bool eqNotifyTriggerEquality(TNode equality, bool value);
+    bool eqNotifyTriggerPredicate(TNode predicate, bool value);
+    bool eqNotifyTriggerTermEquality(TNode t1, TNode t2, bool value); 
+    bool eqNotifyConstantTermMerge(TNode t1, TNode t2);
+  };
+
+
+  /** The notify class for d_equalityEngine */
+  NotifyClass d_notify;
+
+  /** Equality engine */
+  eq::EqualityEngine d_equalityEngine;
+  
+public:
+
+  EqualitySolver(context::Context* c, TheoryBV* bv);
+
+  void  preRegister(TNode node);
+  bool  addAssertions(const std::vector<TNode>& assertions, Theory::Effort e);
+  void  explain(TNode literal, std::vector<TNode>& assumptions);
+  void  addSharedTerm(TNode t) {
+    d_equalityEngine.addTriggerTerm(t);
+  }
+  EqualityStatus getEqualityStatus(TNode a, TNode b) {
+    if (d_equalityEngine.areEqual(a, b)) {
+      // The terms are implied to be equal
+      return EQUALITY_TRUE;
+    }
+    if (d_equalityEngine.areDisequal(a, b)) {
+      // The terms are implied to be dis-equal
+      return EQUALITY_FALSE;
+    }
+    return EQUALITY_UNKNOWN; 
+  }
+}; 
+
+
+// class CoreSolver : public SubtheorySolver {
+  
+// }; 
+
+
+}
+}
+}
+
+#endif /* __CVC4__THEORY__BV__BV_SUBTHEORY_H */
diff --git a/src/theory/bv/theory_bv.cpp b/src/theory/bv/theory_bv.cpp
index 445b2d242..26452e5e8 100644
--- a/src/theory/bv/theory_bv.cpp
+++ b/src/theory/bv/theory_bv.cpp
@@ -31,66 +31,24 @@ using namespace std;
 using namespace CVC4::theory::bv::utils;
 
 
-const bool d_useEqualityEngine = true;
-const bool d_useSatPropagation = true;
 
 
 TheoryBV::TheoryBV(context::Context* c, context::UserContext* u, OutputChannel& out, Valuation valuation, const LogicInfo& logicInfo)
   : Theory(THEORY_BV, c, u, out, valuation, logicInfo),
     d_context(c),
-    d_assertions(c),
-    d_bitblaster(new Bitblaster(c, this) ),
-    d_bitblastQueue(c),
     d_alreadyPropagatedSet(c),
     d_sharedTermsSet(c),
+    d_bitblastSolver(c, this),
+    d_equalitySolver(c, this),
     d_statistics(),
-    d_notify(*this),
-    d_equalityEngine(d_notify, c, "theory::bv::TheoryBV"),
     d_conflict(c, false),
     d_literalsToPropagate(c),
     d_literalsToPropagateIndex(c, 0),
-    d_toBitBlast(c),
     d_propagatedBy(c)
-  {
-    if (d_useEqualityEngine) {
-
-      // The kinds we are treating as function application in congruence
-      d_equalityEngine.addFunctionKind(kind::BITVECTOR_CONCAT);
-      //    d_equalityEngine.addFunctionKind(kind::BITVECTOR_AND);
-      //    d_equalityEngine.addFunctionKind(kind::BITVECTOR_OR);
-      //    d_equalityEngine.addFunctionKind(kind::BITVECTOR_XOR);
-      //    d_equalityEngine.addFunctionKind(kind::BITVECTOR_NOT);
-      //    d_equalityEngine.addFunctionKind(kind::BITVECTOR_NAND);
-      //    d_equalityEngine.addFunctionKind(kind::BITVECTOR_NOR);
-      //    d_equalityEngine.addFunctionKind(kind::BITVECTOR_XNOR);
-      //    d_equalityEngine.addFunctionKind(kind::BITVECTOR_COMP);
-      d_equalityEngine.addFunctionKind(kind::BITVECTOR_MULT);
-      d_equalityEngine.addFunctionKind(kind::BITVECTOR_PLUS);
-      //    d_equalityEngine.addFunctionKind(kind::BITVECTOR_SUB);
-      //    d_equalityEngine.addFunctionKind(kind::BITVECTOR_NEG);
-      //    d_equalityEngine.addFunctionKind(kind::BITVECTOR_UDIV);
-      //    d_equalityEngine.addFunctionKind(kind::BITVECTOR_UREM);
-      //    d_equalityEngine.addFunctionKind(kind::BITVECTOR_SDIV);
-      //    d_equalityEngine.addFunctionKind(kind::BITVECTOR_SREM);
-      //    d_equalityEngine.addFunctionKind(kind::BITVECTOR_SMOD);
-      //    d_equalityEngine.addFunctionKind(kind::BITVECTOR_SHL);
-      //    d_equalityEngine.addFunctionKind(kind::BITVECTOR_LSHR);
-      //    d_equalityEngine.addFunctionKind(kind::BITVECTOR_ASHR);
-      //    d_equalityEngine.addFunctionKind(kind::BITVECTOR_ULT);
-      //    d_equalityEngine.addFunctionKind(kind::BITVECTOR_ULE);
-      //    d_equalityEngine.addFunctionKind(kind::BITVECTOR_UGT);
-      //    d_equalityEngine.addFunctionKind(kind::BITVECTOR_UGE);
-      //    d_equalityEngine.addFunctionKind(kind::BITVECTOR_SLT);
-      //    d_equalityEngine.addFunctionKind(kind::BITVECTOR_SLE);
-      //    d_equalityEngine.addFunctionKind(kind::BITVECTOR_SGT);
-      //    d_equalityEngine.addFunctionKind(kind::BITVECTOR_SGE);
+  {}
 
-    }
-  }
+TheoryBV::~TheoryBV() {}
 
-TheoryBV::~TheoryBV() {
-  delete d_bitblaster; 
-}
 TheoryBV::Statistics::Statistics():
   d_avgConflictSize("theory::bv::AvgBVConflictSize"),
   d_solveSubstitutions("theory::bv::NumberOfSolveSubstitutions", 0),
@@ -115,141 +73,45 @@ void TheoryBV::preRegisterTerm(TNode node) {
     return;
   }
 
-  if ((node.getKind() == kind::EQUAL ||
-       node.getKind() == kind::BITVECTOR_ULT ||
-       node.getKind() == kind::BITVECTOR_ULE ||
-       node.getKind() == kind::BITVECTOR_SLT ||
-       node.getKind() == kind::BITVECTOR_SLE) &&
-      !d_bitblaster->hasBBAtom(node)) {
-    d_bitblastQueue.push_back(node); 
-  }
-
-  if (d_useEqualityEngine) {
-    switch (node.getKind()) {
-      case kind::EQUAL:
-        // Add the trigger for equality
-        d_equalityEngine.addTriggerEquality(node);
-        break;
-      default:
-        d_equalityEngine.addTerm(node);
-        break;
-    }
-  }
-
+  d_bitblastSolver.preRegister(node);
+  d_equalitySolver.preRegister(node); 
 }
 
 void TheoryBV::check(Effort e)
 {
   BVDebug("bitvector") << "TheoryBV::check(" << e << ")" << std::endl;
 
-  if (Options::current()->bitvectorEagerBitblast) {
-    while (!done()) {
-      Assertion assertion = get();
-      TNode fact = assertion.assertion;
-      if (fact.getKind() == kind::NOT) {
-        if (fact[0].getKind() != kind::BITVECTOR_BITOF) {
-          d_bitblaster->bbAtom(fact[0]);
-        }
-      } else {
-        if (fact.getKind() != kind::BITVECTOR_BITOF) {
-          d_bitblaster->bbAtom(fact);
-        }
-      }
-    }
+  // if we are already in conflict just return the conflict 
+  if (d_conflict) {
+    BVDebug("bitvector") << indent() << "TheoryBV::check(): conflict " << d_conflictNode;
+    d_out->conflict(d_conflictNode);
+    d_statistics.d_avgConflictSize.addEntry(d_conflictNode.getNumChildren());
     return;
   }
-
-  // getting the new assertions
   
+  // getting the new assertions
   std::vector<TNode> new_assertions; 
-  while (!done() && !d_conflict) {
+  while (!done()) {
     Assertion assertion = get();
     TNode fact = assertion.assertion;
     new_assertions.push_back(fact);
     BVDebug("bitvector-assertions") << "TheoryBV::check assertion " << fact << "\n"; 
   }
 
-  // sending assertions to equality engine first
-
-  for (unsigned i = 0; i < new_assertions.size(); ++i) {
-    TNode fact = new_assertions[i];
-    TypeNode factType = fact[0].getType(); 
-
-    // Notify the equality engine
-    if (d_useEqualityEngine && !d_conflict && !propagatedBy(fact, SUB_EQUALITY) ) {
-      bool negated = fact.getKind() == kind::NOT;
-      TNode predicate = negated ? fact[0] : fact;
-      if (predicate.getKind() == kind::EQUAL) {
-        if (negated) {
-          // dis-equality
-          d_equalityEngine.assertEquality(predicate, false, fact);
-        } else {
-          // equality
-          d_equalityEngine.assertEquality(predicate, true, fact);
-        }
-      } else {
-        // Adding predicate if the congruence over it is turned on
-        if (d_equalityEngine.isFunctionKind(predicate.getKind())) {
-          d_equalityEngine.assertPredicate(predicate, !negated, fact);
-        }
-      }
-    }
-
-    // checking for a conflict 
-    if (d_conflict) {
-      BVDebug("bitvector") << indent() << "TheoryBV::check(): conflict " << d_conflictNode;
-      d_out->conflict(d_conflictNode);
-      return;
-    }
-  }
-
-  // bit-blasting atoms on queue
-
-  while (!d_bitblastQueue.empty()) {
-    TNode node = d_bitblastQueue.front();
-    d_bitblaster->bbAtom(node);
-    d_bitblastQueue.pop(); 
-  }
+  // sending assertions to the equality solver first
+  bool ok = d_equalitySolver.addAssertions(new_assertions, e);
   
-  // bit-blaster propagation 
-  for (unsigned i = 0; i < new_assertions.size(); ++i) {
-    TNode fact = new_assertions[i];
-    if (!d_conflict && !propagatedBy(fact, SUB_BITBLASTER)) {
-      // Some atoms have not been bit-blasted yet
-      d_bitblaster->bbAtom(fact);
-      // Assert to sat
-      bool ok = d_bitblaster->assertToSat(fact, d_useSatPropagation);
-      if (!ok) {
-        std::vector<TNode> conflictAtoms;
-        d_bitblaster->getConflict(conflictAtoms);
-        d_statistics.d_avgConflictSize.addEntry(conflictAtoms.size());
-        d_conflict = true;
-        d_conflictNode = mkConjunction(conflictAtoms);
-        break;
-      }
-    }
+  if (ok) {
+    // sending assertions to the bitblast solver
+    ok = d_bitblastSolver.addAssertions(new_assertions, e); 
   }
-
-  // If in conflict, output the conflict
-  if (d_conflict) {
+  
+  if (!ok) {
+    // output conflict 
+    Assert (d_conflict);
     BVDebug("bitvector") << indent() << "TheoryBV::check(): conflict " << d_conflictNode;
     d_out->conflict(d_conflictNode);
-    return;
-  }
-
-  if (e == EFFORT_FULL || Options::current()->bitvectorEagerFullcheck) {
-    Assert(done() && !d_conflict);
-    BVDebug("bitvector") << "TheoryBV::check " << e << "\n";
-    bool ok = d_bitblaster->solve();
-    if (!ok) {
-      std::vector<TNode> conflictAtoms;
-      d_bitblaster->getConflict(conflictAtoms);
-      d_statistics.d_avgConflictSize.addEntry(conflictAtoms.size());
-      Node conflict = mkConjunction(conflictAtoms);
-      d_out->conflict(conflict);
-      BVDebug("bitvector") << "TheoryBV::check returns conflict: " <<conflict <<" \n ";
-      return; 
-    }
+    d_statistics.d_avgConflictSize.addEntry(d_conflictNode.getNumChildren());
   }
 }
 
@@ -301,8 +163,7 @@ void TheoryBV::propagate(Effort e) {
           std::vector<TNode> assumptions;
           explain(literal, assumptions);
           explain(negLiteral, assumptions);
-          d_conflictNode = mkAnd(assumptions); 
-          d_conflict = true;
+          setConflict(mkAnd(assumptions)); 
           return;
         }
         
@@ -311,14 +172,12 @@ void TheoryBV::propagate(Effort e) {
         d_alreadyPropagatedSet.insert(literal); 
       } else {
         Debug("bitvector") << indent() << "TheoryBV::propagate(): in conflict, normalized = " << normalized << std::endl;
-        
         Node negatedLiteral;
         std::vector<TNode> assumptions;
         negatedLiteral = normalized.getKind() == kind::NOT ? (Node) normalized[0] : normalized.notNode();
         assumptions.push_back(negatedLiteral);
         explain(literal, assumptions);
-        d_conflictNode = mkAnd(assumptions);
-        d_conflict = true;
+        setConflict(mkAnd(assumptions));
         return;
       }
     }
@@ -381,8 +240,7 @@ bool TheoryBV::storePropagation(TNode literal, SubTheory subtheory)
     Node negatedLiteral = literal.getKind() == kind::NOT ? (Node) literal[0] : literal.notNode();
     assumptions.push_back(negatedLiteral);
     explain(literal, assumptions);
-    d_conflictNode = mkAnd(assumptions);
-    d_conflict = true;
+    setConflict(mkAnd(assumptions)); 
     return false;
   }
 
@@ -396,17 +254,12 @@ bool TheoryBV::storePropagation(TNode literal, SubTheory subtheory)
 
 
 void TheoryBV::explain(TNode literal, std::vector<TNode>& assumptions) {
+  // Ask the appropriate subtheory for the explanation 
   if (propagatedBy(literal, SUB_EQUALITY)) {
-    bool polarity = literal.getKind() != kind::NOT;
-    TNode atom = polarity ? literal : literal[0];
-    if (atom.getKind() == kind::EQUAL) {
-      d_equalityEngine.explainEquality(atom[0], atom[1], polarity, assumptions);
-    } else {
-      d_equalityEngine.explainPredicate(atom, polarity, assumptions);
-    }
+    d_equalitySolver.explain(literal, assumptions); 
   } else {
-    Assert(propagatedBy(literal, SUB_BITBLASTER));
-    d_bitblaster->explain(literal, assumptions); 
+    Assert(propagatedBy(literal, SUB_BITBLAST));
+    d_bitblastSolver.explain(literal, assumptions); 
   }
 }
 
@@ -432,7 +285,7 @@ void TheoryBV::addSharedTerm(TNode t) {
   Debug("bitvector::sharing") << indent() << "TheoryBV::addSharedTerm(" << t << ")" << std::endl;
   d_sharedTermsSet.insert(t); 
   if (!Options::current()->bitvectorEagerBitblast && d_useEqualityEngine) {
-    d_equalityEngine.addTriggerTerm(t);
+    d_equalitySolver.addSharedTerm(t); 
   }
 }
 
@@ -443,16 +296,6 @@ EqualityStatus TheoryBV::getEqualityStatus(TNode a, TNode b)
     return EQUALITY_UNKNOWN;
   }
 
-  if (d_useEqualityEngine) {
-    if (d_equalityEngine.areEqual(a, b)) {
-      // The terms are implied to be equal
-      return EQUALITY_TRUE;
-    }
-    if (d_equalityEngine.areDisequal(a, b)) {
-      // The terms are implied to be dis-equal
-      return EQUALITY_FALSE;
-    }
-  }
-  return EQUALITY_UNKNOWN;
+  return d_equalitySolver.getEqualityStatus(a, b); 
 }
 
diff --git a/src/theory/bv/theory_bv.h b/src/theory/bv/theory_bv.h
index 9ab5f8e1c..214fa3b36 100644
--- a/src/theory/bv/theory_bv.h
+++ b/src/theory/bv/theory_bv.h
@@ -27,40 +27,24 @@
 #include "context/cdhashset.h"
 #include "theory/bv/theory_bv_utils.h"
 #include "util/stats.h"
-#include "theory/uf/equality_engine.h"
 #include "context/cdqueue.h"
-
-namespace BVMinisat {
-class SimpSolver; 
-}
-
+#include "theory/bv/bv_subtheory.h"
 
 namespace CVC4 {
 namespace theory {
 namespace bv {
 
-/// forward declarations 
-class Bitblaster;
-
 class TheoryBV : public Theory {
 
-
-private:
-
   /** The context we are using */
   context::Context* d_context;
 
-  /** The asserted stuff */
-  context::CDList<TNode> d_assertions;
-  
-  /** Bitblaster */
-  Bitblaster* d_bitblaster; 
-
-  context::CDQueue<TNode> d_bitblastQueue; 
-  
   /** Context dependent set of atoms we already propagated */
   context::CDHashSet<TNode, TNodeHashFunction> d_alreadyPropagatedSet;
   context::CDHashSet<TNode, TNodeHashFunction> d_sharedTermsSet;
+
+  BitblastSolver d_bitblastSolver;
+  EqualitySolver d_equalitySolver;
 public:
 
   TheoryBV(context::Context* c, context::UserContext* u, OutputChannel& out, Valuation valuation, const LogicInfo& logicInfo);
@@ -70,6 +54,8 @@ public:
 
   void check(Effort e);
 
+  void propagate(Effort e);
+  
   Node explain(TNode n);
 
   Node getValue(TNode n);
@@ -91,58 +77,6 @@ private:
   
   Statistics d_statistics;
   
-  // Added by Clark
-  // NotifyClass: template helper class for d_equalityEngine - handles call-back from congruence closure module
-  class NotifyClass : public eq::EqualityEngineNotify {
-
-    TheoryBV& d_bv;
-
-  public:
-
-    NotifyClass(TheoryBV& uf): d_bv(uf) {}
-
-    bool eqNotifyTriggerEquality(TNode equality, bool value) {
-      Debug("bitvector") << "NotifyClass::eqNotifyTriggerEquality(" << equality << ", " << (value ? "true" : "false" )<< ")" << std::endl;
-      if (value) {
-        return d_bv.storePropagation(equality, SUB_EQUALITY);
-      } else {
-        return d_bv.storePropagation(equality.notNode(), SUB_EQUALITY);
-      }
-    }
-
-    bool eqNotifyTriggerPredicate(TNode predicate, bool value) {
-      Debug("bitvector") << "NotifyClass::eqNotifyTriggerPredicate(" << predicate << ", " << (value ? "true" : "false" )<< ")" << std::endl;
-      if (value) {
-        return d_bv.storePropagation(predicate, SUB_EQUALITY);
-      } else {
-        return d_bv.storePropagation(predicate.notNode(), SUB_EQUALITY);
-      }
-    }
-
-    bool eqNotifyTriggerTermEquality(TNode t1, TNode t2, bool value) {
-      Debug("bitvector") << "NotifyClass::eqNotifyTriggerTermMerge(" << t1 << ", " << t2 << std::endl;
-      if (value) {
-        return d_bv.storePropagation(t1.eqNode(t2), SUB_EQUALITY);
-      } else {
-        return d_bv.storePropagation(t1.eqNode(t2).notNode(), SUB_EQUALITY);
-      }
-    }
-
-    bool eqNotifyConstantTermMerge(TNode t1, TNode t2) {
-      Debug("bitvector") << "NotifyClass::eqNotifyConstantTermMerge(" << t1 << ", " << t2 << std::endl;
-      if (Theory::theoryOf(t1) == THEORY_BOOL) {
-        return d_bv.storePropagation(t1.iffNode(t2), SUB_EQUALITY);
-      }
-      return d_bv.storePropagation(t1.eqNode(t2), SUB_EQUALITY);
-    }
-  };
-
-  /** The notify class for d_equalityEngine */
-  NotifyClass d_notify;
-
-  /** Equaltity engine */
-  eq::EqualityEngine d_equalityEngine;
-
   // Are we in conflict?
   context::CDO<bool> d_conflict;
 
@@ -155,11 +89,9 @@ private:
   /** Index of the next literal to propagate */
   context::CDO<unsigned> d_literalsToPropagateIndex;
 
-  context::CDQueue<Node> d_toBitBlast;
-
   enum SubTheory {
     SUB_EQUALITY = 1,
-    SUB_BITBLASTER = 2
+    SUB_BITBLAST = 2
   };
 
   /**
@@ -187,17 +119,22 @@ private:
 
   EqualityStatus getEqualityStatus(TNode a, TNode b);
 
-  friend class Bitblaster;
-
   inline std::string indent()
   {
     std::string indentStr(getSatContext()->getLevel(), ' ');
     return indentStr;
   }
-  
-public:
 
-  void propagate(Effort e);
+  void setConflict(Node conflict) {
+    d_conflict = true; 
+    d_conflictNode = conflict; 
+  }
+
+  bool inConflict() { return d_conflict == true; }
+  
+  friend class Bitblaster;
+  friend class BitblastSolver;
+  friend class EqualitySolver; 
   
 };/* class TheoryBV */