started work on the inequality bv subtheory

13 files changed, 542 insertions, 458 deletions

diff --git a/src/theory/bv/bv_inequality_graph.h b/src/theory/bv/bv_inequality_graph.h
new file mode 100644
index 000000000..2ac22bb5b
--- /dev/null
+++ b/src/theory/bv/bv_inequality_graph.h
@@ -0,0 +1,54 @@
+/*********************                                                        */
+/*! \file bv_inequality_graph.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-2012  New York University and The University of Iowa
+ ** 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_INEQUALITY__GRAPH_H
+#define __CVC4__THEORY__BV__BV_INEQUALITY__GRAPH_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 {
+
+typedef unsigned TermId; 
+typedef unsigned ReasonId;
+
+class InequalityGraph {
+  context::Context d_context;
+  
+public:
+  
+  InequalityGraph(context::Context* c)
+    : d_context(c)
+  {}
+  bool addInequality(TermId a, TermId b, ReasonId reason);
+  bool propagate();
+  bool areLessThan(TermId a, TermId b);
+  void getConflict(std::vector<ReasonId>& conflict); 
+}; 
+
+}
+}
+}
+
+#endif /* __CVC4__THEORY__BV__BV_INEQUALITY__GRAPH_H */
diff --git a/src/theory/bv/bv_subtheory.h b/src/theory/bv/bv_subtheory.h
index d95aaa873..9e7566ebb 100644
--- a/src/theory/bv/bv_subtheory.h
+++ b/src/theory/bv/bv_subtheory.h
@@ -32,9 +32,9 @@ class TheoryModel;
 namespace bv {
 
 enum SubTheory {
-  SUB_EQUALITY = 1,
+  SUB_CORE = 1,
   SUB_BITBLAST = 2,
-  SUB_CORE = 3
+  SUB_INEQUALITY = 3
 };
 
 inline std::ostream& operator << (std::ostream& out, SubTheory subtheory) {
@@ -42,9 +42,11 @@ inline std::ostream& operator << (std::ostream& out, SubTheory subtheory) {
   case SUB_BITBLAST:
     out << "BITBLASTER";
     break;
-  case SUB_EQUALITY:
-    out << "EQUALITY";
+  case SUB_CORE:
+    out << "BV_CORE_SUBTHEORY";
     break;
+  case SUB_INEQUALITY:
+    out << "BV_INEQUALITY_SUBTHEORY"; 
   default:
     Unreachable();
     break;
@@ -83,10 +85,10 @@ public:
     d_assertionIndex(c, 0)
   {}
   virtual ~SubtheorySolver() {}
-  
   virtual bool check(Theory::Effort e) = 0; 
   virtual void explain(TNode literal, std::vector<TNode>& assumptions) = 0;
   virtual void preRegister(TNode node) {}
+  virtual void propagate(Effort e) {}
   virtual void collectModelInfo(TheoryModel* m) = 0;
   bool done() { return d_assertionQueue.size() == d_assertionIndex; }
   TNode get() {
diff --git a/src/theory/bv/bv_subtheory_core.cpp b/src/theory/bv/bv_subtheory_core.cpp
index 2e1320d1a..f1255e07c 100644
--- a/src/theory/bv/bv_subtheory_core.cpp
+++ b/src/theory/bv/bv_subtheory_core.cpp
@@ -14,7 +14,7 @@
  ** Algebraic solver.
  **/
 
-#include "theory/bv/bv_subtheory_eq.h"
+#include "theory/bv/bv_subtheory_core.h"
 
 #include "theory/bv/theory_bv.h"
 #include "theory/bv/theory_bv_utils.h"
@@ -28,16 +28,13 @@ using namespace CVC4::theory;
 using namespace CVC4::theory::bv;
 using namespace CVC4::theory::bv::utils;
 
-CoreSolver::CoreSolver(context::Context* c, TheoryBV* bv, Slicer* slicer)
+CoreSolver::CoreSolver(context::Context* c, TheoryBV* bv)
   : SubtheorySolver(c, bv),
     d_notify(*this),
     d_equalityEngine(d_notify, c, "theory::bv::TheoryBV"),
     d_assertions(c),
-    d_normalFormCache(), 
-    d_slicer(slicer),
-    d_isCoreTheory(c, true),
-    d_baseChanged(false),
-    d_checkCalled(false)
+    d_slicer(new Slicer(c, this)),
+    d_isCoreTheory(c, true)
 {
   if (d_useEqualityEngine) {
 
@@ -85,7 +82,7 @@ void CoreSolver::preRegister(TNode node) {
 
   if (node.getKind() == kind::EQUAL) {
       d_equalityEngine.addTriggerEquality(node);
-      d_slicer->processEquality(node);
+      // d_slicer->processEquality(node);
   } else {
     d_equalityEngine.addTerm(node);
   }
@@ -102,14 +99,9 @@ void CoreSolver::explain(TNode literal, std::vector<TNode>& assumptions) {
   }
 }
 
-Node CoreSolver::getBaseDecomposition(TNode a) {
+Node CoreSolver::getBaseDecomposition(TNode a, std::vector<TNode>& explanation) {
   std::vector<Node> a_decomp;
-  // FIXME: hack to do bitwise decomposition 
-  // for (int i = utils::getSize(a) - 1; i>= 0; --i) {
-  //   Node bit = Rewriter::rewrite(utils::mkExtract(a, i, i));
-  //   a_decomp.push_back(bit); 
-  // }
-  d_slicer->getBaseDecomposition(a, a_decomp);
+  d_slicer->getBaseDecomposition(a, a_decomp, explanation);
   Node new_a = utils::mkConcat(a_decomp);
   return new_a; 
 }
@@ -120,50 +112,56 @@ bool CoreSolver::decomposeFact(TNode fact) {
   // concat:
   //   a == a_1 concat ... concat a_k
   //   b == b_1 concat ... concat b_k
-  TNode eq = fact.getKind() == kind::NOT? fact[0] : fact; 
 
-  TNode a = eq[0];
-  TNode b = eq[1];
+  if (fact.getKind() == kind::EQUAL) {
+    TNode a = fact[0];
+    TNode b = fact[1];
 
-  // d_slicer->processEquality(eq); 
-  
-  Node new_a = getBaseDecomposition(a);
-  Node new_b = getBaseDecomposition(b); 
-  
-  Assert (utils::getSize(new_a) == utils::getSize(new_b) &&
-          utils::getSize(new_a) == utils::getSize(a)); 
-  
-  NodeManager* nm = NodeManager::currentNM();
-  Node a_eq_new_a = nm->mkNode(kind::EQUAL, a, new_a);
-  Node b_eq_new_b = nm->mkNode(kind::EQUAL, b, new_b);
+    d_slicer->processEquality(fact); 
+    std::vector<TNode> explanation; 
+    Node new_a = getBaseDecomposition(a, explanation);
+    Node new_b = getBaseDecomposition(b, explanation);
 
-  bool ok = true; 
-  ok = assertFactToEqualityEngine(a_eq_new_a, utils::mkTrue());
-  if (!ok) return false; 
-  ok = assertFactToEqualityEngine(b_eq_new_b, utils::mkTrue());
-  if (!ok) return false; 
-  ok = assertFactToEqualityEngine(fact, fact);
-  if (!ok) return false;
+    explanation.push_back(fact);
+    TNode reason = utils::mkAnd(explanation); 
   
-  if (fact.getKind() == kind::EQUAL) {
+    Assert (utils::getSize(new_a) == utils::getSize(new_b) &&
+            utils::getSize(new_a) == utils::getSize(a)); 
+    // FIXME: do we still need to assert these? 
+    NodeManager* nm = NodeManager::currentNM();
+    Node a_eq_new_a = nm->mkNode(kind::EQUAL, a, new_a);
+    Node b_eq_new_b = nm->mkNode(kind::EQUAL, b, new_b);
+
+    bool ok = true; 
+    ok = assertFactToEqualityEngine(a_eq_new_a, utils::mkTrue());
+    if (!ok) return false; 
+    ok = assertFactToEqualityEngine(b_eq_new_b, utils::mkTrue());
+    if (!ok) return false; 
     // assert the individual equalities as well
     //    a_i == b_i
     if (new_a.getKind() == kind::BITVECTOR_CONCAT &&
         new_b.getKind() == kind::BITVECTOR_CONCAT) {
-      
       Assert (new_a.getNumChildren() == new_b.getNumChildren()); 
       for (unsigned i = 0; i < new_a.getNumChildren(); ++i) {
         Node eq_i = nm->mkNode(kind::EQUAL, new_a[i], new_b[i]);
-        ok = assertFactToEqualityEngine(eq_i, fact);
+        ok = assertFactToEqualityEngine(eq_i, reason);
         if (!ok) return false;
       }
     }
+    // merge the two terms in the slicer as well
+    d_slicer->assertEquality(fact); 
+  } else {
+    // still need to register the terms
+    TNode a = fact[0][0];
+    TNode b = fact[0][1];
+    d_slicer->registerTerm(a);
+    d_slicer->registerTerm(b); 
   }
-  return true; 
+  // finally assert the actual fact to the equality engine
+  return assertFactToEqualityEngine(fact, fact);
 }
 
 bool CoreSolver::check(Theory::Effort e) {
-  d_checkCalled = true; 
   Trace("bitvector::core") << "CoreSolver::check \n";
   Assert (!d_bv->inConflict());
 
@@ -179,7 +177,6 @@ bool CoreSolver::check(Theory::Effort e) {
     
     // only reason about equalities
     if (fact.getKind() == kind::EQUAL || (fact.getKind() == kind::NOT && fact[0].getKind() == kind::EQUAL)) {
-      TNode eq = fact.getKind() == kind::EQUAL ? fact : fact[0];
       ok = decomposeFact(fact);
     } else {
       ok = assertFactToEqualityEngine(fact, fact); 
@@ -188,6 +185,14 @@ bool CoreSolver::check(Theory::Effort e) {
       return false; 
   }
   
+  // make sure to assert the new splits
+  std::vector<Node> new_splits;
+  d_slicer->getNewSplits(new_splits);
+  for (unsigned i = 0; i < new_splits.size(); ++i) {
+    ok = assertFactToEqualityEngine(new_splits[i], utils::mkTrue());
+    if (!ok)
+      return false; 
+  }
   return true;
 }
 
@@ -197,7 +202,6 @@ bool CoreSolver::assertFactToEqualityEngine(TNode fact, TNode reason) {
   // Notify the equality engine 
   if (d_useEqualityEngine && !d_bv->inConflict() && !d_bv->propagatedBy(fact, SUB_CORE) ) {
     Trace("bitvector::core") << "     (assert " << fact << ")\n";  
-    //d_assertions.push_back(fact); 
     bool negated = fact.getKind() == kind::NOT;
     TNode predicate = negated ? fact[0] : fact;
     if (predicate.getKind() == kind::EQUAL) {
diff --git a/src/theory/bv/bv_subtheory_core.h b/src/theory/bv/bv_subtheory_core.h
index d5235a864..230817e13 100644
--- a/src/theory/bv/bv_subtheory_core.h
+++ b/src/theory/bv/bv_subtheory_core.h
@@ -31,14 +31,7 @@ class Base;
  */
 class CoreSolver : public SubtheorySolver {
 
-  enum FactSource {
-    AXIOM = 0, // this is asserting that a node is equal to its decomposition 
-    ASSERTION = 1, // externally visible assertion 
-    SPLIT = 2 //  fact resulting from a split
-  };
-  
   // NotifyClass: handles call-back from congruence closure module
-
   class NotifyClass : public eq::EqualityEngineNotify {
     CoreSolver& d_solver;
 
@@ -52,12 +45,12 @@ class CoreSolver : public SubtheorySolver {
     void eqNotifyPreMerge(TNode t1, TNode t2) { }
     void eqNotifyPostMerge(TNode t1, TNode t2) { }
     void eqNotifyDisequal(TNode t1, TNode t2, TNode reason) { }
-};
+  };
 
 
   /** The notify class for d_equalityEngine */
   NotifyClass d_notify;
-
+  
   /** Equality engine */
   eq::EqualityEngine d_equalityEngine;
 
@@ -69,17 +62,14 @@ class CoreSolver : public SubtheorySolver {
 
   /** FIXME: for debugging purposes only */
   context::CDList<TNode> d_assertions;
-  __gnu_cxx::hash_map<TNode, Node, TNodeHashFunction> d_normalFormCache; 
   Slicer* d_slicer;
   context::CDO<bool> d_isCoreTheory;
 
   bool assertFactToEqualityEngine(TNode fact, TNode reason);  
   bool decomposeFact(TNode fact);
-  Node getBaseDecomposition(TNode a);
-  bool d_baseChanged;
-  bool d_checkCalled;
-public:
-  CoreSolver(context::Context* c, TheoryBV* bv, Slicer* slicer);
+  Node getBaseDecomposition(TNode a, std::vector<TNode>& explanation);
+public: 
+  CoreSolver(context::Context* c, TheoryBV* bv);
   bool  isCoreTheory() { return d_isCoreTheory; }
   void  setMasterEqualityEngine(eq::EqualityEngine* eq);
   void  preRegister(TNode node);
@@ -100,6 +90,7 @@ public:
     }
     return EQUALITY_UNKNOWN;
   }
+  bool hasTerm(TNode node) const { return d_equalityEngine.hasTerm(node); }
 };
 
 
diff --git a/src/theory/bv/bv_subtheory_eq.cpp b/src/theory/bv/bv_subtheory_eq.cpp
deleted file mode 100644
index f11b1252b..000000000
--- a/src/theory/bv/bv_subtheory_eq.cpp
+++ /dev/null
@@ -1,185 +0,0 @@
-/*********************                                                        */
-/*! \file bv_subtheory_eq.cpp
- ** \verbatim
- ** Original author: dejan
- ** Major contributors: none
- ** Minor contributors (to current version): lianah
- ** This file is part of the CVC4 prototype.
- ** Copyright (c) 2009-2012  New York University and The University of Iowa
- ** See the file COPYING in the top-level source directory for licensing
- ** information.\endverbatim
- **
- ** \brief Algebraic solver.
- **
- ** Algebraic solver.
- **/
-
-#include "theory/bv/bv_subtheory_eq.h"
-#include "theory/bv/theory_bv.h"
-#include "theory/bv/theory_bv_utils.h"
-#include "theory/model.h"
-
-using namespace std;
-using namespace CVC4;
-using namespace CVC4::context;
-using namespace CVC4::theory;
-using namespace CVC4::theory::bv;
-using namespace CVC4::theory::bv::utils;
-
-EqualitySolver::EqualitySolver(context::Context* c, TheoryBV* bv)
-  : SubtheorySolver(c, bv),
-    d_notify(*this),
-    d_equalityEngine(d_notify, c, "theory::bv::TheoryBV"),
-    d_assertions(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);
-  }
-}
-
-void EqualitySolver::setMasterEqualityEngine(eq::EqualityEngine* eq) {
-  d_equalityEngine.setMasterEqualityEngine(eq);
-}
-
-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) {
-  Trace("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, SUB_EQUALITY) ) {
-      Trace("bitvector::equality") << "     (assert " << fact << ")\n";  
-      d_assertions.push_back(fact); 
-      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) {
-  Debug("bitvector::equality") << "NotifyClass::eqNotifyTriggerEquality(" << equality << ", " << (value ? "true" : "false" )<< ")" << std::endl;
-  if (value) {
-    return d_solver.storePropagation(equality);
-  } else {
-    return d_solver.storePropagation(equality.notNode());
-  }
-}
-
-bool EqualitySolver::NotifyClass::eqNotifyTriggerPredicate(TNode predicate, bool value) {
-  Debug("bitvector::equality") << "NotifyClass::eqNotifyTriggerPredicate(" << predicate << ", " << (value ? "true" : "false" ) << ")" << std::endl;
-  if (value) {
-    return d_solver.storePropagation(predicate);
-  } else {
-    return d_solver.storePropagation(predicate.notNode());
-  }
-}
-
-bool EqualitySolver::NotifyClass::eqNotifyTriggerTermEquality(TheoryId tag, TNode t1, TNode t2, bool value) {
-  Debug("bitvector::equality") << "NotifyClass::eqNotifyTriggerTermMerge(" << t1 << ", " << t2 << ")" << std::endl;
-  if (value) {
-    return d_solver.storePropagation(t1.eqNode(t2));
-  } else {
-    return d_solver.storePropagation(t1.eqNode(t2).notNode());
-  }
-}
-
-void EqualitySolver::NotifyClass::eqNotifyConstantTermMerge(TNode t1, TNode t2) {
-  d_solver.conflict(t1, t2);
-}
-
-bool EqualitySolver::storePropagation(TNode literal) {
-  return d_bv->storePropagation(literal, SUB_EQUALITY);
-}
-  
-void EqualitySolver::conflict(TNode a, TNode b) {
-  std::vector<TNode> assumptions;
-  d_equalityEngine.explainEquality(a, b, true, assumptions);
-  d_bv->setConflict(mkAnd(assumptions));
-}
-
-void EqualitySolver::collectModelInfo(TheoryModel* m) {
-  if (Debug.isOn("bitvector-model")) {
-    context::CDList<TNode>::const_iterator it = d_assertions.begin();
-    for (; it!= d_assertions.end(); ++it) {
-      Debug("bitvector-model") << "EqualitySolver::collectModelInfo (assert "
-                               << *it << ")\n";
-    }
-  }
-  set<Node> termSet;
-  d_bv->computeRelevantTerms(termSet);
-  m->assertEqualityEngine(&d_equalityEngine, &termSet);
-}
diff --git a/src/theory/bv/bv_subtheory_eq.h b/src/theory/bv/bv_subtheory_eq.h
deleted file mode 100644
index 2b024cfd4..000000000
--- a/src/theory/bv/bv_subtheory_eq.h
+++ /dev/null
@@ -1,90 +0,0 @@
-/*********************                                                        */
-/*! \file bv_subtheory_eq.h
- ** \verbatim
- ** Original author: dejan
- ** Major contributors: none
- ** Minor contributors (to current version): lianah, mdeters
- ** This file is part of the CVC4 prototype.
- ** Copyright (c) 2009-2012  New York University and The University of Iowa
- ** See the file COPYING in the top-level source directory for licensing
- ** information.\endverbatim
- **
- ** \brief Algebraic solver.
- **
- ** Algebraic solver.
- **/
-
-#pragma once
-
-#include "cvc4_private.h"
-#include "theory/bv/bv_subtheory.h"
-
-namespace CVC4 {
-namespace theory {
-namespace bv {
-
-/**
- * Bitvector equality solver
- */
-class EqualitySolver : public SubtheorySolver {
-
-  // NotifyClass: handles call-back from congruence closure module
-
-  class NotifyClass : public eq::EqualityEngineNotify {
-    EqualitySolver& d_solver;
-
-  public:
-    NotifyClass(EqualitySolver& solver): d_solver(solver) {}
-    bool eqNotifyTriggerEquality(TNode equality, bool value);
-    bool eqNotifyTriggerPredicate(TNode predicate, bool value);
-    bool eqNotifyTriggerTermEquality(TheoryId tag, TNode t1, TNode t2, bool value);
-    void eqNotifyConstantTermMerge(TNode t1, TNode t2);
-    void eqNotifyNewClass(TNode t) { }
-    void eqNotifyPreMerge(TNode t1, TNode t2) { }
-    void eqNotifyPostMerge(TNode t1, TNode t2) { }
-    void eqNotifyDisequal(TNode t1, TNode t2, TNode reason) { }
-};
-
-
-  /** The notify class for d_equalityEngine */
-  NotifyClass d_notify;
-
-  /** Equality engine */
-  eq::EqualityEngine d_equalityEngine;
-
-  /** Store a propagation to the bv solver */
-  bool storePropagation(TNode literal);
-  
-  /** Store a conflict from merging two constants */
-  void conflict(TNode a, TNode b);
-
-  /** FIXME: for debugging purposes only */
-  context::CDList<TNode> d_assertions; 
-public:
-
-  EqualitySolver(context::Context* c, TheoryBV* bv);
-  void setMasterEqualityEngine(eq::EqualityEngine* eq);
-  void  preRegister(TNode node);
-  bool  addAssertions(const std::vector<TNode>& assertions, Theory::Effort e);
-  void  explain(TNode literal, std::vector<TNode>& assumptions);
-  void  collectModelInfo(TheoryModel* m);
-  void  addSharedTerm(TNode t) {
-    d_equalityEngine.addTriggerTerm(t, THEORY_BV);
-  }
-  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, false)) {
-      // The terms are implied to be dis-equal
-      return EQUALITY_FALSE;
-    }
-    return EQUALITY_UNKNOWN;
-  }
-};
-
-
-}
-}
-}
diff --git a/src/theory/bv/bv_subtheory_inequality.cpp b/src/theory/bv/bv_subtheory_inequality.cpp
new file mode 100644
index 000000000..7ccef5ff1
--- /dev/null
+++ b/src/theory/bv/bv_subtheory_inequality.cpp
@@ -0,0 +1,38 @@
+/*********************                                                        */
+/*! \file bv_subtheory_inequality.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-2012  New York University and The University of Iowa
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.\endverbatim
+ **
+ ** \brief Algebraic solver.
+ **
+ ** Algebraic solver.
+ **/
+
+#include "theory/bv/bv_subtheory_inequality.h"
+#include "theory/bv/theory_bv.h"
+#include "theory/bv/theory_bv_utils.h"
+#include "theory/model.h"
+
+using namespace std;
+using namespace CVC4;
+using namespace CVC4::context;
+using namespace CVC4::theory;
+using namespace CVC4::theory::bv;
+using namespace CVC4::theory::bv::utils;
+
+bool InequalitySolver::check(Theory::Effort e) {
+  
+}
+void InequalitySolver::explain(TNode literal, std::vector<TNode>& assumptions) {
+  
+}
+
+bool InequalitySolver::propagate(Theory::Effort e) {
+  
+}
diff --git a/src/theory/bv/bv_subtheory_inequality.h b/src/theory/bv/bv_subtheory_inequality.h
new file mode 100644
index 000000000..63f9af9e4
--- /dev/null
+++ b/src/theory/bv/bv_subtheory_inequality.h
@@ -0,0 +1,50 @@
+/*********************                                                        */
+/*! \file bv_subtheory_inequality.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-2012  New York University and The University of Iowa
+ ** 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__INEQUALITY_H
+#define __CVC4__THEORY__BV__BV_SUBTHEORY__INEQUALITY_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 {
+
+class InequalitySolver {
+
+public:
+  
+  InequalitySolver(context::Context* c, TheoryBV* bv)
+    : SubtheorySolver(c, bv)
+  {}
+  
+  bool check(Theory::Effort e);
+  void propagate(Effort e); 
+  void explain(TNode literal, std::vector<TNode>& assumptions); 
+}; 
+
+}
+}
+}
+
+#endif /* __CVC4__THEORY__BV__BV_SUBTHEORY__INEQUALITY_H */ 
diff --git a/src/theory/bv/slicer.cpp b/src/theory/bv/slicer.cpp
index ac668ab20..92166224b 100644
--- a/src/theory/bv/slicer.cpp
+++ b/src/theory/bv/slicer.cpp
@@ -19,7 +19,7 @@
 #include "theory/bv/slicer.h"
 #include "theory/bv/theory_bv_utils.h"
 #include "theory/rewriter.h"
-
+#include "theory/bv/bv_subtheory_core.h"
 using namespace CVC4;
 using namespace CVC4::theory;
 using namespace CVC4::theory::bv;
@@ -159,7 +159,7 @@ std::string NormalForm::debugPrint(const UnionFind& uf) const {
 
 std::string UnionFind::Node::debugPrint() const {
   ostringstream os;
-  os << "Repr " << d_repr << " ["<< d_bitwidth << "] ";
+  os << "Repr " << d_edge.repr << " ["<< d_bitwidth << "] ";
   os << "( " << d_ch1 <<", " << d_ch0 << ")" << endl; 
   return os.str(); 
 }
@@ -169,27 +169,44 @@ std::string UnionFind::Node::debugPrint() const {
  * UnionFind
  * 
  */
-TermId UnionFind::addTerm(Index bitwidth) {
+TermId UnionFind::addNode(Index bitwidth) {
+  Assert (bitwidth > 0); 
   Node node(bitwidth);
   d_nodes.push_back(node);
+  
   ++(d_statistics.d_numNodes);
   
   TermId id = d_nodes.size() - 1; 
   //  d_representatives.insert(id);
   ++(d_statistics.d_numRepresentatives); 
-
   Debug("bv-slicer-uf") << "UnionFind::addTerm " << id << " size " << bitwidth << endl;
   return id; 
 }
+
+TermId UnionFind::addExtract(TermId topLevel, Index high, Index low) {
+  ExtractTerm extract(topLevel, high, low);
+  if (d_extractToId.find(extract) != d_extractToId.end()) {
+    return d_extractToId[extract]; 
+  }
+
+  Assert (high >= low); 
+  
+  TermId id = addNode(high - low + 1); 
+  d_idToExtract[id] = extract;
+  d_extractToId[extract] = id; 
+  return id; 
+}
+
 /** 
  * At this point we assume the slicings of the two terms are properly aligned. 
  * 
  * @param t1 
  * @param t2 
  */
-void UnionFind::unionTerms(const ExtractTerm& t1, const ExtractTerm& t2) {
+void UnionFind::unionTerms(const ExtractTerm& t1, const ExtractTerm& t2, TermId reason) {
   Debug("bv-slicer") << "UnionFind::unionTerms " << t1.debugPrint() << " and \n"
-                     << "                      " << t2.debugPrint() << endl;
+                     << "                      " << t2.debugPrint() << "\n"
+                     << " with reason " << reason << endl;
   Assert (t1.getBitwidth() == t2.getBitwidth());
   
   NormalForm nf1(t1.getBitwidth());
@@ -202,10 +219,11 @@ void UnionFind::unionTerms(const ExtractTerm& t1, const ExtractTerm& t2) {
   Assert (nf1.base == nf2.base);
   
   for (unsigned i = 0; i < nf1.decomp.size(); ++i) {
-    merge (nf1.decomp[i], nf2.decomp[i]); 
+    merge (nf1.decomp[i], nf2.decomp[i], reason); 
   } 
 }
 
+
 /** 
  * Merge the two terms in the union find. Both t1 and t2
  * should be root terms. 
@@ -213,7 +231,7 @@ void UnionFind::unionTerms(const ExtractTerm& t1, const ExtractTerm& t2) {
  * @param t1 
  * @param t2 
  */
-void UnionFind::merge(TermId t1, TermId t2) {
+void UnionFind::merge(TermId t1, TermId t2, TermId reason) {
   Debug("bv-slicer-uf") << "UnionFind::merge (" << t1 <<", " << t2 << ")" << endl;
   ++(d_statistics.d_numMerges);
   t1 = find(t1);
@@ -223,7 +241,7 @@ void UnionFind::merge(TermId t1, TermId t2) {
     return;
 
   Assert (! hasChildren(t1) && ! hasChildren(t2));
-  setRepr(t1, t2); 
+  setRepr(t1, t2, reason);
   recordOperation(UnionFind::MERGE, t1); 
   //d_representatives.erase(t1);
   d_statistics.d_numRepresentatives += -1; 
@@ -233,11 +251,26 @@ TermId UnionFind::find(TermId id) {
   TermId repr = getRepr(id); 
   if (repr != UndefinedId) {
     TermId find_id =  find(repr);
-    // setRepr(id, find_id);
     return find_id; 
   }
   return id; 
 }
+
+TermId UnionFind::findWithExplanation(TermId id, std::vector<ExplanationId>& explanation) {
+  TermId repr = getRepr(id);
+
+  if (repr != UndefinedId) {
+    TermId reason = getReason(id);
+    Assert (reason != UndefinedId); 
+    explanation.push_back(reason);
+  
+    TermId find_id =  findWithExplanation(repr, explanation);
+    return find_id; 
+  }
+  return id; 
+}
+
+
 /** 
  * Splits the representative of the term between i-1 and i
  * 
@@ -259,10 +292,14 @@ void UnionFind::split(TermId id, Index i) {
   Assert (i < getBitwidth(id));
   if (!hasChildren(id)) {
     // first time we split this term 
-    TermId bottom_id = addTerm(i);
-    TermId top_id = addTerm(getBitwidth(id) - i);
+    TermId bottom_id = addExtract(getTopLevel(id), i - 1, 0);
+    TermId top_id = addExtract(getTopLevel(id), getBitwidth(id) - 1, i);
     setChildren(id, top_id, bottom_id);
-    recordOperation(UnionFind::SPLIT, id); 
+    recordOperation(UnionFind::SPLIT, id);
+    
+    if (d_slicer->termInEqualityEngine(id)) {
+      d_slicer->enqueueSplit(id, i); 
+    }
   } else {
     Index cut = getCutPoint(id); 
     if (i < cut )
@@ -273,6 +310,14 @@ void UnionFind::split(TermId id, Index i) {
   ++(d_statistics.d_numSplits);
 }
 
+TermId UnionFind::getTopLevel(TermId id) const {
+  __gnu_cxx::hash_map<TermId, ExtractTerm, __gnu_cxx::hash<TermId> >::const_iterator it = d_idToExtract.find(id); 
+  if (it != d_idToExtract.end()) {
+    return (*it).second.id; 
+  }
+  return id; 
+}
+
 void UnionFind::getNormalForm(const ExtractTerm& term, NormalForm& nf) {
   nf.clear(); 
   getDecomposition(term, nf.decomp);
@@ -319,6 +364,56 @@ void UnionFind::getDecomposition(const ExtractTerm& term, Decomposition& decomp)
     getDecomposition(high_child, decomp); 
   }
 }
+
+void UnionFind::getNormalFormWithExplanation(const ExtractTerm& term, NormalForm& nf,
+                                             std::vector<ExplanationId>& explanation) {
+  nf.clear(); 
+  getDecompositionWithExplanation(term, nf.decomp, explanation);
+  // update nf base
+  Index count = 0; 
+  for (unsigned i = 0; i < nf.decomp.size(); ++i) {
+    count += getBitwidth(nf.decomp[i]);
+    nf.base.sliceAt(count); 
+  }
+  Debug("bv-slicer-uf") << "UnionFind::getNormalFrom term: " << term.debugPrint() << endl;
+  Debug("bv-slicer-uf") << "           nf: " << nf.debugPrint(*this) << endl; 
+}
+
+void UnionFind::getDecompositionWithExplanation(const ExtractTerm& term, Decomposition& decomp,
+                                                std::vector<ExplanationId>& explanation) {
+  // making sure the term is aligned
+  TermId id = findWithExplanation(term.id, explanation); 
+
+  Assert (term.high < getBitwidth(id));
+  // because we split the node, this must be the whole extract
+  if (!hasChildren(id)) {
+    Assert (term.high == getBitwidth(id) - 1 &&
+            term.low == 0);
+    decomp.push_back(id);
+    return; 
+  }
+    
+  Index cut = getCutPoint(id);
+  
+  if (term.low < cut && term.high < cut) {
+    // the extract falls entirely on the low child
+    ExtractTerm child_ex(getChild(id, 0), term.high, term.low); 
+    getDecompositionWithExplanation(child_ex, decomp, explanation); 
+  }
+  else if (term.low >= cut && term.high >= cut){
+    // the extract falls entirely on the high child
+    ExtractTerm child_ex(getChild(id, 1), term.high - cut, term.low - cut);
+    getDecompositionWithExplanation(child_ex, decomp, explanation); 
+  }
+  else {
+    // the extract is split over the two children
+    ExtractTerm low_child(getChild(id, 0), cut - 1, term.low);
+    getDecompositionWithExplanation(low_child, decomp, explanation);
+    ExtractTerm high_child(getChild(id, 1), term.high - cut, 0);
+    getDecompositionWithExplanation(high_child, decomp, explanation); 
+  }
+}
+
 /** 
  * May cause reslicings of the decompositions. Must not assume the decompositons
  * are the current normal form. 
@@ -428,7 +523,7 @@ void UnionFind::ensureSlicing(const ExtractTerm& term) {
 void UnionFind::backtrack() {
   return; 
   int size = d_undoStack.size(); 
-  for (int i = size; i > d_undoStackIndex.get(); --i) {
+  for (int i = size; i > (int)d_undoStackIndex.get(); --i) {
     Operation op = d_undoStack.back(); 
     Assert (!d_undoStack.empty()); 
     d_undoStack.pop_back();
@@ -443,8 +538,8 @@ void UnionFind::backtrack() {
 
 void UnionFind::undoMerge(TermId id) {
   TermId repr = getRepr(id);
-  Assert (repr != id);
-  setRepr(id, UndefinedId); 
+  Assert (repr != UndefinedId);
+  setRepr(id, UndefinedId, UndefinedId); 
 }
 
 void UnionFind::undoSplit(TermId id) {
@@ -453,9 +548,6 @@ void UnionFind::undoSplit(TermId id) {
 }
 
 void UnionFind::recordOperation(OperationKind op, TermId term) {
-  if (op == SPLIT) {
-    d_newSplit = true; 
-  }
   d_undoStackIndex.set(d_undoStackIndex.get() + 1);
   d_undoStack.push_back(Operation(op, term));
   Assert (d_undoStack.size() == d_undoStackIndex); 
@@ -488,7 +580,7 @@ ExtractTerm Slicer::registerTerm(TNode node) {
     low = utils::getExtractLow(node); 
   }
   if (d_nodeToId.find(n) == d_nodeToId.end()) {
-    TermId id = d_unionFind.addTerm(utils::getSize(n)); 
+    TermId id = d_unionFind.addNode(utils::getSize(n)); 
     d_nodeToId[n] = id;
     d_idToNode[id] = n; 
   }
@@ -500,7 +592,8 @@ ExtractTerm Slicer::registerTerm(TNode node) {
 
 void Slicer::processEquality(TNode eq) {
   Debug("bv-slicer") << "Slicer::processEquality: " << eq << endl;
-  
+
+  registerEquality(eq); 
   Assert (eq.getKind() == kind::EQUAL);
   TNode a = eq[0];
   TNode b = eq[1];
@@ -511,13 +604,35 @@ void Slicer::processEquality(TNode eq) {
   d_unionFind.ensureSlicing(b_ex);
   
   d_unionFind.alignSlicings(a_ex, b_ex);
-  d_unionFind.unionTerms(a_ex, b_ex);
+
   Debug("bv-slicer") << "Base of " << a_ex.id <<" " << d_unionFind.debugPrint(a_ex.id) << endl;
   Debug("bv-slicer") << "Base of " << b_ex.id <<" " << d_unionFind.debugPrint(b_ex.id) << endl;
   Debug("bv-slicer") << "Slicer::processEquality done. " << endl;
 }
 
-void Slicer::getBaseDecomposition(TNode node, std::vector<Node>& decomp) {
+void Slicer::assertEquality(TNode eq) {
+  Assert (eq.getKind() == kind::EQUAL);
+  ExtractTerm a = registerTerm(eq[0]);
+  ExtractTerm b = registerTerm(eq[1]);
+  ExplanationId reason = getExplanationId(eq); 
+  d_unionFind.unionTerms(a, b, reason); 
+}
+
+TermId Slicer::getId(TNode node) const {
+  __gnu_cxx::hash_map<TNode, TermId, TNodeHashFunction >::const_iterator it = d_nodeToId.find(node);
+  Assert (it != d_nodeToId.end());
+  return it->second; 
+}
+
+void Slicer::registerEquality(TNode eq) {
+  if (d_explanationToId.find(eq) == d_explanationToId.end()) {
+    ExplanationId id = d_explanations.size(); 
+    d_explanations.push_back(eq);
+    d_explanationToId[eq] = id; 
+  }
+}
+
+void Slicer::getBaseDecomposition(TNode node, std::vector<Node>& decomp, std::vector<TNode>& explanation) {
   Debug("bv-slicer") << "Slicer::getBaseDecomposition " << node << endl;
   
   Index high = utils::getSize(node) - 1;
@@ -528,10 +643,18 @@ void Slicer::getBaseDecomposition(TNode node, std::vector<Node>& decomp) {
     low = utils::getExtractLow(node);
     top = node[0]; 
   }
+  
   Assert (d_nodeToId.find(top) != d_nodeToId.end()); 
   TermId id = d_nodeToId[top];
-  NormalForm nf(high-low+1); 
-  d_unionFind.getNormalForm(ExtractTerm(id, high, low), nf);
+  NormalForm nf(high-low+1);
+  std::vector<ExplanationId> explanation_ids; 
+  d_unionFind.getNormalFormWithExplanation(ExtractTerm(id, high, low), nf, explanation_ids);
+
+  for (unsigned i = 0; i < explanation_ids.size(); ++i) {
+    Assert (hasExplanation(explanation_ids[i])); 
+    TNode exp = getExplanation(explanation_ids[i]);
+    explanation.push_back(exp); 
+  }
   
   // construct actual extract nodes
   Index current_low = 0;
@@ -622,25 +745,68 @@ void Slicer::splitEqualities(TNode node, std::vector<Node>& equalities) {
   d_numAddedEqualities += equalities.size() - 1; 
 }
 
-/** 
- * Returns the base decomposition of the current term. 
- * 
- * @param id 
- * 
- * @return 
- */
-Base Slicer::getTopLevelBase(TNode node) {
-  if (node.getKind() == kind::BITVECTOR_EXTRACT) {
-    node = node[0];
+
+ExtractTerm UnionFind::getExtractTerm(TermId id) const {
+  Assert (isExtractTerm(id));
+  
+  return (d_idToExtract.find(id))->second; 
+}
+
+bool UnionFind::isExtractTerm(TermId id) const {
+  return d_idToExtract.find(id) != d_idToExtract.end();
+}
+
+bool Slicer::hasNode(TermId id) const {
+  return d_idToNode.find(id) != d_idToNode.end(); 
+}
+
+Node Slicer::getNode(TermId id) const {
+  // if it was an extract
+  if (d_unionFind.isExtractTerm(id)) {
+    ExtractTerm extract = d_unionFind.getExtractTerm(id);
+    Assert (hasNode(extract.id)); 
+    TNode node = d_idToNode.find(extract.id)->second;
+    Node ex = utils::mkExtract(node, extract.high, extract.low);
+    return ex; 
   }
-  // if we haven't seen this node before it must not be sliced yet
-  if (d_nodeToId.find(node) == d_nodeToId.end()) {
-    return Base(utils::getSize(node)); 
+  // otherwise must be a top-level term 
+  Assert (hasNode(id));
+  return (d_idToNode.find(id))->second; 
+}
+
+bool Slicer::termInEqualityEngine(TermId id) {
+  Node node = getNode(id); 
+  return d_coreSolver->hasTerm(node); 
+}
+
+void Slicer::enqueueSplit(TermId id, Index i) {
+  Node node = getNode(id);
+  Node bottom = Rewriter::rewrite(utils::mkExtract(node, i -1 , 0));
+  Node top = Rewriter::rewrite(utils::mkExtract(node, utils::getSize(node) - 1, i));
+  Node eq = utils::mkNode(kind::EQUAL, node, utils::mkConcat(top, bottom));
+  d_newSplits.push_back(eq);
+  Debug("bv-slicer") << "Slicer::enqueueSplit " << eq << endl; 
+}
+
+void Slicer::getNewSplits(std::vector<Node>& splits) {
+  for (unsigned i = d_newSplitsIndex; i < d_newSplits.size(); ++i) {
+    splits.push_back(d_newSplits[i]);
   }
-  TermId id = d_nodeToId[node];
-  Base base(d_unionFind.getBitwidth(id));
-  d_unionFind.getBase(id, base, 0);
-  return base; 
+  d_newSplitsIndex = d_newSplits.size(); 
+}
+
+bool Slicer::hasExplanation(ExplanationId id) const {
+  return id < d_explanations.size(); 
+}
+
+TNode Slicer::getExplanation(ExplanationId id) const {
+  Assert(hasExplanation(id));
+  return d_explanations[id]; 
+}
+
+ExplanationId Slicer::getExplanationId(TNode reason) const {
+  Assert (d_explanationToId.find(reason) != d_explanationToId.end());
+  return d_explanationToId.find(reason)->second; 
 }
 
 std::string UnionFind::debugPrint(TermId id) {
diff --git a/src/theory/bv/slicer.h b/src/theory/bv/slicer.h
index 6e09d971b..6bbe2f467 100644
--- a/src/theory/bv/slicer.h
+++ b/src/theory/bv/slicer.h
@@ -32,7 +32,7 @@
 #include "context/context.h"
 #include "context/cdhashset.h"
 #include "context/cdo.h"
-
+#include "context/cdqueue.h"
 #ifndef __CVC4__THEORY__BV__SLICER_BV_H
 #define __CVC4__THEORY__BV__SLICER_BV_H
 
@@ -45,6 +45,7 @@ namespace bv {
 
 
 typedef Index TermId;
+typedef TermId ExplanationId; 
 extern const TermId UndefinedId;
 
 class CDBase; 
@@ -81,49 +82,9 @@ public:
     }
     return true; 
   }
-  friend class CDBase; 
 }; 
 
 
-class CDBase : public context::ContextNotifyObj {
-  context::Context* d_ctx;
-  context::CDO<unsigned> d_undoIndex;
-
-  std::vector<unsigned> d_undoStack; 
-  Base d_base;
-  CDBase(context::Context* ctx, Index bitwidth)
-    : ContextNotifyObj(ctx),
-      d_ctx(ctx),
-      d_undoIndex(d_ctx),
-      d_undoStack(),
-      d_base(bitwidth)
-  {}
-  void sliceAt(Index i) {
-    Assert (!d_base.isCutPoint(i)); 
-    d_undoStack.push_back(i);
-    d_undoIndex.set(d_undoIndex.get() + 1); 
-    d_base.sliceAt(i); 
-  }
-  bool isCutPoint(Index i) {
-    return d_base.isCutPoint(i); 
-  }
-  Index getBitwidth() const {return d_base.getBitwidth(); }
-  virtual ~CDBase() throw(AssertionException) {}
-  void contextNotifyPop() {
-    backtrack();
-  }
-
-  void backtrack() {
-    for (unsigned i = d_undoIndex.get(); i < d_undoStack.size(); ++i) {
-      Index i = d_undoStack.back();
-      d_undoStack.pop_back();
-      d_base.undoSliceAt(i); 
-    }
-    Assert(d_undoIndex.get() == d_undoStack.size()); 
-  }
-  
-}; 
-
 /**
  * UnionFind
  * 
@@ -135,6 +96,11 @@ struct ExtractTerm {
   TermId id;
   Index high;
   Index low;
+  ExtractTerm()
+    : id (UndefinedId),
+      high(UndefinedId),
+      low(UndefinedId)
+  {}
   ExtractTerm(TermId i, Index h, Index l)
     : id (i),
       high(h),
@@ -142,10 +108,24 @@ struct ExtractTerm {
   {
     Assert (h >= l && id != UndefinedId); 
   }
+  bool operator== (const ExtractTerm& other) const {
+    return id == other.id && high == other.high && low == other.low; 
+  }
   Index getBitwidth() const { return high - low + 1; }
   std::string debugPrint() const; 
+  friend class ExtractTermHashFunction; 
 };
 
+struct ExtractTermHashFunction {
+  ::std::size_t operator() (const ExtractTerm& t) const {
+    __gnu_cxx::hash<unsigned> h;
+    unsigned id = t.id;
+    unsigned high = t.high;
+    unsigned low = t.low; 
+    return (h(id) * 7919 + h(high))* 4391 + h(low); 
+  }
+}; 
+
 class UnionFind; 
 
 struct NormalForm {
@@ -168,21 +148,34 @@ struct NormalForm {
   void clear() { base.clear(); decomp.clear(); }
 };
 
+class Slicer; 
 
 class UnionFind : public context::ContextNotifyObj {
+
+  struct ReprEdge {
+    TermId repr;
+    ExplanationId reason;
+    ReprEdge()
+      : repr(UndefinedId),
+        reason(UndefinedId)
+    {}
+  }; 
+    
   class Node {
-    Index d_bitwidth;
-    TermId d_ch1, d_ch0;
-    TermId d_repr;
+    Index d_bitwidth;  
+    TermId d_ch1, d_ch0; // the ids of the two children if they exist
+    ReprEdge d_edge;     // points to the representative and stores the explanation
+    
   public:
     Node(Index b)
   : d_bitwidth(b),
     d_ch1(UndefinedId),
     d_ch0(UndefinedId), 
-    d_repr(UndefinedId)
+    d_edge()
     {}
-    
-    TermId getRepr() const { return d_repr; }
+
+    TermId getRepr() const { return d_edge.repr; }
+    ExplanationId getReason() const { return d_edge.reason; }
     Index getBitwidth() const { return d_bitwidth; }
     bool hasChildren() const { return d_ch1 != UndefinedId && d_ch0 != UndefinedId; }
 
@@ -190,9 +183,10 @@ class UnionFind : public context::ContextNotifyObj {
       Assert (i < 2);
       return i == 0? d_ch0 : d_ch1;
     }
-    void setRepr(TermId id) {
+    void setRepr(TermId repr, ExplanationId reason) {
       Assert (! hasChildren());
-      d_repr = id;
+      d_edge.repr = repr;
+      d_edge.reason = reason; 
     }
     void setChildren(TermId ch1, TermId ch0) {
       // Assert (d_repr == UndefinedId && !hasChildren());
@@ -204,16 +198,21 @@ class UnionFind : public context::ContextNotifyObj {
   
   /// map from TermId to the nodes that represent them 
   std::vector<Node> d_nodes;
-  /// a term is in this set if it is its own representative
-  //CDTermSet d_representatives;
+  __gnu_cxx::hash_map<TermId, ExtractTerm, __gnu_cxx::hash<TermId> > d_idToExtract;
+  __gnu_cxx::hash_map<ExtractTerm, TermId, ExtractTermHashFunction > d_extractToId;
   
   void getDecomposition(const ExtractTerm& term, Decomposition& decomp);
+  void getDecompositionWithExplanation(const ExtractTerm& term, Decomposition& decomp, std::vector<ExplanationId>& explanation);
   void handleCommonSlice(const Decomposition& d1, const Decomposition& d2, TermId common);
   /// getter methods for the internal nodes
   TermId getRepr(TermId id)  const {
     Assert (id < d_nodes.size());
     return d_nodes[id].getRepr(); 
   }
+  ExplanationId getReason(TermId id) const {
+    Assert (id < d_nodes.size());
+    return d_nodes[id].getReason(); 
+  }
   TermId getChild(TermId id, Index i) const {
     Assert (id < d_nodes.size());
     return d_nodes[id].getChild(i); 
@@ -225,10 +224,12 @@ class UnionFind : public context::ContextNotifyObj {
     Assert (id < d_nodes.size());
     return d_nodes[id].hasChildren(); 
   }
+  TermId getTopLevel(TermId id) const;
+  
   /// setter methods for the internal nodes
-  void setRepr(TermId id, TermId new_repr) {
+  void setRepr(TermId id, TermId new_repr, ExplanationId reason) {
     Assert (id < d_nodes.size());
-    d_nodes[id].setRepr(new_repr); 
+    d_nodes[id].setRepr(new_repr, reason); 
   }
   void setChildren(TermId id, TermId ch1, TermId ch0) {
     Assert ((ch1 == UndefinedId && ch0 == UndefinedId) ||
@@ -269,25 +270,32 @@ class UnionFind : public context::ContextNotifyObj {
     Statistics();
     ~Statistics();
   };
-
   Statistics d_statistics;
-  bool d_newSplit; 
+  Slicer* d_slicer; 
 public:
-  UnionFind(context::Context* ctx)
+  UnionFind(context::Context* ctx, Slicer* slicer)
     : ContextNotifyObj(ctx), 
       d_nodes(),
+      d_idToExtract(),
+      d_extractToId(), 
       d_undoStack(),
       d_undoStackIndex(ctx),
-      d_statistics()
+      d_statistics(),
+      d_slicer(slicer)
   {}
 
-  TermId addTerm(Index bitwidth);
-  void unionTerms(const ExtractTerm& t1, const ExtractTerm& t2); 
-  void merge(TermId t1, TermId t2);
-  TermId find(TermId t1); 
+  TermId addNode(Index bitwidth);
+  TermId addExtract(Index topLevel, Index high, Index low);
+  ExtractTerm getExtractTerm(TermId id) const;
+  bool isExtractTerm(TermId id) const; 
+  
+  void unionTerms(const ExtractTerm& t1, const ExtractTerm& t2, TermId reason); 
+  void merge(TermId t1, TermId t2, TermId reason);
+  TermId find(TermId t1);
+  TermId findWithExplanation(TermId id, std::vector<ExplanationId>& explanation); 
   void split(TermId term, Index i);
-
   void getNormalForm(const ExtractTerm& term, NormalForm& nf);
+  void getNormalFormWithExplanation(const ExtractTerm& term, NormalForm& nf, std::vector<ExplanationId>& explanation); 
   void alignSlicings(const ExtractTerm& term1, const ExtractTerm& term2);
   void ensureSlicing(const ExtractTerm& term);
   Index getBitwidth(TermId id) const {
@@ -300,34 +308,56 @@ public:
   void contextNotifyPop() {
     backtrack();
   }
-  bool hasNewSplit() { return d_newSplit; }
-  void resetNewSplit() { d_newSplit = false; } 
-
   friend class Slicer; 
 };
 
+class CoreSolver; 
+
 class Slicer {
-  __gnu_cxx::hash_map<TermId, TNode> d_idToNode;
+  __gnu_cxx::hash_map<TermId, TNode, __gnu_cxx::hash<TermId> > d_idToNode;
   __gnu_cxx::hash_map<TNode, TermId, TNodeHashFunction> d_nodeToId;
   __gnu_cxx::hash_map<TNode, bool, TNodeHashFunction> d_coreTermCache;
+  __gnu_cxx::hash_map<TNode, ExplanationId, TNodeHashFunction> d_explanationToId;
+  std::vector<TNode> d_explanations; 
   UnionFind d_unionFind;
-  ExtractTerm registerTerm(TNode node); 
+
+  context::CDQueue<Node> d_newSplits;
+  context::CDO<unsigned>  d_newSplitsIndex;
+  CoreSolver* d_coreSolver;
+  TermId d_termIdCount; 
 public:
-  Slicer(context::Context* ctx)
+  Slicer(context::Context* ctx, CoreSolver* coreSolver)
     : d_idToNode(),
       d_nodeToId(),
       d_coreTermCache(),
-      d_unionFind(ctx)
+      d_explanationToId(),
+      d_explanations(), 
+      d_unionFind(ctx, this),
+      d_newSplits(ctx),
+      d_newSplitsIndex(ctx, 0),
+      d_coreSolver(coreSolver)
   {}
   
-  void getBaseDecomposition(TNode node, std::vector<Node>& decomp);
+  void getBaseDecomposition(TNode node, std::vector<Node>& decomp, std::vector<TNode>& explanation);
+  void registerEquality(TNode eq);
+  ExtractTerm registerTerm(TNode node);
   void processEquality(TNode eq);
+  void assertEquality(TNode eq);
   bool isCoreTerm (TNode node);
-  Base getTopLevelBase(TNode node); 
+
+  bool hasNode(TermId id) const; 
+  Node  getNode(TermId id) const;
+  TermId getId(TNode node) const;
+
+  bool hasExplanation(ExplanationId id) const;
+  TNode getExplanation(ExplanationId id) const;
+  ExplanationId getExplanationId(TNode reason) const;
+  
+  bool termInEqualityEngine(TermId id); 
+  void enqueueSplit(TermId id, Index i);
+  void getNewSplits(std::vector<Node>& splits);
   static void splitEqualities(TNode node, std::vector<Node>& equalities);
   static unsigned d_numAddedEqualities;
-  inline bool hasNewSplit() { return d_unionFind.hasNewSplit(); }
-  inline void resetNewSplit() { d_unionFind.resetNewSplit();  } 
 }; 
 
 
diff --git a/src/theory/bv/theory_bv.cpp b/src/theory/bv/theory_bv.cpp
index 5d034287d..ed1ba40a8 100644
--- a/src/theory/bv/theory_bv.cpp
+++ b/src/theory/bv/theory_bv.cpp
@@ -40,15 +40,16 @@ TheoryBV::TheoryBV(context::Context* c, context::UserContext* u, OutputChannel&
     d_context(c),
     d_alreadyPropagatedSet(c),
     d_sharedTermsSet(c),
-    d_slicer(c),
     d_bitblastSolver(c, this),
-    d_coreSolver(c, this, &d_slicer),
+    d_coreSolver(c, this),
     d_statistics(),
     d_conflict(c, false),
     d_literalsToPropagate(c),
     d_literalsToPropagateIndex(c, 0),
     d_propagatedBy(c)
-  {}
+  {
+    
+  }
 
 TheoryBV::~TheoryBV() {}
 
@@ -289,7 +290,6 @@ void TheoryBV::addSharedTerm(TNode t) {
 }
 
 
-
 EqualityStatus TheoryBV::getEqualityStatus(TNode a, TNode b)
 {
   if (options::bitvectorEagerBitblast()) {
diff --git a/src/theory/bv/theory_bv.h b/src/theory/bv/theory_bv.h
index 3e14584ed..d457571e2 100644
--- a/src/theory/bv/theory_bv.h
+++ b/src/theory/bv/theory_bv.h
@@ -44,8 +44,8 @@ class TheoryBV : public Theory {
   context::CDHashSet<Node, NodeHashFunction> d_alreadyPropagatedSet;
   context::CDHashSet<Node, NodeHashFunction> d_sharedTermsSet;
 
-  Slicer         d_slicer;
   BitblastSolver d_bitblastSolver;
+  // TODO generalize to multiple subtheories 
   CoreSolver     d_coreSolver;
   
 public:
diff --git a/test/regress/regress0/bv/core/incremental.smt b/test/regress/regress0/bv/core/incremental.smt
new file mode 100644
index 000000000..3a9ff85e0
--- /dev/null
+++ b/test/regress/regress0/bv/core/incremental.smt
@@ -0,0 +1,24 @@
+(benchmark ext_con_004_004_0016.smt
+:logic QF_BV
+:extrafuns ((v4 BitVec[16]))
+:extrafuns ((dummy4 BitVec[1]))
+:extrafuns ((a BitVec[16]))
+:status unknown
+:formula
+(flet ($n1 true)
+(let (?n2 (extract[15:13] a))
+(let (?n3 (extract[15:14] v4))
+(let (?n4 (concat ?n3 dummy4))
+(flet ($n5 (= ?n2 ?n4))
+(let (?n6 (extract[14:12] a))
+(let (?n7 (extract[13:12] v4))
+(let (?n8 (concat dummy4 ?n7))
+(flet ($n9 (= ?n6 ?n8))
+(flet ($n10 (and $n5 $n9))
+(let (?n11 (extract[14:14] v4))
+(let (?n12 (extract[13:13] v4))
+(flet ($n13 (= ?n11 ?n12))
+(flet ($n14 (not $n13))
+(flet ($n15 (and $n1 $n1 $n1 $n10 $n14))
+$n15
+))))))))))))))))