ported my bv-core branch from svn to git

15 files changed, 1306 insertions, 30 deletions

diff --git a/src/theory/bv/Makefile.am b/src/theory/bv/Makefile.am
index 669cbe9e0..686cc7e83 100644
--- a/src/theory/bv/Makefile.am
+++ b/src/theory/bv/Makefile.am
@@ -13,12 +13,16 @@ libbv_la_SOURCES = \
 	bitblaster.h \
 	bitblaster.cpp \
 	bv_subtheory.h \
- 	bv_subtheory_eq.h \
+	bv_subtheory_eq.h \
 	bv_subtheory_eq.cpp \
+	bv_subtheory_core.h \
+	bv_subtheory_core.cpp \
 	bv_subtheory_bitblast.h \
 	bv_subtheory_bitblast.cpp \
 	bitblast_strategies.h \
 	bitblast_strategies.cpp \
+	slicer.h \
+	slicer.cpp \
 	theory_bv.h \
 	theory_bv.cpp \
 	theory_bv_rewrite_rules.h \
diff --git a/src/theory/bv/bitblast_strategies.cpp b/src/theory/bv/bitblast_strategies.cpp
index fbf9a45ee..bd76dd6d4 100644
--- a/src/theory/bv/bitblast_strategies.cpp
+++ b/src/theory/bv/bitblast_strategies.cpp
@@ -346,7 +346,7 @@ void DefaultVarBB (TNode node, Bits& bits, Bitblaster* bb) {
     BVDebug("bitvector-bb") << "                           with bits  " << toString(bits); 
   }
 
-   bb->storeVariable(node);
+  bb->storeVariable(node);
 }
 
 void DefaultConstBB (TNode node, Bits& bits, Bitblaster* bb) {
diff --git a/src/theory/bv/bitblaster.h b/src/theory/bv/bitblaster.h
index 21b389508..fb4394673 100644
--- a/src/theory/bv/bitblaster.h
+++ b/src/theory/bv/bitblaster.h
@@ -164,9 +164,9 @@ public:
   }
 
   bool isSharedTerm(TNode node);
-private:
 
-  
+private:
+ 
   class Statistics {
   public:
     IntStat d_numTermClauses, d_numAtomClauses;
diff --git a/src/theory/bv/bv_subtheory.h b/src/theory/bv/bv_subtheory.h
index 4dbba0797..a256b6001 100644
--- a/src/theory/bv/bv_subtheory.h
+++ b/src/theory/bv/bv_subtheory.h
@@ -33,7 +33,8 @@ namespace bv {
 
 enum SubTheory {
   SUB_EQUALITY = 1,
-  SUB_BITBLAST = 2
+  SUB_BITBLAST = 2,
+  SUB_CORE = 3
 };
 
 inline std::ostream& operator << (std::ostream& out, SubTheory subtheory) {
diff --git a/src/theory/bv/bv_subtheory_core.cpp b/src/theory/bv/bv_subtheory_core.cpp
new file mode 100644
index 000000000..2252fc274
--- /dev/null
+++ b/src/theory/bv/bv_subtheory_core.cpp
@@ -0,0 +1,251 @@
+/*********************                                                        */
+/*! \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/bv/slicer.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;
+
+CoreSolver::CoreSolver(context::Context* c, TheoryBV* bv, Slicer* slicer)
+  : SubtheorySolver(c, bv),
+    d_notify(*this),
+    d_equalityEngine(d_notify, c, "theory::bv::TheoryBV"),
+    d_assertions(c),
+    d_slicer(slicer),
+    d_isCoreTheory(c, true)
+{
+  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 CoreSolver::setMasterEqualityEngine(eq::EqualityEngine* eq) {
+  d_equalityEngine.setMasterEqualityEngine(eq);
+}
+
+void CoreSolver::preRegister(TNode node) {
+  if (!d_useEqualityEngine)
+    return;
+
+  if (node.getKind() == kind::EQUAL) {
+      d_equalityEngine.addTriggerEquality(node);
+  } else {
+    d_equalityEngine.addTerm(node);
+  }
+}
+
+
+void CoreSolver::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 CoreSolver::decomposeFact(TNode fact) {
+  Debug("bv-slicer") << "CoreSolver::decomposeFact fact=" << fact << endl;  
+  // FIXME: are this the right things to assert? 
+  // assert decompositions since the equality engine does not know the semantics of
+  // 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]; 
+  std::vector<Node> a_decomp;
+  std::vector<Node> b_decomp;
+  d_slicer->getBaseDecomposition(a, a_decomp);
+  d_slicer->getBaseDecomposition(b, b_decomp);
+
+  Assert (a_decomp.size() == b_decomp.size());
+  
+  Node new_a = utils::mkConcat(a_decomp);
+  Node new_b = utils::mkConcat(b_decomp);
+
+  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 = assertFact(a_eq_new_a, utils::mkTrue());
+  if (!ok) return false; 
+  ok = assertFact(b_eq_new_b, utils::mkTrue());
+  if (!ok) return false; 
+  ok = assertFact(fact, fact);
+  if (!ok) return false;
+  
+  if (fact.getKind() == kind::EQUAL) {
+    // assert the individual equalities as well
+    //    a_i == b_i
+    for (unsigned i = 0; i < a_decomp.size(); ++i) {
+      Node eq_i = nm->mkNode(kind::EQUAL, a_decomp[i], b_decomp[i]);
+      ok = assertFact(eq_i, fact);
+      if (!ok) return false; 
+    }
+  }
+  return true; 
+}
+
+bool CoreSolver::addAssertions(const std::vector<TNode>& assertions, Theory::Effort e) {
+  Trace("bitvector::core") << "CoreSolver::addAssertions \n";
+  Assert (!d_bv->inConflict());
+
+  bool ok = true; 
+  std::vector<Node> core_eqs;
+  for (unsigned i = 0; i < assertions.size(); ++i) {
+    TNode fact = assertions[i];
+    
+    // update whether we are in the core fragment
+    // FIXME: move isCoreTerm into CoreSolver
+    if (d_isCoreTheory && !d_slicer->isCoreTerm(fact)) {
+      d_isCoreTheory = false; 
+    }
+    ok = decomposeFact(fact);
+    if (!ok)
+      return false; 
+  }
+
+  return true;
+}
+
+bool CoreSolver::assertFact(TNode fact, TNode reason) {
+  Debug("bv-slicer") << "CoreSolver::assertFact fact=" << fact << endl;
+  Debug("bv-slicer") << "                     reason=" << reason << endl;
+  // 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) {
+      if (negated) {
+        // dis-equality
+        d_equalityEngine.assertEquality(predicate, false, reason);
+      } else {
+        // equality
+        d_equalityEngine.assertEquality(predicate, true, reason);
+      }
+    } else {
+      // Adding predicate if the congruence over it is turned on
+      if (d_equalityEngine.isFunctionKind(predicate.getKind())) {
+        d_equalityEngine.assertPredicate(predicate, !negated, reason);
+      }
+    }
+  }
+
+  // checking for a conflict
+  if (d_bv->inConflict()) {
+    return false;
+  }  
+  return true; 
+}
+
+bool CoreSolver::NotifyClass::eqNotifyTriggerEquality(TNode equality, bool value) {
+  BVDebug("bitvector::core") << "NotifyClass::eqNotifyTriggerEquality(" << equality << ", " << (value ? "true" : "false" )<< ")" << std::endl;
+  if (value) {
+    return d_solver.storePropagation(equality);
+  } else {
+    return d_solver.storePropagation(equality.notNode());
+  }
+}
+
+bool CoreSolver::NotifyClass::eqNotifyTriggerPredicate(TNode predicate, bool value) {
+  BVDebug("bitvector::core") << "NotifyClass::eqNotifyTriggerPredicate(" << predicate << ", " << (value ? "true" : "false" ) << ")" << std::endl;
+  if (value) {
+    return d_solver.storePropagation(predicate);
+  } else {
+    return d_solver.storePropagation(predicate.notNode());
+  }
+}
+
+bool CoreSolver::NotifyClass::eqNotifyTriggerTermEquality(TheoryId tag, TNode t1, TNode t2, bool value) {
+  Debug("bitvector::core") << "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 CoreSolver::NotifyClass::eqNotifyConstantTermMerge(TNode t1, TNode t2) {
+  d_solver.conflict(t1, t2);
+}
+
+bool CoreSolver::storePropagation(TNode literal) {
+  return d_bv->storePropagation(literal, SUB_EQUALITY);
+}
+  
+void CoreSolver::conflict(TNode a, TNode b) {
+  std::vector<TNode> assumptions;
+  d_equalityEngine.explainEquality(a, b, true, assumptions);
+  d_bv->setConflict(mkAnd(assumptions));
+}
+
+void CoreSolver::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") << "CoreSolver::collectModelInfo (assert "
+                               << *it << ")\n";
+    }
+  }
+  set<Node> termSet;
+  d_bv->computeRelevantTerms(termSet);
+  m->assertEqualityEngine(&d_equalityEngine, &termSet);
+}
diff --git a/src/theory/bv/bv_subtheory_core.h b/src/theory/bv/bv_subtheory_core.h
new file mode 100644
index 000000000..20b42d61c
--- /dev/null
+++ b/src/theory/bv/bv_subtheory_core.h
@@ -0,0 +1,104 @@
+/*********************                                                        */
+/*! \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"
+#include "context/cdhashmap.h"
+
+namespace CVC4 {
+namespace theory {
+namespace bv {
+
+class Slicer; 
+
+/**
+ * Bitvector equality solver
+ */
+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;
+
+  public:
+    NotifyClass(CoreSolver& 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;
+  Slicer* d_slicer;
+  context::CDO<bool> d_isCoreTheory;
+
+  bool assertFact(TNode fact, TNode reason);  
+  bool decomposeFact(TNode fact);
+public:
+  bool isCoreTheory() {return d_isCoreTheory; }
+  CoreSolver(context::Context* c, TheoryBV* bv, Slicer* slicer);
+  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/kinds b/src/theory/bv/kinds
index 2faa12437..052e477ea 100644
--- a/src/theory/bv/kinds
+++ b/src/theory/bv/kinds
@@ -8,7 +8,7 @@ theory THEORY_BV ::CVC4::theory::bv::TheoryBV "theory/bv/theory_bv.h"
 typechecker "theory/bv/theory_bv_type_rules.h"
 
 properties finite
-properties check propagate
+properties check propagate presolve
 
 rewriter ::CVC4::theory::bv::TheoryBVRewriter "theory/bv/theory_bv_rewriter.h"
 
diff --git a/src/theory/bv/slicer.cpp b/src/theory/bv/slicer.cpp
new file mode 100644
index 000000000..73cad53b8
--- /dev/null
+++ b/src/theory/bv/slicer.cpp
@@ -0,0 +1,474 @@
+/*********************                                                        */
+/*! \file slicer.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 Bitvector theory.
+ **
+ ** Bitvector theory.
+ **/
+
+#include "theory/bv/slicer.h"
+#include "util/integer.h"
+#include "util/utility.h"
+#include "theory/bv/theory_bv_utils.h"
+#include "theory/rewriter.h"
+
+using namespace CVC4;
+using namespace CVC4::theory;
+using namespace CVC4::theory::bv;
+using namespace std; 
+
+void Base::decomposeNode(TNode node, std::vector<Node>& decomp) {
+  Debug("bv-slicer") << "Base::decomposeNode " << node << "\n with base" << debugPrint() << endl;
+  Index low = 0;
+  Index high = utils::getSize(node) - 1; 
+  if (node.getKind() == kind::BITVECTOR_EXTRACT) {
+    low = utils::getExtractLow(node);
+    high = utils::getExtractHigh(node);
+    node = node[0];
+  }
+  Index index = low; 
+  for (Index i = low; i <= high; ++i) {
+    if (isCutPoint(i)) {
+      // make sure the extract is pushed down before concat
+      Node slice = Rewriter::rewrite(utils::mkExtract(node, i, index));
+      index = i + 1;
+      decomp.push_back(slice);
+      Debug("bv-slicer") << slice <<" "; 
+    }
+  }
+  Debug("bv-slicer") << endl; 
+}
+
+/** 
+ * Adds a cutPoint at Index i and splits the corresponding Splinter
+ * 
+ * @param i the index where the cut point will be introduced
+ * @param sp the splinter pointer corresponding to the splinter to be sliced
+ * @param low_splinter the resulting bottom part of the splinter
+ * @param top_splinter the resulting top part of the splinter
+ */
+void Slice::split(Index i, SplinterPointer& sp, Splinter*& low_splinter, Splinter*& top_splinter) {
+  Debug("bv-slicer") << "Slice::split " << this->debugPrint() << "\n"; 
+  Assert (!d_base.isCutPoint(i));
+  d_base.sliceAt(i);
+  
+  Splinter* s = NULL;
+  Slice::const_iterator it = begin();
+  bool lt, gt; 
+  for (; it != end(); ++it) {
+    lt = (it->second)->getHigh() >= i;
+    gt = (it->second)->getLow() <= i;
+    if (gt && lt) {
+      s = it->second;
+      break; 
+    }
+  }
+  
+  Assert (s != NULL);
+
+  sp = s->getPointer();
+  Index low = s->getLow();
+  Index high = s->getHigh();
+  // creating the two splinter fragments 
+  low_splinter = new Splinter(i, low);
+  top_splinter = new Splinter(high, i+1);
+  
+  addSplinter(low, low_splinter);
+  addSplinter(i+1, top_splinter);
+  Debug("bv-slicer") << "          to " << this->debugPrint() << "\n"; 
+} 
+ 
+void Slice::addSplinter(Index i, Splinter* sp) {
+  Assert (i == sp->getLow() && sp->getHigh() < d_bitwidth);
+
+  if (i != 0) {
+    d_base.sliceAt(i - 1);
+  }
+  d_base.debugPrint(); 
+  // free the memory associated with the previous splinter
+  if (d_splinters.find(i) != d_splinters.end()) {
+    delete d_splinters[i];
+  }
+  d_splinters[i] = sp;
+}
+
+std::string Slice::debugPrint() {
+  std::ostringstream os;
+  os << d_base.debugPrint(); 
+  os << "{ ";
+  for (Slice::const_iterator it = begin(); it != end(); ++it) {
+    Splinter* s = (*it).second;
+    os << "[" << s->getLow() << ":" << s->getHigh() <<"]"; 
+    Assert ((*it).first == s->getLow());
+    Assert (s->getLow() == 0 || d_base.isCutPoint(s->getLow() - 1)); 
+    SplinterPointer sp = s->getPointer(); 
+    if (s->getPointer() != Undefined) {
+      os << "->" << sp.debugPrint(); 
+    }
+    os << " "; 
+  }
+  os << "}";
+  return os.str(); 
+}
+
+void SliceBlock::computeBlockBase(std::vector<RootId>& queue)  {
+  Debug("bv-slicer") << "SliceBlock::computeBlockBase for block" << d_rootId << endl;
+  Debug("bv-slicer") << this->debugPrint() << endl; 
+
+  // at this point d_base has all the cut points in the individual slices
+  for (unsigned row = 0; row < d_block.size(); ++row) {
+    Slice* slice = d_block[row];
+    const Base base = slice->getBase();
+    Base new_cut_points = base.diffCutPoints(d_base);
+    // use the cut points from the base to split the current slice
+    for (unsigned i = 0; i < d_bitwidth; ++i) {
+      if (new_cut_points.isCutPoint(i) && i != d_bitwidth - 1) {
+        Debug("bv-slicer") << "    adding cut point at " << i << " for row " << row << endl; 
+        // split this slice (this updates the slice's base)
+        Splinter* bottom, *top = NULL;
+        SplinterPointer sp;
+        slice->split(i, sp, bottom, top);
+          
+        if (sp != Undefined) {
+          // if we do need to split something else split it
+          Debug("bv-slicer") <<"    must split " << sp.debugPrint(); 
+          Slice* slice = d_slicer->getSlice(sp);
+          Splinter* s = d_slicer->getSplinter(sp);
+          Index cutPoint = s->getLow() + i; 
+          Splinter* new_bottom = new Splinter(cutPoint, s->getLow());
+          Splinter* new_top = new Splinter(s->getHigh(), cutPoint + 1);
+          new_bottom->setPointer(SplinterPointer(d_rootId, row, bottom->getLow()));
+          new_top->setPointer(SplinterPointer(d_rootId, row, top->getLow()));
+
+          slice->addSplinter(new_bottom->getLow(), new_bottom);
+          slice->addSplinter(new_top->getLow(), new_top); 
+          
+          bottom->setPointer(SplinterPointer(sp.term, sp.row, new_bottom->getLow()));
+          top->setPointer(SplinterPointer(sp.term, sp.row, new_top->getLow()));
+          // update base for block
+          d_slicer->getSliceBlock(sp)->sliceBaseAt(cutPoint);
+          // add to queue of blocks that have changed base
+          Debug("bv-slicer") << "    adding block to queue: " << sp.term << endl; 
+          queue.push_back(sp.term); 
+        }
+      }
+    }
+  }
+
+  Debug("bv-slicer") << "base computed: " << d_rootId << endl;
+  Debug("bv-slicer") << this->debugPrint() << endl;
+  Debug("bv-slicer") << "SliceBlock::computeBlockBase done. \n"; 
+
+}
+
+std::string SliceBlock::debugPrint() {
+  std::ostringstream os;
+  os << "Width " << d_bitwidth << endl; 
+  os << "Base " << d_base.debugPrint() << endl;
+  for (SliceBlock::const_iterator it = begin(); it!= end(); ++it) {
+    os << (*it)->debugPrint() << endl;
+  }
+  return os.str(); 
+}
+
+Slicer::Slicer()
+  : d_simpleEqualities(),
+    d_roots(),
+    d_numRoots(0),
+    d_nodeRootMap(),
+    d_rootBlocks(),
+    d_coreTermCache()
+{}
+
+RootId Slicer::makeRoot(TNode n)  {
+  Assert (n.getKind() != kind::BITVECTOR_EXTRACT && n.getKind() != kind::BITVECTOR_CONCAT);
+  if (d_nodeRootMap.find(n) != d_nodeRootMap.end()) {
+    return d_nodeRootMap[n];
+  }
+  RootId id = d_roots.size();
+  d_nodeRootMap[n] = id; 
+  d_roots.push_back(n); 
+  d_rootBlocks.push_back(new SliceBlock(id, utils::getSize(n), this));
+  Assert (d_roots.size() == d_rootBlocks.size());
+  
+  Debug("bv-slicer") << "Slicer::makeRoot " << n << " -> " << id << endl;
+  return id; 
+}
+
+void Slicer::splitEqualities(TNode node, std::vector<Node>& equalities) {
+  Assert (node.getKind() == kind::EQUAL);
+  TNode t1 = node[0];
+  TNode t2 = node[1];
+
+  uint32_t width = utils::getSize(t1); 
+  
+  Base base1(width); 
+  if (t1.getKind() == kind::BITVECTOR_CONCAT) {
+    unsigned size = 0; 
+    for (int i = t1.getNumChildren(); i >= 0; --i) {
+      size = size + utils::getSize(t1[i]);
+      base1.sliceAt(size); 
+    }
+  }
+
+  Base base2(width); 
+  if (t2.getKind() == kind::BITVECTOR_CONCAT) {
+    unsigned size = 0; 
+    for (int i = t2.getNumChildren(); i >= 0; --i) {
+      size = size + utils::getSize(t2[i]);
+      base2.sliceAt(size); 
+    }
+  }
+
+  base1.sliceWith(base2); 
+  if (base1 != Base(width)) {
+    // we split the equalities according to the base
+    int last = 0; 
+    for (unsigned i = 1; i < utils::getSize(t1); ++i) {
+      if (base1.isCutPoint(i)) {
+        Node extract1 = Rewriter::rewrite(utils::mkExtract(t1, last, i - 1));
+        Node extract2 = Rewriter::rewrite(utils::mkExtract(t2, last, i - 1));
+        last = i;
+        Assert (utils::getSize(extract1) == utils::getSize(extract2)); 
+        equalities.push_back(utils::mkNode(kind::EQUAL, extract1, extract2)); 
+      }
+    }
+  } else {
+    // just return same equality
+    equalities.push_back(node);
+  }
+} 
+ 
+void Slicer::processEquality(TNode node) {
+  Assert (node.getKind() == kind::EQUAL);
+  Debug("bv-slicer") << "theory::bv::Slicer::processEquality " << node << endl; 
+  std::vector<Node> equalities;
+  splitEqualities(node, equalities); 
+  for (unsigned i = 0; i < equalities.size(); ++i) {
+    Debug("bv-slicer") << "    splitEqualities " << node << endl;
+    registerSimpleEquality(equalities[i]); 
+    d_simpleEqualities.push_back(equalities[i]);
+  }
+}
+
+void Slicer::registerSimpleEquality(TNode eq) {
+  Assert (eq.getKind() == kind::EQUAL);
+  Debug("bv-slicer") << "theory::bv::Slicer::registerSimpleEquality " << eq << endl;  
+  TNode a = eq[0];
+  TNode b = eq[1];
+ 
+  RootId id_a = registerTerm(a);
+  RootId id_b = registerTerm(b);
+  
+  unsigned low_a = 0; 
+  unsigned low_b = 0; 
+
+  if (a.getKind() == kind::BITVECTOR_EXTRACT) {
+    low_a  = utils::getExtractLow(a);
+  }
+  
+  if (b.getKind() == kind::BITVECTOR_EXTRACT) {
+    low_b  = utils::getExtractLow(b);
+  }
+
+  if (id_a == id_b) {
+    // we are in the special case a[i0:j0] = a[i1:j1]
+    Index high_a = utils::getExtractHigh(a);
+    Index high_b = utils::getExtractHigh(b);
+    
+    unsigned intersection_low = std::max(low_a, low_b);
+    unsigned intersection_high = std::min(high_a, high_b);
+    if (intersection_low <= intersection_high) {
+      // if the two extracts intersect 
+      unsigned intersection_size = intersection_high - intersection_low + 1;
+      // gcd between overlapping area and difference
+      unsigned diff = low_a > low_b ? low_a - low_b  : low_b - low_a; 
+      unsigned granularity = gcd(intersection_size, diff);
+      SliceBlock* block_a = d_rootBlocks[id_a];
+      Assert (a.getKind() == kind::BITVECTOR_EXTRACT);
+      unsigned size = utils::getSize(a[0]);
+      
+      Slice* slice = new Slice(size);
+      unsigned low = low_a > low_b ? low_b : low_a;
+      unsigned high = high_a > high_b ? high_a : high_b;
+      Splinter* prev_splinter = NULL;
+      // the row the new slice will be in 
+      unsigned block_row = block_a->getSize(); 
+      for (unsigned i = low; i < high; i+=granularity) {
+        Splinter* s = new Splinter(i+ granularity-1, i);
+        slice->addSplinter(i, s);
+        // update splinter pointers to reflect entailed equalities 
+        if (prev_splinter!= NULL) {
+          // the previous splinter will be equal to the current 
+          prev_splinter->setPointer(SplinterPointer(id_a, block_row, i));
+        }
+        prev_splinter = s; 
+      }
+      // make sure to splinters for the extremities
+      if (low!= 0) {
+        Splinter* s = new Splinter(low -1 , 0);
+        slice->addSplinter(0, s); 
+      }
+      if (high + granularity <= size) {
+        Splinter* s = new Splinter(size - 1, high + 1);
+        slice->addSplinter(high+1, s); 
+      }
+      block_a->addSlice(slice);
+      return; 
+    }
+  }
+  
+  Slice* slice_a = makeSlice(a);
+  Slice* slice_b = makeSlice(b); 
+
+  SliceBlock* block_a = d_rootBlocks[id_a];
+  SliceBlock* block_b = d_rootBlocks[id_b];
+
+  uint32_t row_a = block_a->addSlice(slice_a);
+  uint32_t row_b = block_b->addSlice(slice_b); 
+
+  SplinterPointer sp_a = SplinterPointer(id_a, row_a, low_a);
+  SplinterPointer sp_b = SplinterPointer(id_b, row_b, low_b); 
+
+  slice_a->getSplinter(low_a)->setPointer(sp_b);
+  slice_b->getSplinter(low_b)->setPointer(sp_a); 
+}
+
+Slice* Slicer::makeSlice(TNode node) {
+  //Assert (d_sliceSet.find(node) == d_sliceSet.end());
+  
+  Index bitwidth = utils::getSize(node); 
+  Index low = 0;
+  Index high = bitwidth -1;
+  if (node.getKind() == kind::BITVECTOR_EXTRACT) {
+    low  = utils::getExtractLow(node);
+    high = utils::getExtractHigh(node);
+    bitwidth = utils::getSize(node[0]); 
+  }
+  Splinter* splinter = new Splinter(high, low);
+  Slice* slice = new Slice(bitwidth);
+  slice->addSplinter(low, splinter);
+  if (low != 0) {
+    Splinter* bottom_splinter = new Splinter(low-1, 0);
+    slice->addSplinter(0, bottom_splinter); 
+  }
+  if (high != bitwidth - 1) {
+    Splinter* top_splinter = new Splinter(bitwidth - 1, high + 1);
+    slice->addSplinter(high+1, top_splinter); 
+  }
+  return slice; 
+}
+
+
+RootId Slicer::registerTerm(TNode node) {
+  if (node.getKind() == kind::BITVECTOR_EXTRACT ) {
+    node = node[0];
+    Assert (isRootTerm(node)); 
+  }
+  // setting up the data-structures for the root term
+  RootId id = makeRoot(node);
+  return id; 
+}
+
+bool Slicer::isCoreTerm(TNode node) {
+  if (d_coreTermCache.find(node) == d_coreTermCache.end()) {
+    Kind kind = node.getKind(); 
+    if (kind != kind::BITVECTOR_EXTRACT &&
+        kind != kind::BITVECTOR_CONCAT &&
+        kind != kind::EQUAL && kind != kind::NOT) {
+      d_coreTermCache[node] = false;
+      return false; 
+    } else {
+      // we need to recursively check whether the term is a root term or not
+      bool isCore = true;
+      for (unsigned i = 0; i < node.getNumChildren(); ++i) {
+        isCore = isCore && isCoreTerm(node[i]); 
+      }
+      d_coreTermCache[node] = isCore;
+      return isCore; 
+    }
+  }
+  return d_coreTermCache[node]; 
+}
+
+bool Slicer::isRootTerm(TNode node) {
+  Kind kind = node.getKind();
+  return kind != kind::BITVECTOR_EXTRACT && kind != kind::BITVECTOR_CONCAT;
+}
+
+// Base Slicer::getBase(TNode node) {
+//   Assert (d_bases.find(node) != d_bases.end());
+//   return d_bases[node]; 
+// }
+
+// void Slicer::updateBase(TNode node, const Base& base) {
+//   Assert (d_bases.find(node) != d_bases.end());
+//   d_bases[node] = d_bases[node].bitwiseOr(base); 
+// }
+
+
+void Slicer::computeCoarsestBase() {
+  Debug("bv-slicer") << "theory::bv::Slicer::computeCoarsestBase " << endl; 
+  std::vector<RootId> queue;
+  for (unsigned i = 0; i < d_rootBlocks.size(); ++i) {
+    SliceBlock* block = d_rootBlocks[i];
+    block->computeBlockBase(queue);
+  }
+
+  Debug("bv-slicer") << " processing queue of size " << queue.size() << endl; 
+  while (!queue.empty()) {
+    // process split candidate
+    RootId current = queue.back();
+    queue.pop_back();
+    SliceBlock* block = d_rootBlocks[current];
+    block->computeBlockBase(queue); 
+  }
+  debugCheckBase(); 
+}
+
+
+void Slicer::getBaseDecomposition(TNode node, std::vector<Node>& decomp) {
+  TNode root = node.getKind() == kind::BITVECTOR_EXTRACT ? node[0] : node; 
+  Assert (isRootTerm(root)); 
+  Base base = getSliceBlock(getRootId(root))->getBase();
+  base.decomposeNode(node, decomp);
+}
+
+void Slicer::debugCheckBase() {
+  // iterate through blocks and check that the block base is the same as each slice base
+  for (unsigned i = 0; i < d_rootBlocks.size(); ++i) {
+    SliceBlock* block = d_rootBlocks[i];
+    Base block_base = block->getBase();
+    SliceBlock::const_iterator it = block->begin();
+    for (; it != block->end(); ++it) {
+      Slice* slice = *it;
+      Base diff_points = slice->getBase().diffCutPoints(block_base);
+      Assert (diff_points == Base(block->getBitwidth()));
+      Slice::const_iterator slice_it = slice->begin();
+      for (; slice_it!= slice->end(); ++slice_it) {
+        Splinter* splinter = (*slice_it).second;
+        const SplinterPointer& sp = splinter->getPointer();
+        if (sp != Undefined) {
+          Splinter* other = getSplinter(sp);
+          Assert (splinter->getBitwidth() == other->getBitwidth());
+        }
+      }
+    }
+  }
+}
+
+
+
+
+
+
diff --git a/src/theory/bv/slicer.h b/src/theory/bv/slicer.h
new file mode 100644
index 000000000..33bc26b5a
--- /dev/null
+++ b/src/theory/bv/slicer.h
@@ -0,0 +1,373 @@
+/*********************                                                        */
+/*! \file slicer.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 Bitvector theory.
+ **
+ ** Bitvector theory.
+ **/
+
+#include "cvc4_private.h"
+
+#include <vector>
+#include <list>
+#include <ext/hash_map>
+#include "util/bitvector.h"
+#include "expr/node.h"
+#include "theory/bv/theory_bv_utils.h"
+#ifndef __CVC4__THEORY__BV__SLICER_BV_H
+#define __CVC4__THEORY__BV__SLICER_BV_H
+
+
+namespace CVC4 {
+
+namespace theory {
+namespace bv {
+
+typedef uint32_t RootId;
+typedef uint32_t SplinterId;
+typedef uint32_t Index;
+
+class Base {
+  uint32_t d_size;
+  CVC4::BitVector d_repr;  
+public:
+  Base(uint32_t size) 
+    : d_size(size) {
+    Assert (size > 1);
+    d_repr = BitVector(size - 1, 0u);
+  }
+
+  Base(const BitVector& repr) 
+    : d_size(repr.getSize() + 1),
+      d_repr(repr) {
+    Assert (d_size > 1);
+  }
+  
+  /** 
+   * Marks the base by adding a cut between index and index + 1
+   * 
+   * @param index 
+   */
+  void sliceAt(Index index) {
+    Assert (index < d_size - 1); 
+    d_repr = d_repr.setBit(index); 
+  }
+
+  void sliceWith(const Base& other) {
+    Assert (d_size == other.d_size); 
+    d_repr = d_repr | other.d_repr; 
+  }
+
+  void decomposeNode(TNode node, std::vector<Node>& decomp);
+
+  bool isCutPoint(Index index) {
+    Assert (index < d_size); 
+    // the last cut point is implicit
+    if (index == d_size - 1)
+      return true; 
+    return d_repr.isBitSet(index); 
+  }
+
+  Base diffCutPoints(const Base& other) const {
+    return Base(other.d_repr ^ d_repr); 
+  }
+
+  bool operator==(const Base& other) const {
+    return d_repr == other.d_repr; 
+  }
+  bool operator!=(const Base& other) const {
+    return !(*this == other); 
+  }
+  std::string debugPrint() {
+    std::ostringstream os;
+    os << "[";
+    bool first = true; 
+    for (Index i = 0; i < d_size - 1; ++i) {
+      if (isCutPoint(i)) {
+        if (first)
+          first = false;
+        else
+          os <<"| "; 
+        
+        os << i ; 
+      }
+    }
+    os << "]"; 
+    return os.str(); 
+  }
+  
+}; 
+
+
+struct SplinterPointer {
+  RootId term;
+  uint32_t row; 
+  Index index;
+
+  SplinterPointer()
+    : term(-1),
+      row(-1),
+      index(-1)
+  {}
+
+  SplinterPointer(RootId t, uint32_t r,  Index i)
+    : term(t),
+      row(r),
+      index(i)
+  {}
+  
+  bool operator==(const SplinterPointer& other) const {
+    return term == other.term && index == other.index && row == other.row; 
+  }
+  bool operator!=(const SplinterPointer& other) const {
+    return !(*this == other); 
+  }
+
+  std::string debugPrint() {
+    std::ostringstream os;
+    os << "(id" << term << ", row" << row <<", i" << index << ")";
+    return os.str();
+  }
+  
+};
+
+static const SplinterPointer Undefined = SplinterPointer(-1, -1, -1); 
+
+class Splinter {
+  // start and end indices in slice
+  Index d_low;
+  Index d_high;
+
+  // keeps track of splinter this splinter is equal to
+  // equal to Undefined if there is none
+  SplinterPointer d_pointer;
+  
+public:
+  Splinter(uint32_t high, uint32_t low) :
+    d_low(low),
+    d_high(high),
+    d_pointer(Undefined)
+  {
+    Assert (high >= low); 
+  }
+    
+  void setPointer(const SplinterPointer& pointer) {
+    Assert (d_pointer == Undefined);
+    d_pointer = pointer; 
+  }
+
+  const SplinterPointer& getPointer() const {
+    return d_pointer; 
+  }
+
+  Index getLow() const { return d_low; }
+  Index getHigh() const {return d_high; }
+  uint32_t getBitwidth() const { return d_high - d_low; }
+};
+
+class Slice {
+  uint32_t d_bitwidth; 
+  // map from the beginning of a splinter to the actual splinter id
+  std::map<Index, Splinter*> d_splinters;
+  Base d_base;
+  
+public:
+  Slice(uint32_t bitwidth)
+    : d_bitwidth(bitwidth),
+      d_splinters(),
+      d_base(bitwidth)
+  {}
+  /** 
+   * Split the slice by adding a cut point between indices i and i+1
+   * 
+   * @param i index where to cut
+   * @param id the id of the root term this slice belongs to
+   * @param row the row of the SliceBlock this Slice belongs to
+   */
+  void split(Index i, SplinterPointer& sp, Splinter*& low_splinter, Splinter*& top_splinter);
+  /** 
+   * Add splinter sp at Index i. If a splinter already exists there
+   * replace it and free the memory it occupied. 
+   * 
+   * @param i index where splinter starts
+   * @param sp new splinter
+   */
+  void addSplinter(Index i, Splinter* sp); 
+  /** 
+   * Return the splinter starting at Index start.
+   * 
+   * @param start 
+   * 
+   * @return 
+   */
+  Splinter* getSplinter (Index start) {
+    Assert (d_splinters.find(start) != d_splinters.end()); 
+    return d_splinters[start]; 
+  }
+  const Base& getBase() const { return d_base; }
+
+  typedef std::map<Index, Splinter*>::const_iterator const_iterator; 
+  std::map<Index, Splinter*>::const_iterator begin() {
+    return d_splinters.begin(); 
+  }
+  std::map<Index, Splinter*>::const_iterator end() {
+    return d_splinters.end(); 
+  }
+  std::string debugPrint(); 
+};
+
+class Slicer; 
+
+class SliceBlock {
+  uint32_t d_bitwidth; 
+  RootId d_rootId;                /**< the id of the root term this block corresponds to */
+  std::vector<Slice*> d_block;    /**< the slices in the block */
+  Base d_base;                    /**<  the base corresponding to this block containing all the cut points.
+                                   Invariant: the base should contain all the cut-points in the slices*/
+  Slicer* d_slicer; // FIXME: more elegant way to do this
+
+public:
+
+
+  SliceBlock(RootId rootId, uint32_t bitwidth, Slicer* slicer)
+    : d_bitwidth(bitwidth),
+      d_rootId(rootId),
+      d_block(),
+      d_base(bitwidth),
+      d_slicer(slicer)
+  {}
+
+  uint32_t addSlice(Slice* slice) {
+    // update the base with the cut-points in the slice
+    Debug("bv-slice") << "SliceBlock::addSlice Block"<< d_rootId << " adding slice " << slice->debugPrint() << std::endl; 
+    d_base.sliceWith(slice->getBase()); 
+    d_block.push_back(slice);
+    return d_block.size() - 1; 
+  }
+
+  Slice* getSlice(uint32_t row) const {
+    Assert (row < d_block.size()); 
+    return d_block[row]; 
+  }
+  /** 
+   * Propagate all the cut points in the Base to all the Slices. If one of the
+   * splinters that needs to get cut has a pointer to a splinter in a different
+   * block that splinter will also be split. 
+   * 
+   * @param queue other blocks that changed their base. 
+   */
+  void computeBlockBase(std::vector<RootId>& queue);
+
+  void sliceBaseAt(Index i) {
+    d_base.sliceAt(i); 
+  }
+  typedef std::vector<Slice*>::const_iterator const_iterator; 
+  std::vector<Slice*>::const_iterator begin() {
+    return d_block.begin(); 
+  }
+  std::vector<Slice*>::const_iterator end() {
+    return d_block.end(); 
+  }
+
+  uint32_t getBitwidth() const {
+    return d_bitwidth; 
+  }
+  Base& getBase() {
+    return d_base; 
+  }
+
+  unsigned getSize() const {
+    return d_block.size(); 
+  }
+  std::string debugPrint(); 
+};
+
+typedef __gnu_cxx::hash_map<TNode, bool, TNodeHashFunction> RootTermCache;
+
+typedef __gnu_cxx::hash_map<TNode, RootId, TNodeHashFunction> NodeRootIdMap;
+typedef std::vector<TNode> Roots; 
+
+typedef __gnu_cxx::hash_map<TNode, SplinterId, TNodeHashFunction> NodeSplinterIdMap;
+typedef std::vector<Splinter*> Splinters;
+
+typedef std::vector<SliceBlock*> SliceBlocks;
+
+class Slicer {
+  std::vector<TNode> d_simpleEqualities; /**< equalities of the form a[i0:j0] = b[i1:j1] */
+  Roots d_roots;
+  uint32_t d_numRoots; 
+  NodeRootIdMap d_nodeRootMap;
+  /* Indexed by Root Id */
+  SliceBlocks d_rootBlocks;
+  RootTermCache d_coreTermCache;
+public:
+  Slicer();
+  void computeCoarsestBase();
+  /** 
+   * Takes an equality that is of the following form:
+   *          a1 a2 ... an = b1 b2 ... bk
+   * where ai, and bi are either variables or extracts over variables,
+   * and consecutive extracts have been merged. 
+   * 
+   * @param node 
+   */
+  void processEquality(TNode node);
+  bool isCoreTerm(TNode node); 
+private:
+  void registerSimpleEquality(TNode node);
+  void splitEqualities(TNode node, std::vector<Node>& equalities);
+  TNode addSimpleTerm(TNode t);
+  bool isRootTerm(TNode node);
+
+  TNode getRoot(RootId id) {return d_roots[id]; }
+
+  RootId getRootId(TNode node) {
+    Assert (d_nodeRootMap.find(node) != d_nodeRootMap.end());
+    return d_nodeRootMap[node]; 
+  }
+
+  RootId registerTerm(TNode node); 
+  RootId makeRoot(TNode n);
+  Slice* makeSlice(TNode node);
+
+  void debugCheckBase(); 
+public:
+  Slice* getSlice(const SplinterPointer& sp) {
+    Assert (sp != Undefined); 
+    SliceBlock* sb = d_rootBlocks[sp.term];
+    return sb->getSlice(sp.row); 
+  }
+  
+  Splinter* getSplinter(const SplinterPointer& sp) {
+    Slice* slice = getSlice(sp);
+    return slice->getSplinter(sp.index); 
+  }
+
+  SliceBlock* getSliceBlock(RootId id) {
+    Assert (id < d_rootBlocks.size());
+    return d_rootBlocks[id]; 
+  }
+
+  SliceBlock* getSliceBlock(const SplinterPointer& sp) {
+    return getSliceBlock(sp.term); 
+  }
+
+  void getBaseDecomposition(TNode node, std::vector<Node>& decomp); 
+
+}; /* Slicer class */
+
+}/* CVC4::theory::bv namespace */
+}/* CVC4::theory namespace */
+}/* CVC4 namespace */
+
+#endif /* __CVC4__THEORY__BV__SLICER_BV_H */
diff --git a/src/theory/bv/theory_bv.cpp b/src/theory/bv/theory_bv.cpp
index 7acb93cc2..c4e16545f 100644
--- a/src/theory/bv/theory_bv.cpp
+++ b/src/theory/bv/theory_bv.cpp
@@ -17,6 +17,7 @@
 
 #include "theory/bv/theory_bv.h"
 #include "theory/bv/theory_bv_utils.h"
+#include "theory/bv/slicer.h"
 #include "theory/valuation.h"
 #include "theory/bv/bitblaster.h"
 #include "theory/bv/options.h"
@@ -39,8 +40,9 @@ TheoryBV::TheoryBV(context::Context* c, context::UserContext* u, OutputChannel&
     d_context(c),
     d_alreadyPropagatedSet(c),
     d_sharedTermsSet(c),
+    d_slicer(),
     d_bitblastSolver(c, this),
-    d_equalitySolver(c, this),
+    d_coreSolver(c, this, &d_slicer),
     d_statistics(),
     d_conflict(c, false),
     d_literalsToPropagate(c),
@@ -52,7 +54,7 @@ TheoryBV::~TheoryBV() {}
 
 
 void TheoryBV::setMasterEqualityEngine(eq::EqualityEngine* eq) {
-  d_equalitySolver.setMasterEqualityEngine(eq);
+  d_coreSolver.setMasterEqualityEngine(eq);
 }
 
 TheoryBV::Statistics::Statistics():
@@ -72,15 +74,19 @@ TheoryBV::Statistics::~Statistics() {
 }
 
 void TheoryBV::preRegisterTerm(TNode node) {
-  BVDebug("bitvector-preregister") << "TheoryBV::preRegister(" << node << ")" << std::endl;
+  Debug("bitvector-preregister") << "TheoryBV::preRegister(" << node << ")" << std::endl;
 
   if (options::bitvectorEagerBitblast()) {
     // don't use the equality engine in the eager bit-blasting
     return;
   }
 
+  if (node.getKind() == kind::EQUAL) {
+    d_slicer.processEquality(node); 
+  }
+  
   d_bitblastSolver.preRegister(node);
-  d_equalitySolver.preRegister(node);
+  d_coreSolver.preRegister(node);
 }
 
 void TheoryBV::sendConflict() {
@@ -88,7 +94,7 @@ void TheoryBV::sendConflict() {
   if (d_conflictNode.isNull()) {
     return;
   } else {
-    BVDebug("bitvector") << indent() << "TheoryBV::check(): conflict " << d_conflictNode;
+    Debug("bitvector") << indent() << "TheoryBV::check(): conflict " << d_conflictNode;
     d_out->conflict(d_conflictNode);
     d_statistics.d_avgConflictSize.addEntry(d_conflictNode.getNumChildren());
     d_conflictNode = Node::null();
@@ -97,7 +103,7 @@ void TheoryBV::sendConflict() {
 
 void TheoryBV::check(Effort e)
 {
-  BVDebug("bitvector") << "TheoryBV::check(" << e << ")" << std::endl;
+  Debug("bitvector") << "TheoryBV::check(" << e << ")" << std::endl;
 
   // if we are already in conflict just return the conflict
   if (inConflict()) {
@@ -111,17 +117,20 @@ void TheoryBV::check(Effort e)
     Assertion assertion = get();
     TNode fact = assertion.assertion;
     new_assertions.push_back(fact);
-    BVDebug("bitvector-assertions") << "TheoryBV::check assertion " << fact << "\n";
+    Debug("bitvector-assertions") << "TheoryBV::check assertion " << fact << "\n";
   }
 
   if (!inConflict()) {
     // sending assertions to the equality solver first
-    d_equalitySolver.addAssertions(new_assertions, e);
+    d_coreSolver.addAssertions(new_assertions, e);
   }
 
-  if (!inConflict()) {
-    // sending assertions to the bitblast solver
-    d_bitblastSolver.addAssertions(new_assertions, e);
+  // FIXME: this is not quite correct as it does not take into account cardinality constraints 
+  if (!d_coreSolver.isCoreTheory()) {
+    if (!inConflict()) {
+      // sending assertions to the bitblast solver
+      d_bitblastSolver.addAssertions(new_assertions, e);
+    }
   }
 
   if (inConflict()) {
@@ -132,13 +141,13 @@ void TheoryBV::check(Effort e)
 void TheoryBV::collectModelInfo( TheoryModel* m, bool fullModel ){
   Assert(!inConflict());
   //  Assert (fullModel); // can only query full model
-  d_equalitySolver.collectModelInfo(m); 
+  d_coreSolver.collectModelInfo(m); 
   d_bitblastSolver.collectModelInfo(m); 
   
 }
 
 void TheoryBV::propagate(Effort e) {
-  BVDebug("bitvector") << indent() << "TheoryBV::propagate()" << std::endl;
+  Debug("bitvector") << indent() << "TheoryBV::propagate()" << std::endl;
 
   if (inConflict()) {
     return;
@@ -152,7 +161,7 @@ void TheoryBV::propagate(Effort e) {
   }
 
   if (!ok) {
-    BVDebug("bitvector::propagate") << indent() << "TheoryBV::propagate(): conflict from theory engine" << std::endl;
+    Debug("bitvector::propagate") << indent() << "TheoryBV::propagate(): conflict from theory engine" << std::endl;
     setConflict();
   }
 }
@@ -184,7 +193,6 @@ Theory::PPAssertStatus TheoryBV::ppAssert(TNode in, SubstitutionMap& outSubstitu
   return PP_ASSERT_STATUS_UNSOLVED;
 }
 
-
 Node TheoryBV::ppRewrite(TNode t)
 {
   if (RewriteRule<BitwiseEq>::applies(t)) {
@@ -194,6 +202,10 @@ Node TheoryBV::ppRewrite(TNode t)
   return t;
 }
 
+void TheoryBV::presolve() {
+  Debug("bitvector") << "TheoryBV::presolve" << endl; 
+  d_slicer.computeCoarsestBase(); 
+}
 
 bool TheoryBV::storePropagation(TNode literal, SubTheory subtheory)
 {
@@ -224,7 +236,7 @@ bool TheoryBV::storePropagation(TNode literal, SubTheory subtheory)
   // * bitblaster needs to be left alone until it's done, otherwise it doesn't know how to explain
   // * equality engine can propagate eagerly
   bool ok = true;
-  if (subtheory == SUB_EQUALITY) {
+  if (subtheory == SUB_CORE) {
     d_out->propagate(literal);
     if (!ok) {
       setConflict();
@@ -239,19 +251,19 @@ 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)) {
-    BVDebug("bitvector::explain") << "TheoryBV::explain(" << literal << "): EQUALITY" << std::endl;
-    d_equalitySolver.explain(literal, assumptions);
+  if (propagatedBy(literal, SUB_CORE)) {
+    Debug("bitvector::explain") << "TheoryBV::explain(" << literal << "): EQUALITY" << std::endl;
+    d_coreSolver.explain(literal, assumptions);
   } else {
     Assert(propagatedBy(literal, SUB_BITBLAST));
-    BVDebug("bitvector::explain") << "TheoryBV::explain(" << literal << ") : BITBLASTER" << std::endl;
+    Debug("bitvector::explain") << "TheoryBV::explain(" << literal << ") : BITBLASTER" << std::endl;
     d_bitblastSolver.explain(literal, assumptions);
   }
 }
 
 
 Node TheoryBV::explain(TNode node) {
-  BVDebug("bitvector::explain") << "TheoryBV::explain(" << node << ")" << std::endl;
+  Debug("bitvector::explain") << "TheoryBV::explain(" << node << ")" << std::endl;
   std::vector<TNode> assumptions;
 
   // Ask for the explanation
@@ -271,18 +283,19 @@ void TheoryBV::addSharedTerm(TNode t) {
   Debug("bitvector::sharing") << indent() << "TheoryBV::addSharedTerm(" << t << ")" << std::endl;
   d_sharedTermsSet.insert(t);
   if (!options::bitvectorEagerBitblast() && d_useEqualityEngine) {
-    d_equalitySolver.addSharedTerm(t);
+    d_coreSolver.addSharedTerm(t);
   }
 }
 
 
+
 EqualityStatus TheoryBV::getEqualityStatus(TNode a, TNode b)
 {
   if (options::bitvectorEagerBitblast()) {
     return EQUALITY_UNKNOWN;
   }
 
-  EqualityStatus status = d_equalitySolver.getEqualityStatus(a, b);
+  EqualityStatus status = d_coreSolver.getEqualityStatus(a, b);
   if (status == EQUALITY_UNKNOWN) {
     status = d_bitblastSolver.getEqualityStatus(a, b);
   }
diff --git a/src/theory/bv/theory_bv.h b/src/theory/bv/theory_bv.h
index e38f3568c..c16e854cc 100644
--- a/src/theory/bv/theory_bv.h
+++ b/src/theory/bv/theory_bv.h
@@ -28,7 +28,9 @@
 #include "context/cdqueue.h"
 #include "theory/bv/bv_subtheory.h"
 #include "theory/bv/bv_subtheory_eq.h"
+#include "theory/bv/bv_subtheory_core.h"
 #include "theory/bv/bv_subtheory_bitblast.h"
+#include "theory/bv/slicer.h"
 
 namespace CVC4 {
 namespace theory {
@@ -43,8 +45,11 @@ class TheoryBV : public Theory {
   context::CDHashSet<Node, NodeHashFunction> d_alreadyPropagatedSet;
   context::CDHashSet<Node, NodeHashFunction> d_sharedTermsSet;
 
+  Slicer         d_slicer;
+  
   BitblastSolver d_bitblastSolver;
-  EqualitySolver d_equalitySolver;
+  CoreSolver d_coreSolver;
+
 public:
 
   TheoryBV(context::Context* c, context::UserContext* u, OutputChannel& out, Valuation valuation, const LogicInfo& logicInfo, QuantifiersEngine* qe);
@@ -67,6 +72,7 @@ public:
   PPAssertStatus ppAssert(TNode in, SubstitutionMap& outSubstitutions);
   Node ppRewrite(TNode t);
 
+  void presolve();
 private:
 
   class Statistics {
@@ -137,6 +143,7 @@ private:
   friend class Bitblaster;
   friend class BitblastSolver;
   friend class EqualitySolver;
+  friend class CoreSolver;
 
 };/* class TheoryBV */
 
diff --git a/src/util/bitvector.h b/src/util/bitvector.h
index 2c178ec2e..5df632ff4 100644
--- a/src/util/bitvector.h
+++ b/src/util/bitvector.h
@@ -178,6 +178,17 @@ public:
     Integer prod = d_value * y.d_value;
     return BitVector(d_size, prod);
   }
+
+  BitVector setBit(uint32_t i) const {
+    CheckArgument(i < d_size, i);
+    Integer res = d_value.setBit(i);
+    return BitVector(d_size, res); 
+  }
+
+  bool isBitSet(uint32_t i) const {
+    CheckArgument(i < d_size, i); 
+    return d_value.isBitSet(i); 
+  }
   
   BitVector unsignedDiv (const BitVector& y) const {
     CheckArgument(d_size == y.d_size, y);
diff --git a/src/util/integer_cln_imp.h b/src/util/integer_cln_imp.h
index 211c40741..e2a8f4a62 100644
--- a/src/util/integer_cln_imp.h
+++ b/src/util/integer_cln_imp.h
@@ -218,6 +218,16 @@ public:
     return Integer( d_value << ipow);
   }
 
+  bool isBitSet(uint32_t i) const {
+    return !extractBitRange(1, i).isZero(); 
+  }
+  
+  Integer setBit(uint32_t i) const {
+    cln::cl_I mask(1);
+    mask = mask << i; 
+    return Integer(cln::logior(d_value, mask)); 
+  }
+  
   Integer oneExtend(uint32_t size, uint32_t amount) const {
     DebugCheckArgument((*this) < Integer(1).multiplyByPow2(size), size);
     cln::cl_byte range(amount, size);
diff --git a/src/util/integer_gmp_imp.h b/src/util/integer_gmp_imp.h
index bebd0e1e2..d6882b6ac 100644
--- a/src/util/integer_gmp_imp.h
+++ b/src/util/integer_gmp_imp.h
@@ -137,6 +137,7 @@ public:
     return *this;
   }
 
+
   Integer bitwiseOr(const Integer& y) const {
     mpz_class result;
     mpz_ior(result.get_mpz_t(), d_value.get_mpz_t(), y.d_value.get_mpz_t());
@@ -170,6 +171,24 @@ public:
     return Integer( result );
   }
 
+  /** 
+   * Returns the Integer obtained by setting the ith bit of the
+   * current Integer to 1. 
+   * 
+   * @param bit 
+   * 
+   * @return 
+   */
+  Integer setBit(uint32_t i) const {
+    mpz_class res = d_value;
+    mpz_setbit(res.get_mpz_t(), i);
+    return Integer(res); 
+  }
+
+  bool isBitSet(uint32_t i) const {
+    return !extractBitRange(1, i).isZero(); 
+  }
+  
   /**
    * Returns the integer with the binary representation of size bits
    * extended with amount 1's
diff --git a/src/util/utility.h b/src/util/utility.h
index 5ce185b5b..72213764f 100644
--- a/src/util/utility.h
+++ b/src/util/utility.h
@@ -67,6 +67,15 @@ inline InputIterator find_if_unique(InputIterator first, InputIterator last, Pre
   return (match2 == last) ? match : last;
 }
 
+template <class T>
+inline T gcd(T a, T b) {
+  while (b != 0) {
+    a = b;
+    b = a % b; 
+  }
+  return a;
+}
+
 
 }/* CVC4 namespace */