Merge branch 'master' of github.com:CVC4/CVC4

36 files changed, 3927 insertions, 494 deletions

diff --git a/src/cvc4.i b/src/cvc4.i
index ebb8cbd63..965452b84 100644
--- a/src/cvc4.i
+++ b/src/cvc4.i
@@ -66,6 +66,8 @@ std::set<JavaInputStreamAdapter*> CVC4::JavaInputStreamAdapter::s_adapters;
 %template(vectorDatatypeType) std::vector< CVC4::DatatypeType >;
 %template(vectorSExpr) std::vector< CVC4::SExpr >;
 %template(vectorString) std::vector< std::string >;
+%template(vectorPairStringType) std::vector< std::pair< std::string, CVC4::Type > >;
+%template(pairStringType) std::pair< std::string, CVC4::Type >;
 %template(setType) std::set< CVC4::Type >;
 %template(hashmapExpr) std::hash_map< CVC4::Expr, CVC4::Expr, CVC4::ExprHashFunction >;
 
diff --git a/src/expr/command.i b/src/expr/command.i
index 6085a444f..76c8fa674 100644
--- a/src/expr/command.i
+++ b/src/expr/command.i
@@ -54,6 +54,12 @@
 // getNext() just allows C++ iterator access from Java-side next(), make it private
 %javamethodmodifiers CVC4::JavaIteratorAdapter<CVC4::CommandSequence>::getNext() "private";
 
+// map the types appropriately
+%typemap(jni) CVC4::CommandSequence::const_iterator::value_type "jobject";
+%typemap(jtype) CVC4::CommandSequence::const_iterator::value_type "edu.nyu.acsys.CVC4.Command";
+%typemap(jstype) CVC4::CommandSequence::const_iterator::value_type "edu.nyu.acsys.CVC4.Command";
+%typemap(javaout) CVC4::CommandSequence::const_iterator::value_type { return $jnicall; }
+
 #endif /* SWIGJAVA */
 
 %include "expr/command.h"
diff --git a/src/expr/expr.i b/src/expr/expr.i
index 92ab517b1..977345a63 100644
--- a/src/expr/expr.i
+++ b/src/expr/expr.i
@@ -72,6 +72,12 @@ namespace CVC4 {
 // getNext() just allows C++ iterator access from Java-side next(), make it private
 %javamethodmodifiers CVC4::JavaIteratorAdapter<CVC4::Expr>::getNext() "private";
 
+// map the types appropriately
+%typemap(jni) CVC4::Expr::const_iterator::value_type "jobject";
+%typemap(jtype) CVC4::Expr::const_iterator::value_type "edu.nyu.acsys.CVC4.Expr";
+%typemap(jstype) CVC4::Expr::const_iterator::value_type "edu.nyu.acsys.CVC4.Expr";
+%typemap(javaout) CVC4::Expr::const_iterator::value_type { return $jnicall; }
+
 #endif /* SWIGJAVA */
 
 %include "expr/expr.h"
diff --git a/src/expr/type_checker_template.cpp b/src/expr/type_checker_template.cpp
index 16f9ba917..4d9cbc60d 100644
--- a/src/expr/type_checker_template.cpp
+++ b/src/expr/type_checker_template.cpp
@@ -39,6 +39,9 @@ TypeNode TypeChecker::computeType(NodeManager* nodeManager, TNode n, bool check)
   case kind::BUILTIN:
     typeNode = nodeManager->builtinOperatorType();
     break;
+  case kind::BITVECTOR_EXTRACT_OP :
+    typeNode = nodeManager->builtinOperatorType();
+    break; 
 
 ${typerules}
 
diff --git a/src/theory/arrays/array_info.cpp b/src/theory/arrays/array_info.cpp
index bb9a9e417..32eaff355 100644
--- a/src/theory/arrays/array_info.cpp
+++ b/src/theory/arrays/array_info.cpp
@@ -167,6 +167,20 @@ void ArrayInfo::setRIntro1Applied(const TNode a) {
   
 }
 
+void ArrayInfo::setModelRep(const TNode a, const TNode b) {
+  Assert(a.getType().isArray());
+  Info* temp_info;
+  CNodeInfoMap::iterator it = info_map.find(a);
+  if(it == info_map.end()) {
+    temp_info = new Info(ct, bck);
+    temp_info->modelRep = b;
+    info_map[a] = temp_info;
+  } else {
+    (*it).second->modelRep = b;
+  }
+  
+}
+
 /**
  * Returns the information associated with TNode a
  */
@@ -200,6 +214,16 @@ const bool ArrayInfo::rIntro1Applied(const TNode a) const
   return false;
 }
 
+const TNode ArrayInfo::getModelRep(const TNode a) const
+{
+  CNodeInfoMap::const_iterator it = info_map.find(a);
+
+  if(it!= info_map.end()) {
+    return (*it).second->modelRep;
+  }
+  return TNode();
+}
+
 const CTNodeList* ArrayInfo::getIndices(const TNode a) const{
   CNodeInfoMap::const_iterator it = info_map.find(a);
   if(it!= info_map.end()) {
diff --git a/src/theory/arrays/array_info.h b/src/theory/arrays/array_info.h
index 13fae2ae5..10c15fd0e 100644
--- a/src/theory/arrays/array_info.h
+++ b/src/theory/arrays/array_info.h
@@ -63,11 +63,12 @@ class Info {
 public:
   context::CDO<bool> isNonLinear;
   context::CDO<bool> rIntro1Applied;
+  context::CDO<TNode> modelRep;
   CTNodeList* indices;
   CTNodeList* stores;
   CTNodeList* in_stores;
 
-  Info(context::Context* c, Backtracker<TNode>* bck) : isNonLinear(c, false), rIntro1Applied(c, false) {
+  Info(context::Context* c, Backtracker<TNode>* bck) : isNonLinear(c, false), rIntro1Applied(c, false), modelRep(c,TNode()) {
     indices = new(true)CTNodeList(c);
     stores = new(true)CTNodeList(c);
     in_stores = new(true)CTNodeList(c);
@@ -209,6 +210,7 @@ public:
 
   void setNonLinear(const TNode a);
   void setRIntro1Applied(const TNode a);
+  void setModelRep(const TNode a, const TNode rep);
 
   /**
    * Returns the information associated with TNode a
@@ -220,6 +222,8 @@ public:
 
   const bool rIntro1Applied(const TNode a) const;
 
+  const TNode getModelRep(const TNode a) const;
+
   const CTNodeList* getIndices(const TNode a) const;
 
   const CTNodeList* getStores(const TNode a) const;
diff --git a/src/theory/arrays/options b/src/theory/arrays/options
index 755cf239c..8a971cfe8 100644
--- a/src/theory/arrays/options
+++ b/src/theory/arrays/options
@@ -11,4 +11,10 @@ option arraysOptimizeLinear --arrays-optimize-linear bool :default true :read-wr
 option arraysLazyRIntro1 --arrays-lazy-rintro1 bool :default true :read-write
  turn on optimization to only perform RIntro1 rule lazily (see Jovanovic/Barrett 2012: Being Careful with Theory Combination)
 
+option arraysModelBased --arrays-model-based bool :default false :read-write
+ turn on model-based arrray solver
+
+option arraysEagerIndexSplitting --arrays-eager-index bool :default true :read-write
+ turn on eager index splitting for generated array lemmas
+
 endmodule
diff --git a/src/theory/arrays/theory_arrays.cpp b/src/theory/arrays/theory_arrays.cpp
index dcf4813fc..783929f97 100644
--- a/src/theory/arrays/theory_arrays.cpp
+++ b/src/theory/arrays/theory_arrays.cpp
@@ -48,7 +48,7 @@ const bool d_solveWrite2 = false;
   // These are now options
   //bool d_useNonLinearOpt = true;
   //bool d_lazyRIntro1 = true;
-const bool d_eagerIndexSplitting = true;
+  //bool d_eagerIndexSplitting = false;
 
 TheoryArrays::TheoryArrays(context::Context* c, context::UserContext* u, OutputChannel& out, Valuation valuation, const LogicInfo& logicInfo, QuantifiersEngine* qe) :
   Theory(THEORY_ARRAY, c, u, out, valuation, logicInfo, qe),
@@ -58,6 +58,10 @@ TheoryArrays::TheoryArrays(context::Context* c, context::UserContext* u, OutputC
   d_numExplain("theory::arrays::number of explanations", 0),
   d_numNonLinear("theory::arrays::number of calls to setNonLinear", 0),
   d_numSharedArrayVarSplits("theory::arrays::number of shared array var splits", 0),
+  d_numGetModelValSplits("theory::arrays::number of getModelVal splits", 0),
+  d_numGetModelValConflicts("theory::arrays::number of getModelVal conflicts", 0),
+  d_numSetModelValSplits("theory::arrays::number of setModelVal splits", 0),
+  d_numSetModelValConflicts("theory::arrays::number of setModelVal conflicts", 0),
   d_checkTimer("theory::arrays::checkTime"),
   d_ppEqualityEngine(u, "theory::arrays::TheoryArraysPP"),
   d_ppFacts(u),
@@ -79,8 +83,11 @@ TheoryArrays::TheoryArrays(context::Context* c, context::UserContext* u, OutputC
   d_sharedOther(c),
   d_sharedTerms(c, false),
   d_reads(c),
+  d_skolemIndex(c, 0),
   d_decisionRequests(c),
-  d_permRef(c)
+  d_permRef(c),
+  d_modelConstraints(c),
+  d_inCheckModel(false)
 {
   StatisticsRegistry::registerStat(&d_numRow);
   StatisticsRegistry::registerStat(&d_numExt);
@@ -88,6 +95,10 @@ TheoryArrays::TheoryArrays(context::Context* c, context::UserContext* u, OutputC
   StatisticsRegistry::registerStat(&d_numExplain);
   StatisticsRegistry::registerStat(&d_numNonLinear);
   StatisticsRegistry::registerStat(&d_numSharedArrayVarSplits);
+  StatisticsRegistry::registerStat(&d_numGetModelValSplits);
+  StatisticsRegistry::registerStat(&d_numGetModelValConflicts);
+  StatisticsRegistry::registerStat(&d_numSetModelValSplits);
+  StatisticsRegistry::registerStat(&d_numSetModelValConflicts);
   StatisticsRegistry::registerStat(&d_checkTimer);
 
   d_true = NodeManager::currentNM()->mkConst<bool>(true);
@@ -119,6 +130,10 @@ TheoryArrays::~TheoryArrays() {
   StatisticsRegistry::unregisterStat(&d_numExplain);
   StatisticsRegistry::unregisterStat(&d_numNonLinear);
   StatisticsRegistry::unregisterStat(&d_numSharedArrayVarSplits);
+  StatisticsRegistry::unregisterStat(&d_numGetModelValSplits);
+  StatisticsRegistry::unregisterStat(&d_numGetModelValConflicts);
+  StatisticsRegistry::unregisterStat(&d_numSetModelValSplits);
+  StatisticsRegistry::unregisterStat(&d_numSetModelValConflicts);
   StatisticsRegistry::unregisterStat(&d_checkTimer);
 
 }
@@ -140,6 +155,128 @@ bool TheoryArrays::ppDisequal(TNode a, TNode b) {
           Rewriter::rewrite(a.eqNode(b)) == d_false);
 }
 
+
+Node TheoryArrays::solveWrite(TNode term, bool solve1, bool solve2, bool ppCheck)
+{
+  if (!solve1) {
+    return term;
+  }
+  if (term[0].getKind() != kind::STORE &&
+      term[1].getKind() != kind::STORE) {
+    return term;
+  }
+  TNode left = term[0];
+  TNode right = term[1];
+  int leftWrites = 0, rightWrites = 0;
+
+  // Count nested writes
+  TNode e1 = left;
+  while (e1.getKind() == kind::STORE) {
+    ++leftWrites;
+    e1 = e1[0];
+  }
+
+  TNode e2 = right;
+  while (e2.getKind() == kind::STORE) {
+    ++rightWrites;
+    e2 = e2[0];
+  }
+
+  if (rightWrites > leftWrites) {
+    TNode tmp = left;
+    left = right;
+    right = tmp;
+    int tmpWrites = leftWrites;
+    leftWrites = rightWrites;
+    rightWrites = tmpWrites;
+  }
+
+  NodeManager* nm = NodeManager::currentNM();
+  if (rightWrites == 0) {
+    if (e1 != e2) {
+      return term;
+    }
+    // write(store, index_0, v_0, index_1, v_1, ..., index_n, v_n) = store IFF
+    //
+    // read(store, index_n) = v_n &
+    // index_{n-1} != index_n -> read(store, index_{n-1}) = v_{n-1} &
+    // (index_{n-2} != index_{n-1} & index_{n-2} != index_n) -> read(store, index_{n-2}) = v_{n-2} &
+    // ...
+    // (index_1 != index_2 & ... & index_1 != index_n) -> read(store, index_1) = v_1
+    // (index_0 != index_1 & index_0 != index_2 & ... & index_0 != index_n) -> read(store, index_0) = v_0
+    TNode write_i, write_j, index_i, index_j;
+    Node conc;
+    NodeBuilder<> result(kind::AND);
+    int i, j;
+    write_i = left;
+    for (i = leftWrites-1; i >= 0; --i) {
+      index_i = write_i[1];
+
+      // build: [index_i /= index_n && index_i /= index_(n-1) &&
+      //         ... && index_i /= index_(i+1)] -> read(store, index_i) = v_i
+      write_j = left;
+      {
+        NodeBuilder<> hyp(kind::AND);
+        for (j = leftWrites - 1; j > i; --j) {
+          index_j = write_j[1];
+          if (!ppCheck || !ppDisequal(index_i, index_j)) {
+            Node hyp2(index_i.getType() == nm->booleanType()?
+                      index_i.iffNode(index_j) : index_i.eqNode(index_j));
+            hyp << hyp2.notNode();
+          }
+          write_j = write_j[0];
+        }
+
+        Node r1 = nm->mkNode(kind::SELECT, e1, index_i);
+        conc = (r1.getType() == nm->booleanType())?
+          r1.iffNode(write_i[2]) : r1.eqNode(write_i[2]);
+        if (hyp.getNumChildren() != 0) {
+          if (hyp.getNumChildren() == 1) {
+            conc = hyp.getChild(0).impNode(conc);
+          }
+          else {
+            r1 = hyp;
+            conc = r1.impNode(conc);
+          }
+        }
+
+        // And into result
+        result << conc;
+
+        // Prepare for next iteration
+        write_i = write_i[0];
+      }
+    }
+    Assert(result.getNumChildren() > 0);
+    if (result.getNumChildren() == 1) {
+      return result.getChild(0);
+    }
+    return result;
+  }
+  else {
+    if (!solve2) {
+      return term;
+    }
+    // store(...) = store(a,i,v) ==>
+    // store(store(...),i,select(a,i)) = a && select(store(...),i)=v
+    Node l = left;
+    Node tmp;
+    NodeBuilder<> nb(kind::AND);
+    while (right.getKind() == kind::STORE) {
+      tmp = nm->mkNode(kind::SELECT, l, right[1]);
+      nb << tmp.eqNode(right[2]);
+      tmp = nm->mkNode(kind::SELECT, right[0], right[1]);
+      l = nm->mkNode(kind::STORE, l, right[1], tmp);
+      right = right[0];
+    }
+    nb << solveWrite(l.eqNode(right), solve1, solve2, ppCheck);
+    return nb;
+  }
+  Unreachable();
+  return term;
+}
+
+
 Node TheoryArrays::ppRewrite(TNode term) {
   if (!d_preprocess) return term;
   d_ppEqualityEngine.addTerm(term);
@@ -163,115 +300,7 @@ Node TheoryArrays::ppRewrite(TNode term) {
       break;
     }
     case kind::EQUAL: {
-      if (!d_solveWrite) break;
-      if (term[0].getKind() == kind::STORE ||
-          term[1].getKind() == kind::STORE) {
-        TNode left = term[0];
-        TNode right = term[1];
-        int leftWrites = 0, rightWrites = 0;
-
-        // Count nested writes
-        TNode e1 = left;
-        while (e1.getKind() == kind::STORE) {
-          ++leftWrites;
-          e1 = e1[0];
-        }
-
-        TNode e2 = right;
-        while (e2.getKind() == kind::STORE) {
-          ++rightWrites;
-          e2 = e2[0];
-        }
-
-        if (rightWrites > leftWrites) {
-          TNode tmp = left;
-          left = right;
-          right = tmp;
-          int tmpWrites = leftWrites;
-          leftWrites = rightWrites;
-          rightWrites = tmpWrites;
-        }
-
-        NodeManager* nm = NodeManager::currentNM();
-        if (rightWrites == 0) {
-          if (e1 == e2) {
-            // write(store, index_0, v_0, index_1, v_1, ..., index_n, v_n) = store IFF
-            //
-            // read(store, index_n) = v_n &
-            // index_{n-1} != index_n -> read(store, index_{n-1}) = v_{n-1} &
-            // (index_{n-2} != index_{n-1} & index_{n-2} != index_n) -> read(store, index_{n-2}) = v_{n-2} &
-            // ...
-            // (index_1 != index_2 & ... & index_1 != index_n) -> read(store, index_1) = v_1
-            // (index_0 != index_1 & index_0 != index_2 & ... & index_0 != index_n) -> read(store, index_0) = v_0
-            TNode write_i, write_j, index_i, index_j;
-            Node conc;
-            NodeBuilder<> result(kind::AND);
-            int i, j;
-            write_i = left;
-            for (i = leftWrites-1; i >= 0; --i) {
-              index_i = write_i[1];
-
-              // build: [index_i /= index_n && index_i /= index_(n-1) &&
-              //         ... && index_i /= index_(i+1)] -> read(store, index_i) = v_i
-              write_j = left;
-              {
-                NodeBuilder<> hyp(kind::AND);
-                for (j = leftWrites - 1; j > i; --j) {
-                  index_j = write_j[1];
-                  if (!ppDisequal(index_i, index_j)) {
-                    Node hyp2(index_i.getType() == nm->booleanType()?
-                              index_i.iffNode(index_j) : index_i.eqNode(index_j));
-                    hyp << hyp2.notNode();
-                  }
-                  write_j = write_j[0];
-                }
-
-                Node r1 = nm->mkNode(kind::SELECT, e1, index_i);
-                conc = (r1.getType() == nm->booleanType())?
-                  r1.iffNode(write_i[2]) : r1.eqNode(write_i[2]);
-                if (hyp.getNumChildren() != 0) {
-                  if (hyp.getNumChildren() == 1) {
-                    conc = hyp.getChild(0).impNode(conc);
-                  }
-                  else {
-                    r1 = hyp;
-                    conc = r1.impNode(conc);
-                  }
-                }
-
-                // And into result
-                result << conc;
-
-                // Prepare for next iteration
-                write_i = write_i[0];
-              }
-            }
-            Assert(result.getNumChildren() > 0);
-            if (result.getNumChildren() == 1) {
-              return result.getChild(0);
-            }
-            return result;
-          }
-          break;
-        }
-        else {
-          if (!d_solveWrite2) break;
-          // store(...) = store(a,i,v) ==>
-          // store(store(...),i,select(a,i)) = a && select(store(...),i)=v
-          Node l = left;
-          Node tmp;
-          NodeBuilder<> nb(kind::AND);
-          while (right.getKind() == kind::STORE) {
-            tmp = nm->mkNode(kind::SELECT, l, right[1]);
-            nb << tmp.eqNode(right[2]);
-            tmp = nm->mkNode(kind::SELECT, right[0], right[1]);
-            l = nm->mkNode(kind::STORE, l, right[1], tmp);
-            right = right[0];
-          }
-          nb << l.eqNode(right);
-          return nb;
-        }
-      }
+      return solveWrite(term, d_solveWrite, d_solveWrite2, true);
       break;
     }
     default:
@@ -330,6 +359,9 @@ bool TheoryArrays::propagate(TNode literal)
   }
 
   // Propagate away
+  if (d_inCheckModel && getSatContext()->getLevel() != d_topLevel) {
+    return true;
+  }
   bool ok = d_out->propagate(literal);
   if (!ok) {
     d_conflict = true;
@@ -453,6 +485,7 @@ void TheoryArrays::preRegisterTermInternal(TNode node)
 
     d_infoMap.addStore(node, node);
     d_infoMap.addInStore(a, node);
+    d_infoMap.setModelRep(node, node);
 
     checkStore(node);
     break;
@@ -554,6 +587,7 @@ void TheoryArrays::computeCareGraph()
       }
     }
   }
+  if (options::arraysModelBased()) return;
   if (d_sharedTerms) {
 
     vector< pair<TNode, TNode> > currentPairs;
@@ -821,7 +855,40 @@ void TheoryArrays::presolve()
 /////////////////////////////////////////////////////////////////////////////
 
 
+Node TheoryArrays::getSkolem(TNode ref, const string& name, const TypeNode& type, const string& comment, bool makeEqual)
+{
+  Node skolem;
+  std::hash_map<Node, Node, NodeHashFunction>::iterator it = d_skolemCache.find(ref);
+  if (it == d_skolemCache.end()) {
+    NodeManager* nm = NodeManager::currentNM();
+    skolem = nm->mkSkolem(name, type, comment);
+    d_skolemCache[ref] = skolem;
+  }
+  else {
+    skolem = (*it).second;
+    if (d_equalityEngine.hasTerm(ref) &&
+        d_equalityEngine.hasTerm(skolem) &&
+        d_equalityEngine.areEqual(ref, skolem)) {
+      makeEqual = false;
+    }
+  }
+  preRegisterTermInternal(skolem);
+  if (makeEqual) {
+    Node d = skolem.eqNode(ref);
+    Debug("arrays-model-based") << "Asserting skolem equality " << d << endl;
+    d_equalityEngine.assertEquality(d, true, d_true);
+    Assert(!d_conflict);
+    d_skolemAssertions.push_back(d);
+    d_skolemIndex = d_skolemIndex + 1;
+  }
+  return skolem;
+}
+
+
 void TheoryArrays::check(Effort e) {
+  if (done() && !fullEffort(e)) {
+    return;
+  }
   TimerStat::CodeTimer codeTimer(d_checkTimer);
 
   while (!done() && !d_conflict)
@@ -852,13 +919,18 @@ void TheoryArrays::check(Effort e) {
     switch (fact.getKind()) {
       case kind::EQUAL:
         d_equalityEngine.assertEquality(fact, true, fact);
+        if (!fact[0].getType().isArray()) {
+          d_modelConstraints.push_back(fact);
+        }
         break;
       case kind::SELECT:
         d_equalityEngine.assertPredicate(fact, true, fact);
+        d_modelConstraints.push_back(fact);
         break;
       case kind::NOT:
         if (fact[0].getKind() == kind::SELECT) {
           d_equalityEngine.assertPredicate(fact[0], false, fact);
+          d_modelConstraints.push_back(fact);
         } else if (!d_equalityEngine.areDisequal(fact[0][0], fact[0][1], false)) {
           // Assert the dis-equality
           d_equalityEngine.assertEquality(fact[0], false, fact);
@@ -867,16 +939,7 @@ void TheoryArrays::check(Effort e) {
           if(fact[0][0].getType().isArray() && !d_conflict) {
             NodeManager* nm = NodeManager::currentNM();
             TypeNode indexType = fact[0][0].getType()[0];
-            TNode k;
-            std::hash_map<TNode, Node, TNodeHashFunction>::iterator it = d_diseqCache.find(fact);
-            if (it == d_diseqCache.end()) {
-              Node newk = nm->mkSkolem("array_ext_index_$$", indexType, "an extensional lemma index variable from the theory of arrays");
-              d_diseqCache[fact] = newk;
-              k = newk;
-            }
-            else {
-              k = (*it).second;
-            }
+            TNode k = getSkolem(fact,"array_ext_index_$$", indexType, "an extensional lemma index variable from the theory of arrays", false);
 
             Node ak = nm->mkNode(kind::SELECT, fact[0][0], k);
             Node bk = nm->mkNode(kind::SELECT, fact[0][1], k);
@@ -887,6 +950,9 @@ void TheoryArrays::check(Effort e) {
             d_out->lemma(lemma);
             ++d_numExt;
           }
+          else {
+            d_modelConstraints.push_back(fact);
+          }
         }
         break;
       default:
@@ -894,8 +960,11 @@ void TheoryArrays::check(Effort e) {
     }
   }
 
-  // If in conflict, output the conflict
-  if(!d_eagerLemmas && fullEffort(e) && !d_conflict) {
+  if (options::arraysModelBased() && !d_conflict && (options::arraysEagerIndexSplitting() || fullEffort(e))) {
+    checkModel(e);
+  }
+
+  if(!d_eagerLemmas && fullEffort(e) && !d_conflict && !options::arraysModelBased()) {
     // generate the lemmas on the worklist
     Trace("arrays-lem")<<"Arrays::discharging lemmas: "<<d_RowQueue.size()<<"\n";
     dischargeLemmas();
@@ -905,43 +974,754 @@ void TheoryArrays::check(Effort e) {
 }
 
 
-Node TheoryArrays::mkAnd(std::vector<TNode>& conjunctions)
+void TheoryArrays::convertNodeToAssumptions(TNode node, vector<TNode>& assumptions, TNode nodeSkip)
+{
+  Assert(node.getKind() == kind::AND);
+  for(TNode::iterator child_it = node.begin(); child_it != node.end(); ++child_it) {
+    if ((*child_it).getKind() == kind::AND) {
+      convertNodeToAssumptions(*child_it, assumptions, nodeSkip);
+    }
+    else if (*child_it != nodeSkip) {
+      assumptions.push_back(*child_it);
+    }
+  }
+}
+
+
+void TheoryArrays::preRegisterStores(TNode s)
+{
+  if (d_equalityEngine.hasTerm(s)) {
+    return;
+  }
+  if (s.getKind() == kind::STORE) {
+    preRegisterStores(s[0]);
+    preRegisterTermInternal(s);
+  }
+}
+
+
+void TheoryArrays::checkModel(Effort e)
+{
+  d_inCheckModel = true;
+  d_topLevel = getSatContext()->getLevel();
+  Assert(d_skolemIndex == 0);
+  Assert(d_skolemAssertions.empty());
+  Assert(d_lemmas.empty());
+
+  if (fullEffort(e)) {
+    // Add constraints for shared terms
+    context::CDList<TNode>::const_iterator shared_it = shared_terms_begin(), shared_it_end = shared_terms_end(), shared_it2;
+    Node modelVal, modelVal2, d;
+    vector<TNode> assumptions;
+    for (; shared_it != shared_it_end; ++shared_it) {
+      if ((*shared_it).getType().isArray()) {
+        continue;
+      }
+      if ((*shared_it).isConst()) {
+        modelVal = (*shared_it);
+      }
+      else {
+        modelVal = d_valuation.getModelValue(*shared_it);
+        if (modelVal.isNull()) {
+          continue;
+        }
+      }
+      Assert(modelVal.isConst());
+      for (shared_it2 = shared_it, ++shared_it2; shared_it2 != shared_it_end; ++shared_it2) {
+        if ((*shared_it2).getType() != (*shared_it).getType()) {
+          continue;
+        }
+        if ((*shared_it2).isConst()) {
+          modelVal2 = (*shared_it2);
+        }
+        else {
+          modelVal2 = d_valuation.getModelValue(*shared_it2);
+          if (modelVal2.isNull()) {
+            continue;
+          }
+        }
+        Assert(modelVal2.isConst());
+        d = (*shared_it).eqNode(*shared_it2);
+        if (modelVal != modelVal2) {
+          d = d.notNode();
+        }
+        if (!setModelVal(d, d_true, false, true, assumptions)) {
+          assumptions.push_back(d);
+          d_lemmas.push_back(mkAnd(assumptions, true));
+          goto finish;
+        }
+        assumptions.clear();
+      }
+    }
+  }
+  {
+  // TODO: record and replay decisions
+  int baseLevel = getSatContext()->getLevel();
+  unsigned constraintIdx;
+  Node assertion, assertionToCheck;
+  vector<TNode> assumptions;
+  while (true) {
+    int level = getSatContext()->getLevel();
+    d_getModelValCache.clear();
+    for (constraintIdx = 0; constraintIdx < d_modelConstraints.size(); ++constraintIdx) {
+      assertion = d_modelConstraints[constraintIdx];
+      if (getModelValRec(assertion) != d_true) {
+        break;
+      }
+    }
+    getSatContext()->popto(level);
+    if (constraintIdx == d_modelConstraints.size()) {
+      break;
+    }
+    
+    if (assertion.getKind() == kind::EQUAL && assertion[0].getType().isArray()) {
+      assertionToCheck = solveWrite(expandStores(assertion[0], assumptions).eqNode(expandStores(assertion[1], assumptions)), true, true, false);
+      if (assertionToCheck.getKind() == kind::AND &&
+          assertionToCheck[assertionToCheck.getNumChildren()-1].getKind() == kind::EQUAL) {
+        TNode s = assertionToCheck[assertionToCheck.getNumChildren()-1][0];
+        preRegisterStores(s);
+      }
+    }
+    else {
+      assertionToCheck = assertion;
+    }
+    // TODO: try not collecting assumptions the first time
+    while (!setModelVal(assertionToCheck, d_true, false, true, assumptions)) {
+    restart:
+      if (assertion.getKind() == kind::EQUAL) {
+        d_equalityEngine.explainEquality(assertion[0], assertion[1], true, assumptions);
+      }
+      else {
+        assumptions.push_back(assertion);
+      }
+#ifdef CVC4_ASSERTIONS
+      std::set<TNode> validAssumptions;
+      context::CDList<Assertion>::const_iterator assert_it2 = facts_begin();
+      for (; assert_it2 != facts_end(); ++assert_it2) {
+        validAssumptions.insert(*assert_it2);
+      }
+      for (unsigned i = 0; i < d_decisions.size(); ++i) {
+        validAssumptions.insert(d_decisions[i]);
+      }
+#endif
+      std::set<TNode> all;
+      std::set<TNode> explained;
+      unsigned i = 0;
+      TNode t;
+      for (; i < assumptions.size(); ++i) {
+        t = assumptions[i];
+        if (t == d_true) {
+          continue;
+        }
+        if (t.getKind() == kind::AND) {
+          for(TNode::iterator child_it = t.begin(); child_it != t.end(); ++child_it) {
+            Assert(validAssumptions.find(*child_it) != validAssumptions.end());
+            all.insert(*child_it);
+          }
+        }
+        // Expand explanation resulting from propagating a ROW lemma
+        else if (t.getKind() == kind::OR) {
+          if ((explained.find(t) == explained.end())) {
+            Assert(t[1].getKind() == kind::EQUAL);
+            d_equalityEngine.explainEquality(t[1][0], t[1][1], false, assumptions);
+            explained.insert(t);
+          }
+          continue;
+        }
+        else {
+          Assert(validAssumptions.find(t) != validAssumptions.end());
+          all.insert(t);
+        }
+      }
+      //      d_lemmas.push_back(mkAnd(assumptions, true));
+
+      bool eq = false;
+      Node decision, explanation;
+      while (!d_decisions.empty()) {
+        getSatContext()->pop();
+        decision = d_decisions.back();
+        d_decisions.pop_back();
+        if (all.find(decision) != all.end()) {
+          if (getSatContext()->getLevel() < baseLevel) {
+            if (all.size() == 1) {
+              d_lemmas.push_back(decision.negate());
+            }
+            else {
+              NodeBuilder<> disjunction(kind::OR);
+              std::set<TNode>::const_iterator it = all.begin();
+              std::set<TNode>::const_iterator it_end = all.end();
+              while (it != it_end) {
+                disjunction << (*it).negate();
+                ++it;
+              }
+              d_lemmas.push_back(disjunction);
+            }
+            goto finish;
+          }
+          all.erase(decision);
+          eq = false;
+          if (decision.getKind() == kind::NOT) {
+            decision = decision[0];
+            eq = true;
+          }
+          while (getSatContext()->getLevel() != baseLevel && all.find(d_decisions.back()) == all.end()) {
+            getSatContext()->pop();
+            d_decisions.pop_back();
+          }
+          break;
+        }
+        else {
+          decision = Node();
+        }
+      }
+      if (all.size() == 0) {
+        explanation = d_true;
+      }
+      if (all.size() == 1) {
+        // All the same, or just one
+        explanation = *(all.begin());
+      }
+      else {
+        NodeBuilder<> conjunction(kind::AND);
+        std::set<TNode>::const_iterator it = all.begin();
+        std::set<TNode>::const_iterator it_end = all.end();
+        while (it != it_end) {
+          conjunction << *it;
+          ++it;
+        }
+        explanation = conjunction;
+        d_permRef.push_back(explanation);
+      }
+      if (decision.isNull()) {
+        //        d_lemmas.pop_back();
+        d_conflictNode = explanation;
+        d_conflict = true;
+        break;
+      }
+      d_equalityEngine.assertEquality(decision, eq, explanation);
+      if (!eq) decision = decision.notNode();
+      Debug("arrays-model-based") << "Asserting learned literal " << decision << " with explanation " << explanation << endl;
+      if (d_conflict) {
+        assumptions.clear();
+        convertNodeToAssumptions(d_conflictNode, assumptions, TNode());
+        assertion = d_true;
+        goto restart;
+      }
+      assumptions.clear();
+
+      // Reassert skolems if necessary
+      Node d;
+      while (d_skolemIndex < d_skolemAssertions.size()) {
+        d = d_skolemAssertions[d_skolemIndex];
+        Assert(isLeaf(d[0]));
+        if (!d_equalityEngine.hasTerm(d[0])) {
+          preRegisterTermInternal(d[0]);
+        }
+        if (d[0].getType().isArray()) {
+          Assert(d[1].getKind() == kind::STORE);
+          if (d[1][0].getKind() == kind::STORE) {
+            if (!d_equalityEngine.hasTerm(d[1][0][0])) {
+              preRegisterTermInternal(d[1][0][0]);
+            }
+            if (!d_equalityEngine.hasTerm(d[1][0][2])) {
+              preRegisterTermInternal(d[1][0][2]);
+            }
+          }
+          if (!d_equalityEngine.hasTerm(d[1][0])) {
+            preRegisterTermInternal(d[1][0]);
+          }
+          if (!d_equalityEngine.hasTerm(d[1][2])) {
+            preRegisterTermInternal(d[1][2]);
+          }
+          if (!d_equalityEngine.hasTerm(d[1])) {
+            preRegisterTermInternal(d[1]);
+          }
+        }
+        Debug("arrays-model-based") << "Re-asserting skolem equality " << d << endl;
+        d_equalityEngine.assertEquality(d, true, d_true);
+        Assert(!d_conflict);
+        if (!d[0].getType().isArray()) {
+          if (!setModelVal(d[1], d[0], false, true, assumptions)) {
+            assertion = d_true;
+            goto restart;
+          }
+          assumptions.clear();
+        }
+        d_skolemIndex = d_skolemIndex + 1;
+      }
+    }
+    if (d_conflict) {
+      break;
+    }
+    //    Assert(getModelVal(assertion) == d_true);
+    assumptions.clear();
+  }
+#ifdef CVC4_ASSERTIONS
+  if (!d_conflict) {
+    context::CDList<Assertion>::const_iterator assert_it = facts_begin(), assert_it_end = facts_end();
+    for (; assert_it != assert_it_end; ++assert_it) {
+      Assert(getModelVal(*assert_it) == d_true);
+    }
+  }
+#endif
+  }
+  finish:
+  while (!d_decisions.empty()) {
+    Assert(!d_conflict);
+    getSatContext()->pop();
+    d_decisions.pop_back();
+  }
+  d_skolemAssertions.clear();
+  d_skolemIndex = 0;
+  while (!d_lemmas.empty()) {
+    Debug("arrays-model-based") << "Sending lemma: " << d_lemmas.back() << endl;
+    d_out->lemma(d_lemmas.back());
+    d_lemmas.pop_back();
+  }
+  Assert(getSatContext()->getLevel() == d_topLevel);
+  if (d_conflict) {
+    Node tmp = d_conflictNode;
+    d_out->conflict(tmp);
+  }
+  d_inCheckModel = false;
+}
+
+
+Node TheoryArrays::getModelVal(TNode node)
+{
+  int level = getSatContext()->getLevel();
+  d_getModelValCache.clear();
+  Node ret = getModelValRec(node);
+  getSatContext()->popto(level);
+  return ret;
+}
+
+
+Node TheoryArrays::getModelValRec(TNode node)
+{
+  if (node.isConst()) {
+    return node;
+  }
+  NodeMap::iterator it = d_getModelValCache.find(node);
+  if (it != d_getModelValCache.end()) {
+    return (*it).second;
+  }
+  Node val;
+  switch (node.getKind()) {
+    case kind::NOT:
+      val = getModelValRec(node[0]) == d_true ? d_false : d_true;
+      break;
+    case kind::AND: {
+      val = d_true;
+      for(TNode::iterator child_it = node.begin(); child_it != node.end(); ++child_it) {
+        if (getModelValRec(*child_it) != d_true) {
+          val = d_false;
+          break;
+        }
+      }
+      break;
+    }
+    case kind::IMPLIES:
+      if (getModelValRec(node[0]) == d_false) {
+        val = d_true;
+      }
+      else {
+        val = getModelValRec(node[1]);
+      }
+    case kind::EQUAL:
+      val = getModelValRec(node[0]);
+      val = (val == getModelValRec(node[1])) ? d_true : d_false;
+      break;
+    case kind::SELECT: {
+      NodeManager* nm = NodeManager::currentNM();
+      Node indexVal = getModelValRec(node[1]);
+      val = Rewriter::rewrite(nm->mkNode(kind::SELECT, node[0], indexVal));
+      if (val.isConst()) {
+        break;
+      }
+      val = Rewriter::rewrite(nm->mkNode(kind::SELECT, getModelValRec(node[0]), indexVal));
+      Assert(val.isConst());
+      break;
+    }
+    case kind::STORE: {
+      NodeManager* nm = NodeManager::currentNM();
+      val = getModelValRec(node[0]);
+      val = Rewriter::rewrite(nm->mkNode(kind::STORE, val, getModelValRec(node[1]), getModelValRec(node[2])));
+      Assert(val.isConst());
+      break;
+    }
+    default: {
+      Assert(isLeaf(node));
+      TNode eRep = d_equalityEngine.getRepresentative(node);
+      if (eRep.isConst()) {
+        val = eRep;
+        break;
+      }
+      TNode rep = d_infoMap.getModelRep(eRep);
+      if (!rep.isNull()) {
+        // TODO: check for loop here
+        val = getModelValRec(rep);
+      }
+      else {
+        NodeMap::iterator it = d_lastVal.find(eRep);
+        if (it != d_lastVal.end()) {
+          val = (*it).second;
+          if (!d_equalityEngine.hasTerm(val) ||
+              !d_equalityEngine.areDisequal(eRep, val, true)) {
+            getSatContext()->push();
+            ++d_numGetModelValSplits;
+            d_equalityEngine.assertEquality(eRep.eqNode(val), true, d_true);
+            if (!d_conflict) {
+              break;
+            }
+            ++d_numGetModelValConflicts;
+            getSatContext()->pop();
+          }
+        }
+
+        TypeEnumerator te(eRep.getType());
+        val = *te;
+        while (true) {
+          if (!d_equalityEngine.hasTerm(val) ||
+              !d_equalityEngine.areDisequal(eRep, val, true)) {
+            getSatContext()->push();
+            ++d_numGetModelValSplits;
+            d_equalityEngine.assertEquality(eRep.eqNode(val), true, d_true);
+            if (!d_conflict) {
+              d_lastVal[eRep] = val;
+              break;
+            }
+            ++d_numGetModelValConflicts;
+            getSatContext()->pop();
+          } 
+          ++te;
+          if (te.isFinished()) {
+            Assert(false);
+            // TODO: conflict
+            break;
+          }
+          val = *te;
+        }
+      }
+      break;
+    }
+  }
+  d_getModelValCache[node] = val;
+  return val;
+}
+
+
+bool TheoryArrays::hasLoop(TNode node, TNode target)
+{
+  if (node == target) {
+    return true;
+  }
+
+  if (isLeaf(node)) {
+    TNode rep = d_infoMap.getModelRep(d_equalityEngine.getRepresentative(node));
+    if (!rep.isNull()) {
+      return hasLoop(rep, target);
+    }
+    return false;
+  }
+
+  for(TNode::iterator child_it = node.begin(); child_it != node.end(); ++child_it) {
+    if (hasLoop(*child_it, target)) {
+      return true;
+    }
+  }
+  
+  return false;
+}
+
+
+// Return true iff it we were able to modify model so that value of node has same value as val
+bool TheoryArrays::setModelVal(TNode node, TNode val, bool invert, bool explain, vector<TNode>& assumptions)
+{
+  Assert(!d_conflict);
+  if (node == val) {
+    return !invert;
+  }
+  if (node.isConst()) {
+    if (invert) {
+      return (val.isConst() && node != val);
+    }
+    return val == node;
+  }
+  switch(node.getKind()) {
+    case kind::NOT:
+      Assert(val == d_true || val == d_false);
+      return setModelVal(node[0], val, !invert, explain, assumptions);
+      break;
+    case kind::AND: {
+      Assert(val == d_true || val == d_false);
+      if (val == d_false) {
+        invert = !invert;
+      }
+      int i;
+      for(i = node.getNumChildren()-1; i >=0; --i) {
+        if (setModelVal(node[i], d_true, invert, explain, assumptions) == invert) {
+          return invert;
+        }
+      }
+      return !invert;
+    }
+    case kind::IMPLIES:
+      Assert(val == d_true || val == d_false);
+      if (val == d_false) {
+        invert = !invert;
+      }
+      if (setModelVal(node[0], d_false, invert, explain, assumptions) == !invert) {
+        return !invert;
+      }
+      if (setModelVal(node[1], d_true, invert, explain, assumptions) == !invert) {
+        return !invert;
+      }
+      return invert;
+    case kind::EQUAL:
+      Assert(val == d_true || val == d_false);
+      if (val == d_false) {
+        invert = !invert;
+      }
+      if (node[0].isConst()) {
+        return setModelVal(node[1], node[0], invert, explain, assumptions);
+      }
+      else {
+        return setModelVal(node[0], node[1], invert, explain, assumptions);
+      }
+    case kind::SELECT: {
+      TNode s = node[0];
+      Node index = node[1];
+
+      while (s.getKind() == kind::STORE) {
+        if (setModelVal(s[1].eqNode(index), d_true, false, explain, assumptions)) {
+          if (setModelVal(s[2].eqNode(val), d_true, invert, explain, assumptions)) {
+            return true;
+          }
+          // Now try to set the indices to be disequal
+          if (!setModelVal(s[1].eqNode(index), d_false, false, explain, assumptions)) {
+            return false;
+          }
+          Unreachable();
+        }
+        s = s[0];
+      }
+      TNode rep = d_infoMap.getModelRep(d_equalityEngine.getRepresentative(s));
+      NodeManager* nm = NodeManager::currentNM();
+      if (!rep.isNull()) {
+        // TODO: check for loop
+        if (explain) {
+          d_equalityEngine.explainEquality(s, rep, true, assumptions);
+        }
+        return setModelVal(nm->mkNode(kind::SELECT, rep, index), val, invert, explain, assumptions);
+      }
+      if (val.getKind() == kind::SELECT && val[0].getKind() == kind::STORE) {
+        return setModelVal(val, nm->mkNode(kind::SELECT, s, index), invert, explain, assumptions);
+      }
+
+      // Solve equation for s: select(s,index) op val --> s = store(s',i',v') /\ index = i' /\ v' op val
+      Node newVarArr = getSkolem(s, "array_model_arr_var_$$", s.getType(), "a new array variable from the theory of arrays", false);
+      Assert(d_infoMap.getModelRep(d_equalityEngine.getRepresentative(newVarArr)).isNull());
+      Node lookup;
+      bool checkIndex1 = false, checkIndex2 = false, checkIndex3 = false;
+      if (!isLeaf(index)) {
+        index = getSkolem(index, "array_model_index_$$", index.getType(), "a new index variable from the theory of arrays");
+        if (!index.getType().isArray()) {
+          checkIndex1 = true;
+        }
+      }
+      lookup = nm->mkNode(kind::SELECT, s, index);
+      Node newVarVal = getSkolem(lookup, "array_model_var_$$", val.getType(), "a new value variable from the theory of arrays", false);
+
+      Node newVarVal2;
+      Node index2;
+      TNode saveVal = val;
+      if (val.getKind() == kind::SELECT && val[0] == s) {
+        // Special case: select(s,index) = select(s,j): solution becomes s = store(store(s',j,v'),index,w') /\ v' = w'
+        index2 = val[1];
+        if (!isLeaf(index2)) {
+          index2 = getSkolem(val, "array_model_index_$$", index2.getType(), "a new index variable from the theory of arrays");
+          if (!index2.getType().isArray()) {
+            checkIndex2 = true;
+          }
+        }
+        if (invert) {
+          checkIndex3 = true;
+        }
+        lookup = nm->mkNode(kind::SELECT, s, index2);
+        newVarVal2 = getSkolem(lookup, "array_model_var_$$", val.getType(), "a new value variable from the theory of arrays", false);
+        newVarArr = nm->mkNode(kind::STORE, newVarArr, index2, newVarVal2);
+        preRegisterTermInternal(newVarArr);
+        val = newVarVal2;
+      }
+
+      Node d = nm->mkNode(kind::STORE, newVarArr, index, newVarVal);
+      preRegisterTermInternal(d);
+      d = s.eqNode(d);
+      Debug("arrays-model-based") << "Asserting array skolem equality " << d << endl;
+      d_equalityEngine.assertEquality(d, true, d_true);
+      d_skolemAssertions.push_back(d);
+      d_skolemIndex = d_skolemIndex + 1;
+      Assert(!d_conflict);
+      if (checkIndex1) {
+        if (!setModelVal(node[1], index, false, explain, assumptions)) {
+          return false;
+        }
+      }
+      if (checkIndex2) {
+        if (!setModelVal(saveVal[1], index2, false, explain, assumptions)) {
+          return false;
+        }
+      }
+      if (checkIndex3) {
+        if (!setModelVal(index2, index, true, explain, assumptions)) {
+          return false;
+        }
+      }
+      return setModelVal(newVarVal, val, invert, explain, assumptions);
+    }
+    case kind::STORE:
+      if (val.getKind() != kind::STORE) {
+        return setModelVal(val, node, invert, explain, assumptions);
+      }
+      Unreachable();
+      break;
+    default: {
+      Assert(isLeaf(node));
+      TNode rep = d_infoMap.getModelRep(d_equalityEngine.getRepresentative(node));
+      if (!rep.isNull()) {
+        // Assume this array equation has already been dealt with - otherwise, it shouldn't have a rep
+        return true;
+      }
+      if (val.getKind() == kind::SELECT) {
+        return setModelVal(val, node, invert, explain, assumptions);
+      }
+      if (d_equalityEngine.hasTerm(node) &&
+          d_equalityEngine.hasTerm(val)) {
+        if ((!invert && d_equalityEngine.areDisequal(node, val, true)) ||
+            (invert && d_equalityEngine.areEqual(node, val))) {
+          if (explain) {
+            d_equalityEngine.explainEquality(node, val, invert, assumptions);
+          }
+          return false;
+        }
+        if ((!invert && d_equalityEngine.areEqual(node, val)) ||
+            (invert && d_equalityEngine.areDisequal(node, val, true))) {
+          return true;
+        }
+      }
+      getSatContext()->push();
+      Node d = node.eqNode(val);
+      d_decisions.push_back(invert ? d.notNode() : d);
+      d_equalityEngine.assertEquality(d, !invert, d_decisions.back());
+      Debug("arrays-model-based") << "Asserting " << d_decisions.back() << " with explanation " << d_decisions.back() << endl;
+      ++d_numSetModelValSplits;
+      if (d_conflict) {
+        ++d_numSetModelValConflicts;
+        Debug("arrays-model-based") << "...which results in a conflict!" << endl;
+        d = d_decisions.back();
+        unsigned sz = assumptions.size();
+        convertNodeToAssumptions(d_conflictNode, assumptions, d);
+        unsigned sz2 = assumptions.size();
+        Assert(sz2 > sz);
+        Node explanation;
+        if (sz2 == sz+1) {
+          explanation = assumptions[sz];
+        }
+        else {
+          NodeBuilder<> conjunction(kind::AND);
+          for (unsigned i = sz; i < sz2; ++i) {
+            conjunction << assumptions[i];
+          }
+          explanation = conjunction;
+        }
+        //        assumptions.push_back(d);
+        //        d_lemmas.push_back(mkAnd(assumptions, true, sz));
+        // while (assumptions.size() > sz2) {
+        //   assumptions.pop_back();
+        // }
+        getSatContext()->pop();
+        d_decisions.pop_back();
+        d_permRef.push_back(explanation);
+        d = d.negate();
+        Debug("arrays-model-based") << "Asserting learned literal " << d << " with explanation " << explanation << endl;
+        bool eq = true;
+        if (d.getKind() == kind::NOT) {
+          d = d[0];
+          eq = false;
+        }
+        d_equalityEngine.assertEquality(d, eq, explanation);
+        if (d_conflict) {
+          Assert(false);
+        }
+        return false;
+      }
+      return true;
+    }
+  }
+  Unreachable();
+  return false;
+}
+
+
+Node TheoryArrays::mkAnd(std::vector<TNode>& conjunctions, bool invert, unsigned startIndex)
 {
   Assert(conjunctions.size() > 0);
 
   std::set<TNode> all;
   std::set<TNode> explained;
 
-  unsigned i = 0;
+  unsigned i = startIndex;
   TNode t;
   for (; i < conjunctions.size(); ++i) {
     t = conjunctions[i];
-
-    // Expand explanation resulting from propagating a ROW lemma
-    if (t.getKind() == kind::OR) {
+    if (t == d_true) {
+      continue;
+    }
+    else if (t.getKind() == kind::AND) {
+      for(TNode::iterator child_it = t.begin(); child_it != t.end(); ++child_it) {
+        if (*child_it == d_true) {
+          continue;
+        }
+        all.insert(*child_it);
+      }
+    }
+    else if (t.getKind() == kind::OR) {
+      // Expand explanation resulting from propagating a ROW lemma
       if ((explained.find(t) == explained.end())) {
         Assert(t[1].getKind() == kind::EQUAL);
         d_equalityEngine.explainEquality(t[1][0], t[1][1], false, conjunctions);
         explained.insert(t);
       }
-      continue;
     }
-    all.insert(t);
+    else {
+      all.insert(t);
+    }
   }
 
   if (all.size() == 0) {
-    return d_true;
+    return invert ? d_false : d_true;
   }
   if (all.size() == 1) {
     // All the same, or just one
-    return *(all.begin());
+    if (invert) {
+      return (*(all.begin())).negate();
+    }
+    else {
+      return *(all.begin());
+    }
   }
 
-  NodeBuilder<> conjunction(kind::AND);
+  NodeBuilder<> conjunction(invert ? kind::OR : kind::AND);
   std::set<TNode>::const_iterator it = all.begin();
   std::set<TNode>::const_iterator it_end = all.end();
   while (it != it_end) {
-    conjunction << *it;
+    if (invert) {
+      conjunction << (*it).negate();
+    }
+    else {
+      conjunction << *it;
+    }
     ++ it;
   }
 
@@ -951,6 +1731,7 @@ Node TheoryArrays::mkAnd(std::vector<TNode>& conjunctions)
 
 void TheoryArrays::setNonLinear(TNode a)
 {
+  if (options::arraysModelBased()) return;
   if (d_infoMap.isNonLinear(a)) return;
 
   Trace("arrays") << spaces(getSatContext()->getLevel()) << "Arrays::setNonLinear (" << a << ")\n";
@@ -1063,6 +1844,86 @@ void TheoryArrays::checkRIntro1(TNode a, TNode b)
 }
 
 
+Node TheoryArrays::removeRepLoops(TNode a, TNode rep)
+{
+  if (rep.getKind() != kind::STORE) {
+    Assert(isLeaf(rep));
+    TNode tmp = d_infoMap.getModelRep(d_equalityEngine.getRepresentative(rep));
+    if (!tmp.isNull()) {
+      Node tmp2 = removeRepLoops(a, tmp);
+      if (tmp != tmp2) {
+        return tmp2;
+      }
+    }
+    return rep;
+  }
+
+  Node s = removeRepLoops(a, rep[0]);
+  bool changed = (s != rep[0]);
+
+  Node index = rep[1];
+  Node value = rep[2];
+  Node lookup;
+
+  // TODO: Change to hasLoop?
+  if (!isLeaf(index)) {
+    changed = true;
+    index = getSkolem(index, "array_model_index_$$", index.getType(), "a new index variable from the theory of arrays", false);
+    if (!d_equalityEngine.hasTerm(index) ||
+        !d_equalityEngine.hasTerm(rep[1]) ||
+        !d_equalityEngine.areEqual(rep[1], index)) {
+      Node d = index.eqNode(rep[1]);
+      Debug("arrays-model-based") << "Asserting skolem equality " << d << endl;
+      d_equalityEngine.assertEquality(d, true, d_true);
+      d_modelConstraints.push_back(d);
+    }
+  }
+  if (!isLeaf(value)) {
+    changed = true;
+    value = getSkolem(value, "array_model_var_$$", value.getType(), "a new value variable from the theory of arrays", false);
+    if (!d_equalityEngine.hasTerm(value) ||
+        !d_equalityEngine.hasTerm(rep[2]) ||
+        !d_equalityEngine.areEqual(rep[2], value)) {
+      Node d = value.eqNode(rep[2]);
+      Debug("arrays-model-based") << "Asserting skolem equality " << d << endl;
+      d_equalityEngine.assertEquality(d, true, d_true);
+      d_modelConstraints.push_back(d);
+    }
+  }
+  if (changed) {
+    NodeManager* nm = NodeManager::currentNM();
+    return nm->mkNode(kind::STORE, s, index, value);
+  }
+  return rep;
+}
+
+
+Node TheoryArrays::expandStores(TNode s, vector<TNode>& assumptions, bool checkLoop, TNode a, TNode loopRep)
+{
+  if (s.getKind() != kind::STORE) {
+    Assert(isLeaf(s));
+    TNode tmp = d_equalityEngine.getRepresentative(s);
+    if (checkLoop && tmp == a) {
+      // Loop detected
+      d_equalityEngine.explainEquality(s, loopRep, true, assumptions);
+      return loopRep;
+    }
+    tmp = d_infoMap.getModelRep(tmp);
+    if (!tmp.isNull()) {
+      d_equalityEngine.explainEquality(s, tmp, true, assumptions);
+      return expandStores(tmp, assumptions, checkLoop, a, loopRep);
+    }
+    return s;
+  }
+  Node tmp = expandStores(s[0], assumptions, checkLoop, a, loopRep);
+  if (tmp != s[0]) {
+    NodeManager* nm = NodeManager::currentNM();
+    return nm->mkNode(kind::STORE, tmp, s[1], s[2]);
+  }
+  return s;
+}
+
+
 void TheoryArrays::mergeArrays(TNode a, TNode b)
 {
   // Note: a is the new representative
@@ -1085,7 +1946,7 @@ void TheoryArrays::mergeArrays(TNode a, TNode b)
       checkRIntro1(b, a);
     }
 
-    if (options::arraysOptimizeLinear()) {
+    if (options::arraysOptimizeLinear() && !options::arraysModelBased()) {
       bool aNL = d_infoMap.isNonLinear(a);
       bool bNL = d_infoMap.isNonLinear(b);
       if (aNL) {
@@ -1120,6 +1981,74 @@ void TheoryArrays::mergeArrays(TNode a, TNode b)
     checkRowLemmas(a,b);
     checkRowLemmas(b,a);
 
+    if (options::arraysModelBased()) {
+      TNode repA = d_infoMap.getModelRep(a);
+      Assert(repA.isNull() || d_equalityEngine.areEqual(a, repA));
+      TNode repB = d_infoMap.getModelRep(b);
+      Assert(repB.isNull() || d_equalityEngine.areEqual(a, repB));
+      Node rep;
+      bool done = false;
+      if (repA.isNull()) {
+        if (repB.isNull()) {
+          done = true;
+        }
+        else {
+          rep = repB;
+        }
+      }
+      else {
+        if (repB.isNull()) {
+          rep = repA;
+        }
+        else {
+          vector<TNode> assumptions;
+          rep = expandStores(repA, assumptions, true, a, repB);
+          if (rep != repA) {
+            Debug("arrays-model-based") << "Merging (" << a << "," << b << "): new rep is " << rep << endl;
+            d_infoMap.setModelRep(a, rep);
+            Node reason = mkAnd(assumptions);
+            d_permRef.push_back(reason);
+            d_equalityEngine.assertEquality(repA.eqNode(rep), true, reason);
+          }
+          d_modelConstraints.push_back(rep.eqNode(repB));
+          done = true;
+        }
+      }
+      if (!done) {
+        // 1. Check for store loop
+        TNode s = rep;
+        while (true) {
+          Assert(s.getKind() == kind::STORE);
+          while (s.getKind() == kind::STORE) {
+            s = s[0];
+          }
+          Assert(isLeaf(s));
+          TNode tmp = d_equalityEngine.getRepresentative(s);
+          if (tmp == a) {
+            d_modelConstraints.push_back(s.eqNode(rep));
+            rep = TNode();
+            break;
+          }
+          tmp = d_infoMap.getModelRep(tmp);
+          if (tmp.isNull()) {
+            break;
+          }
+          s = tmp;
+        }
+        if (!rep.isNull()) {
+          Node repOrig = rep;
+          rep = removeRepLoops(a, rep);
+          if (repOrig != rep) {
+            d_equalityEngine.assertEquality(repOrig.eqNode(rep), true, d_true);
+          }
+        }
+        if (rep != repA) {
+          Debug("arrays-model-based") << "Merging (" << a << "," << b << "): new rep is " << rep << endl;
+          d_infoMap.setModelRep(a, rep);
+        }
+      }
+    }
+
     // merge info adds the list of the 2nd argument to the first
     d_infoMap.mergeInfo(a, b);
 
@@ -1139,6 +2068,7 @@ void TheoryArrays::mergeArrays(TNode a, TNode b)
 
 
 void TheoryArrays::checkStore(TNode a) {
+  if (options::arraysModelBased()) return;
   Trace("arrays-cri")<<"Arrays::checkStore "<<a<<"\n";
 
   if(Trace.isOn("arrays-cri")) {
@@ -1168,6 +2098,7 @@ void TheoryArrays::checkStore(TNode a) {
 
 void TheoryArrays::checkRowForIndex(TNode i, TNode a)
 {
+  if (options::arraysModelBased()) return;
   Trace("arrays-cri")<<"Arrays::checkRowForIndex "<<a<<"\n";
   Trace("arrays-cri")<<"                   index "<<i<<"\n";
 
@@ -1211,6 +2142,7 @@ void TheoryArrays::checkRowForIndex(TNode i, TNode a)
 // look for new ROW lemmas
 void TheoryArrays::checkRowLemmas(TNode a, TNode b)
 {
+  if (options::arraysModelBased()) return;
   Trace("arrays-crl")<<"Arrays::checkLemmas begin \n"<<a<<"\n";
   if(Trace.isOn("arrays-crl"))
     d_infoMap.getInfo(a)->print();
@@ -1323,7 +2255,7 @@ void TheoryArrays::queueRowLemma(RowLemmaType lem)
   }
 
   // Prefer equality between indexes so as not to introduce new read terms
-  if (d_eagerIndexSplitting && !bothExist && !d_equalityEngine.areDisequal(i,j, false)) {
+  if (options::arraysEagerIndexSplitting() && !bothExist && !d_equalityEngine.areDisequal(i,j, false)) {
     Node i_eq_j = d_valuation.ensureLiteral(i.eqNode(j));
     getOutputChannel().requirePhase(i_eq_j, true);
     d_decisionRequests.push(i_eq_j);
@@ -1494,7 +2426,9 @@ void TheoryArrays::conflict(TNode a, TNode b) {
   } else {
     d_conflictNode = explain(a.eqNode(b));
   }
-  d_out->conflict(d_conflictNode);
+  if (!d_inCheckModel) {
+    d_out->conflict(d_conflictNode);
+  }
   d_conflict = true;
 }
 
diff --git a/src/theory/arrays/theory_arrays.h b/src/theory/arrays/theory_arrays.h
index 172482e71..b659a8e68 100644
--- a/src/theory/arrays/theory_arrays.h
+++ b/src/theory/arrays/theory_arrays.h
@@ -115,6 +115,14 @@ class TheoryArrays : public Theory {
   IntStat d_numNonLinear;
   /** splits on array variables */
   IntStat d_numSharedArrayVarSplits;
+  /** splits in getModelVal */
+  IntStat d_numGetModelValSplits;
+  /** conflicts in getModelVal */
+  IntStat d_numGetModelValConflicts;
+  /** splits in setModelVal */
+  IntStat d_numSetModelValSplits;
+  /** conflicts in setModelVal */
+  IntStat d_numSetModelValConflicts;
   /** time spent in check() */
   TimerStat d_checkTimer;
 
@@ -152,6 +160,7 @@ class TheoryArrays : public Theory {
   Node preprocessTerm(TNode term);
   Node recursivePreprocessTerm(TNode term);
   bool ppDisequal(TNode a, TNode b);
+  Node solveWrite(TNode term, bool solve1, bool solve2, bool ppCheck);
 
   public:
 
@@ -339,17 +348,24 @@ class TheoryArrays : public Theory {
   CDNodeSet d_sharedOther;
   context::CDO<bool> d_sharedTerms;
   context::CDList<TNode> d_reads;
-  std::hash_map<TNode, Node, TNodeHashFunction> d_diseqCache;
+  std::hash_map<Node, Node, NodeHashFunction> d_skolemCache;
+  context::CDO<unsigned> d_skolemIndex;
+  std::vector<Node> d_skolemAssertions;
 
   // The decision requests we have for the core
   context::CDQueue<Node> d_decisionRequests;
 
   // List of nodes that need permanent references in this context
   context::CDList<Node> d_permRef;
+  context::CDList<Node> d_modelConstraints;
+  std::vector<Node> d_lemmas;
 
-  Node mkAnd(std::vector<TNode>& conjunctions);
+  Node getSkolem(TNode ref, const std::string& name, const TypeNode& type, const std::string& comment, bool makeEqual = true);
+  Node mkAnd(std::vector<TNode>& conjunctions, bool invert = false, unsigned startIndex = 0);
   void setNonLinear(TNode a);
   void checkRIntro1(TNode a, TNode b);
+  Node removeRepLoops(TNode a, TNode rep);
+  Node expandStores(TNode s, std::vector<TNode>& assumptions, bool checkLoop = false, TNode a = TNode(), TNode b = TNode());
   void mergeArrays(TNode a, TNode b);
   void checkStore(TNode a);
   void checkRowForIndex(TNode i, TNode a);
@@ -357,6 +373,21 @@ class TheoryArrays : public Theory {
   void queueRowLemma(RowLemmaType lem);
   void dischargeLemmas();
 
+  std::vector<Node> d_decisions;
+  bool d_inCheckModel;
+  int d_topLevel;
+  void convertNodeToAssumptions(TNode node, std::vector<TNode>& assumptions, TNode nodeSkip);
+  void preRegisterStores(TNode s);
+  void checkModel(Effort e);
+  bool hasLoop(TNode node, TNode target);
+  typedef std::hash_map<Node, Node, NodeHashFunction> NodeMap;
+  NodeMap d_getModelValCache;
+  NodeMap d_lastVal;
+  Node getModelVal(TNode node);
+  Node getModelValRec(TNode node);
+  bool setModelVal(TNode node, TNode val, bool invert,
+                   bool explain, std::vector<TNode>& assumptions);
+
   public:
 
   eq::EqualityEngine* getEqualityEngine() {
diff --git a/src/theory/bv/Makefile.am b/src/theory/bv/Makefile.am
index ab6382770..a70521791 100644
--- a/src/theory/bv/Makefile.am
+++ b/src/theory/bv/Makefile.am
@@ -13,12 +13,18 @@ libbv_la_SOURCES = \
 	bitblaster.h \
 	bitblaster.cpp \
 	bv_subtheory.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 \
+	bv_subtheory_inequality.h \
+	bv_subtheory_inequality.cpp \
+	bv_inequality_graph.h \
+	bv_inequality_graph.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/bitblaster.cpp b/src/theory/bv/bitblaster.cpp
index 4f5325e10..d3a54a3e4 100644
--- a/src/theory/bv/bitblaster.cpp
+++ b/src/theory/bv/bitblaster.cpp
@@ -412,16 +412,43 @@ bool Bitblaster::isSharedTerm(TNode node) {
   return d_bv->d_sharedTermsSet.find(node) != d_bv->d_sharedTermsSet.end(); 
 }
 
-Node Bitblaster::getVarValue(TNode a) {
+bool Bitblaster::hasValue(TNode a) {
   Assert (d_termCache.find(a) != d_termCache.end()); 
   Bits bits = d_termCache[a];
+  for (int i = bits.size() -1; i >= 0; --i) {
+    SatValue bit_value; 
+    if (d_cnfStream->hasLiteral(bits[i])) { 
+      SatLiteral bit = d_cnfStream->getLiteral(bits[i]);
+      bit_value = d_satSolver->value(bit);
+      if (bit_value == SAT_VALUE_UNKNOWN)
+        return false; 
+    } else {
+      return false; 
+    }
+  }
+  return true; 
+}
+/** 
+ * Returns the value a is currently assigned to in the SAT solver
+ * or null if the value is completely unassigned. 
+ * 
+ * @param a 
+ * 
+ * @return 
+ */
+Node Bitblaster::getVarValue(TNode a) {
+  if (d_termCache.find(a) == d_termCache.end()) {
+    Assert(isSharedTerm(a));
+    return Node(); 
+  }
+  Bits bits = d_termCache[a];
   Integer value(0); 
   for (int i = bits.size() -1; i >= 0; --i) {
     SatValue bit_value;
     if (d_cnfStream->hasLiteral(bits[i])) { 
       SatLiteral bit = d_cnfStream->getLiteral(bits[i]);
       bit_value = d_satSolver->value(bit);
-      Assert (bit_value != SAT_VALUE_UNKNOWN);
+      Assert (bit_value != SAT_VALUE_UNKNOWN); 
     } else {
       // the bit is unconstrainted so we can give it an arbitrary value 
       bit_value = SAT_VALUE_FALSE;
@@ -436,8 +463,12 @@ void Bitblaster::collectModelInfo(TheoryModel* m) {
   __gnu_cxx::hash_set<TNode, TNodeHashFunction>::iterator it = d_variables.begin();
   for (; it!= d_variables.end(); ++it) {
     TNode var = *it;
-    if (Theory::theoryOf(var) == theory::THEORY_BV || isSharedTerm(var)) {
+    if (Theory::theoryOf(var) == theory::THEORY_BV || isSharedTerm(var))  {
       Node const_value = getVarValue(var);
+      if(const_value == Node()) {
+        // if the value is unassigned just set it to zero
+        const_value = utils::mkConst(BitVector(utils::getSize(var), 0u)); 
+      }
       Debug("bitvector-model") << "Bitblaster::collectModelInfo (assert (= "
                                 << var << " "
                                 << const_value << "))\n";
diff --git a/src/theory/bv/bitblaster.h b/src/theory/bv/bitblaster.h
index 21b389508..84a67e884 100644
--- a/src/theory/bv/bitblaster.h
+++ b/src/theory/bv/bitblaster.h
@@ -124,7 +124,8 @@ class Bitblaster {
   // division is bitblasted in terms of constraints
   // so it needs to use private bitblaster interface
   void bbUdiv(TNode node, Bits& bits);
-  void bbUrem(TNode node, Bits& bits); 
+  void bbUrem(TNode node, Bits& bits);
+  bool hasValue(TNode a); 
 public:
   void cacheTermDef(TNode node, Bits def); // public so we can cache remainder for division
   void bbTerm(TNode node, Bits&  bits);
@@ -164,9 +165,9 @@ public:
   }
 
   bool isSharedTerm(TNode node);
-private:
 
-  
+private:
+ 
   class Statistics {
   public:
     IntStat d_numTermClauses, d_numAtomClauses;
diff --git a/src/theory/bv/bv_inequality_graph.cpp b/src/theory/bv/bv_inequality_graph.cpp
new file mode 100644
index 000000000..499d362a9
--- /dev/null
+++ b/src/theory/bv/bv_inequality_graph.cpp
@@ -0,0 +1,466 @@
+/*********************                                                        */
+/*! \file bv_inequality_graph.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 A graph representation of the currently asserted bv inequalities. 
+ **
+ ** A graph representation of the currently asserted bv inequalities. 
+ **/
+
+#include "theory/bv/bv_inequality_graph.h"
+#include "theory/bv/theory_bv_utils.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;
+
+const TermId CVC4::theory::bv::UndefinedTermId = -1; 
+const ReasonId CVC4::theory::bv::UndefinedReasonId = -1;
+const ReasonId CVC4::theory::bv::AxiomReasonId = -2;
+
+
+bool InequalityGraph::addInequality(TNode a, TNode b, bool strict, TNode reason) {
+  Debug("bv-inequality") << "InequlityGraph::addInequality " << a << " " << b << " strict: " << strict << "\n"; 
+
+  TermId id_a = registerTerm(a);
+  TermId id_b = registerTerm(b);
+  ReasonId id_reason = registerReason(reason);
+
+  Assert (!(isConst(id_a) && isConst(id_b))); 
+  BitVector a_val = getValue(id_a);
+  BitVector b_val = getValue(id_b);
+    
+  unsigned bitwidth = utils::getSize(a); 
+  BitVector diff = strict ? BitVector(bitwidth, 1u) : BitVector(bitwidth, 0u);
+
+  if (a_val + diff < a_val) {
+    // we have an overflow
+    std::vector<ReasonId> conflict;
+    conflict.push_back(id_reason);
+    computeExplanation(UndefinedTermId, id_a, conflict);
+    setConflict(conflict);
+    return false; 
+  }
+  
+  if (a_val + diff <= b_val) {
+    // the inequality is true in the current partial model
+    // we still add the edge because it may not be true later (cardinality)
+    addEdge(id_a, id_b, strict, id_reason);
+    return true;
+  }
+
+  if (isConst(id_b) && a_val + diff > b_val) {
+    // we must be in a conflict since a has the minimum value that
+    // satisifes the constraints
+    std::vector<ReasonId> conflict;
+    conflict.push_back(id_reason);
+    computeExplanation(UndefinedTermId, id_a, conflict);
+    Debug("bv-inequality") << "InequalityGraph::addInequality conflict: constant UB \n"; 
+    setConflict(conflict);
+    return false; 
+  }
+  
+  // add the inequality edge
+  addEdge(id_a, id_b, strict, id_reason);
+  BFSQueue queue(&d_modelValues);
+  Assert (hasModelValue(id_a)); 
+  queue.push(id_a);
+  return processQueue(queue, id_a); 
+}
+
+bool InequalityGraph::updateValue(TermId id, ModelValue new_mv, TermId start, bool& changed) {
+  BitVector lower_bound = new_mv.value;
+  
+  if (isConst(id)) {
+    if (getValue(id) < lower_bound) {
+      Debug("bv-inequality") << "Conflict: constant " << getValue(id) << "\n"; 
+      std::vector<ReasonId> conflict;
+      TermId parent = new_mv.parent; 
+      ReasonId reason = new_mv.reason; 
+      conflict.push_back(reason); 
+      computeExplanation(UndefinedTermId, parent, conflict);
+      Debug("bv-inequality") << "InequalityGraph::addInequality conflict: constant\n"; 
+      setConflict(conflict); 
+      return false; 
+    }
+  } else {
+    // if not constant we can try to update the value
+    if (getValue(id) < lower_bound) {
+      // if we are updating the term we started with we must be in a cycle
+      if (id == start) {
+        TermId parent = new_mv.parent;
+        ReasonId reason = new_mv.reason;
+        std::vector<TermId> conflict;
+        conflict.push_back(reason);
+        computeExplanation(id, parent, conflict);
+        Debug("bv-inequality") << "InequalityGraph::addInequality conflict: cycle \n"; 
+        setConflict(conflict); 
+        return false; 
+      }
+      Debug("bv-inequality-internal") << "Updating " << getTermNode(id) 
+                                      << "  from " << getValue(id) << "\n"
+                                      << "  to " << lower_bound << "\n";
+      changed = true;
+      setModelValue(id, new_mv); 
+    }
+  }
+  return true; 
+}
+
+bool InequalityGraph::processQueue(BFSQueue& queue, TermId start) {
+  while (!queue.empty()) {
+    TermId current = queue.top();
+    queue.pop();
+    Debug("bv-inequality-internal") << "InequalityGraph::processQueue proceessing " << getTermNode(current) << "\n";
+  
+    BitVector current_value = getValue(current);
+  
+    unsigned size = getBitwidth(current);
+    const BitVector zero(size, 0u); 
+    const BitVector one(size, 1u); 
+  
+    const Edges& edges = getEdges(current);
+    for (Edges::const_iterator it = edges.begin(); it!= edges.end(); ++it) {
+      TermId next = it->next;
+      ReasonId reason = it->reason;
+
+      const BitVector increment = it->strict ? one : zero; 
+      const BitVector next_lower_bound = current_value + increment;
+
+      if (next_lower_bound < current_value) {
+        // it means we have an overflow and hence a conflict
+        std::vector<TermId> conflict;
+        conflict.push_back(it->reason);
+        computeExplanation(start, current, conflict);
+        Debug("bv-inequality") << "InequalityGraph::addInequality conflict: cycle \n"; 
+        setConflict(conflict); 
+        return false; 
+      }
+      
+      ModelValue new_mv(next_lower_bound, current, reason);       
+      bool updated = false; 
+      if (!updateValue(next, new_mv, start, updated)) {
+        return false; 
+      }
+      
+      if (next == start) {
+        // we know what we didn't update start or we would have had a conflict 
+        // this means we are in a cycle where all the values are forced to be equal
+        Debug("bv-inequality-internal") << "InequalityGraph::processQueue equal cycle."; 
+        continue; 
+      }
+      
+      if (!updated) {
+        // if we didn't update current we don't need to add to the queue it's children 
+        Debug("bv-inequality-internal") << "  unchanged " << getTermNode(next) << "\n";  
+        continue; 
+      }
+
+      queue.push(next);
+      Debug("bv-inequality-internal") << "   enqueue " << getTermNode(next) << "\n"; 
+    }
+  }
+  return true; 
+}
+
+void InequalityGraph::computeExplanation(TermId from, TermId to, std::vector<ReasonId>& explanation) {
+  if(Debug.isOn("bv-inequality")) {
+    if (from == UndefinedTermId) {
+      Debug("bv-inequality") << "InequalityGraph::computeExplanation " << getTermNode(to) << "\n";
+    } else {
+      Debug("bv-inequality") << "InequalityGraph::computeExplanation " << getTermNode(from) <<" => "
+                             << getTermNode(to) << "\n";
+    }
+  }
+
+  TermIdSet seen;
+
+  while(hasReason(to) && from != to && !seen.count(to)) {
+    seen.insert(to); 
+    const ModelValue& exp = getModelValue(to);
+    Assert (exp.reason != UndefinedReasonId); 
+    explanation.push_back(exp.reason);
+    Assert (exp.parent != UndefinedTermId); 
+    to = exp.parent; 
+    Debug("bv-inequality-internal") << "  parent: " << getTermNode(to) << "\n"
+                                    << "  reason: " << getReasonNode(exp.reason) << "\n"; 
+  }
+}
+
+void InequalityGraph::addEdge(TermId a, TermId b, bool strict, TermId reason) {
+  Debug("bv-inequality-internal") << "InequalityGraph::addEdge " << getTermNode(a) << " => " << getTermNode(b) << "\n"
+                                  << " strict ? " << strict << "\n"; 
+  Edges& edges = getEdges(a);
+  InequalityEdge new_edge(b, strict, reason); 
+  edges.push_back(new_edge);
+  d_undoStack.push_back(std::make_pair(a, new_edge));
+  d_undoStackIndex = d_undoStackIndex + 1; 
+}
+
+void InequalityGraph::initializeModelValue(TNode node) {
+  TermId id = getTermId(node); 
+  Assert (!hasModelValue(id));
+  bool isConst = node.getKind() == kind::CONST_BITVECTOR;
+  unsigned size = utils::getSize(node); 
+  BitVector value = isConst? node.getConst<BitVector>() : BitVector(size, 0u); 
+  setModelValue(id, ModelValue(value, UndefinedTermId, UndefinedReasonId));
+}
+
+bool InequalityGraph::isRegistered(TNode term) const {
+  return d_termNodeToIdMap.find(term) != d_termNodeToIdMap.end(); 
+}
+
+TermId InequalityGraph::registerTerm(TNode term) {
+  if (d_termNodeToIdMap.find(term) != d_termNodeToIdMap.end()) {
+    TermId id = d_termNodeToIdMap[term];
+    if (!hasModelValue(id)) {
+      // we could have backtracked and
+      initializeModelValue(term); 
+    }
+    return id; 
+  }
+
+  // store in node mapping
+  TermId id = d_termNodes.size();
+  Debug("bv-inequality-internal") << "InequalityGraph::registerTerm " << term << " => id"<< id << "\n"; 
+  
+  d_termNodes.push_back(term);
+  d_termNodeToIdMap[term] = id;
+  
+  // create InequalityNode
+  unsigned size = utils::getSize(term);
+
+  bool isConst = term.getKind() == kind::CONST_BITVECTOR;
+  InequalityNode ineq = InequalityNode(id, size, isConst);
+
+  Assert (d_ineqNodes.size() == id); 
+  d_ineqNodes.push_back(ineq);
+  
+  Assert (d_ineqEdges.size() == id); 
+  d_ineqEdges.push_back(Edges());
+
+  initializeModelValue(term); 
+  
+  return id; 
+}
+
+ReasonId InequalityGraph::registerReason(TNode reason) {
+  if (d_reasonToIdMap.find(reason) != d_reasonToIdMap.end()) {
+    return d_reasonToIdMap[reason]; 
+  }
+  ReasonId id = d_reasonNodes.size();
+  d_reasonNodes.push_back(reason);
+  d_reasonToIdMap[reason] = id;
+  return id; 
+}
+
+TNode InequalityGraph::getReasonNode(ReasonId id) const {
+  Assert (d_reasonNodes.size() > id);
+  return d_reasonNodes[id]; 
+}
+
+TNode InequalityGraph::getTermNode(TermId id) const {
+  Assert (d_termNodes.size() > id);
+  return d_termNodes[id]; 
+}
+
+TermId InequalityGraph::getTermId(TNode node) const {
+  Assert (d_termNodeToIdMap.find(node) != d_termNodeToIdMap.end());
+  return d_termNodeToIdMap.find(node)->second; 
+}
+
+void InequalityGraph::setConflict(const std::vector<ReasonId>& conflict) {
+  Assert (!d_inConflict); 
+  d_inConflict = true;
+  d_conflict.clear(); 
+  for (unsigned i = 0; i < conflict.size(); ++i) {
+    if (conflict[i] != AxiomReasonId) {
+      d_conflict.push_back(getReasonNode(conflict[i]));
+    }
+  }
+  if (Debug.isOn("bv-inequality")) {
+    Debug("bv-inequality") << "InequalityGraph::setConflict \n";
+    for (unsigned i = 0; i < d_conflict.size(); ++i) {
+      Debug("bv-inequality") << "   " << d_conflict[i] <<"\n"; 
+    }
+  }
+}
+
+void InequalityGraph::getConflict(std::vector<TNode>& conflict) {
+  for (unsigned i = 0; i < d_conflict.size(); ++i) {
+    conflict.push_back(d_conflict[i]); 
+  }
+}
+
+void InequalityGraph::setModelValue(TermId term, const ModelValue& mv) {
+  d_modelValues[term] = mv; 
+}
+
+InequalityGraph::ModelValue InequalityGraph::getModelValue(TermId term) const {
+  Assert (d_modelValues.find(term) != d_modelValues.end());
+  return (*(d_modelValues.find(term))).second; 
+}
+
+bool InequalityGraph::hasModelValue(TermId id) const {
+  return d_modelValues.find(id) != d_modelValues.end(); 
+}
+
+BitVector InequalityGraph::getValue(TermId id) const {
+  Assert (hasModelValue(id)); 
+  return (*(d_modelValues.find(id))).second.value;
+}
+
+bool InequalityGraph::hasReason(TermId id) const {
+  const ModelValue& mv = getModelValue(id);
+  return mv.reason != UndefinedReasonId; 
+}
+
+bool InequalityGraph::addDisequality(TNode a, TNode b, TNode reason) {
+  Debug("bv-inequality") << "InequalityGraph::addDisequality " << reason << "\n"; 
+  d_disequalities.push_back(reason);
+
+  if (!isRegistered(a) || !isRegistered(b)) {
+    //splitDisequality(reason);
+    return true; 
+  }
+  TermId id_a = getTermId(a);
+  TermId id_b = getTermId(b);
+  if (!hasModelValue(id_a)) {
+    initializeModelValue(a); 
+  }
+  if (!hasModelValue(id_b)) {
+    initializeModelValue(b); 
+  }
+  const BitVector val_a = getValue(id_a);
+  const BitVector val_b = getValue(id_b);
+  if (val_a == val_b) {
+    if (a.getKind() == kind::CONST_BITVECTOR) {
+      // then we know b cannot be smaller  than the assigned value so we try to make it larger
+      std::vector<ReasonId> explanation_ids; 
+      computeExplanation(UndefinedTermId, id_b, explanation_ids); 
+      std::vector<TNode> explanation_nodes;
+      explanation_nodes.push_back(reason);
+      for (unsigned i = 0; i < explanation_ids.size(); ++i) {
+        explanation_nodes.push_back(getReasonNode(explanation_ids[i])); 
+      }
+      Node explanation = utils::mkAnd(explanation_nodes);
+      d_reasonSet.insert(explanation); 
+      return addInequality(a, b, true, explanation);
+    }
+    if (b.getKind() == kind::CONST_BITVECTOR) {
+      // then we know b cannot be smaller  than the assigned value so we try to make it larger
+      std::vector<ReasonId> explanation_ids; 
+      computeExplanation(UndefinedTermId, id_a, explanation_ids); 
+      std::vector<TNode> explanation_nodes;
+      explanation_nodes.push_back(reason);
+      for (unsigned i = 0; i < explanation_ids.size(); ++i) {
+        explanation_nodes.push_back(getReasonNode(explanation_ids[i])); 
+      }
+      Node explanation = utils::mkAnd(explanation_nodes);
+      d_reasonSet.insert(explanation); 
+      return addInequality(b, a, true, explanation);
+    }
+    // if none of the terms are constants just add the lemma 
+    //splitDisequality(reason);
+  } else {
+    Debug("bv-inequality-internal") << "Disequal: " << a << " => " << val_a.toString(10) << "\n"
+                                    << "          " << b << " => " << val_b.toString(10) << "\n"; 
+  }
+  return true; 
+}
+
+// void InequalityGraph::splitDisequality(TNode diseq) {
+//   Debug("bv-inequality-internal")<<"InequalityGraph::splitDisequality " << diseq <<"\n"; 
+//   Assert (diseq.getKind() == kind::NOT && diseq[0].getKind() == kind::EQUAL);
+//   if (d_disequalitiesAlreadySplit.find(diseq) == d_disequalitiesAlreadySplit.end()) {
+//     d_disequalitiesToSplit.push_back(diseq); 
+//   }
+// }
+
+void InequalityGraph::backtrack() {
+  Debug("bv-inequality-internal") << "InequalityGraph::backtrack()\n"; 
+  int size = d_undoStack.size(); 
+  for (int i = size - 1; i >= (int)d_undoStackIndex.get(); --i) {
+    Assert (!d_undoStack.empty());
+    TermId id = d_undoStack.back().first; 
+    InequalityEdge edge = d_undoStack.back().second;
+    d_undoStack.pop_back();
+    
+    Debug("bv-inequality-internal") << " remove edge " << getTermNode(id) << " => "
+                                                       << getTermNode(edge.next) <<"\n"; 
+    Edges& edges = getEdges(id);
+    for (Edges::const_iterator it = edges.begin(); it!= edges.end(); ++it) {
+      Debug("bv-inequality-internal") << getTermNode(it->next) <<" " << it->strict << "\n"; 
+    }
+    Assert (!edges.empty());
+    Assert (edges.back() == edge);
+    edges.pop_back(); 
+  }
+}
+
+Node InequalityGraph::makeDiseqSplitLemma(TNode diseq) {
+  Assert (diseq.getKind() == kind::NOT && diseq[0].getKind() == kind::EQUAL);
+  TNode a = diseq[0][0];
+  TNode b = diseq[0][1];
+  Node a_lt_b = utils::mkNode(kind::BITVECTOR_ULT, a, b);
+  Node b_lt_a = utils::mkNode(kind::BITVECTOR_ULT, b, a);
+  Node eq = diseq[0]; 
+  Node lemma = utils::mkNode(kind::OR, a_lt_b, b_lt_a, eq);
+  return lemma; 
+}
+
+void InequalityGraph::checkDisequalities(std::vector<Node>& lemmas) {
+  for (CDQueue<TNode>::const_iterator it = d_disequalities.begin(); it != d_disequalities.end(); ++it) {
+    if (d_disequalitiesAlreadySplit.find(*it) == d_disequalitiesAlreadySplit.end()) {
+      // if we haven't already split on this disequality
+      TNode diseq = *it;
+      TermId a_id = registerTerm(diseq[0][0]);
+      TermId b_id = registerTerm(diseq[0][1]);
+      if (getValue(a_id) == getValue(b_id)) {
+        lemmas.push_back(makeDiseqSplitLemma(diseq));
+        d_disequalitiesAlreadySplit.insert(diseq);
+      }
+    }
+  }
+}
+
+bool InequalityGraph::isLessThan(TNode a, TNode b) {
+  Assert (isRegistered(a) && isRegistered(b));
+  Unimplemented(); 
+}
+
+bool InequalityGraph::hasValueInModel(TNode node) const {
+  if (isRegistered(node)) {
+    TermId id = getTermId(node);
+    return hasModelValue(id); 
+  }
+  return false; 
+}
+
+BitVector InequalityGraph::getValueInModel(TNode node) const {
+  TermId id = getTermId(node); 
+  Assert (hasModelValue(id));
+  return getValue(id); 
+}
+
+void InequalityGraph::getAllValuesInModel(std::vector<Node>& assignments) {
+  for (ModelValues::const_iterator it = d_modelValues.begin(); it != d_modelValues.end(); ++it) {
+    TermId id = (*it).first;
+    BitVector value = (*it).second.value;
+    TNode var = getTermNode(id);
+    Node constant = utils::mkConst(value);
+    Node assignment = utils::mkNode(kind::EQUAL, var, constant);
+    assignments.push_back(assignment); 
+    Debug("bitvector-model") << "   " << var <<" => " << constant << "\n"; 
+  }
+}
diff --git a/src/theory/bv/bv_inequality_graph.h b/src/theory/bv/bv_inequality_graph.h
new file mode 100644
index 000000000..d402b1561
--- /dev/null
+++ b/src/theory/bv/bv_inequality_graph.h
@@ -0,0 +1,290 @@
+/*********************                                                        */
+/*! \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"
+#include <queue>
+#include <list>
+namespace CVC4 {
+namespace theory {
+
+
+namespace bv {
+
+typedef unsigned TermId; 
+typedef unsigned ReasonId;
+extern const TermId UndefinedTermId;
+extern const ReasonId UndefinedReasonId;
+extern const ReasonId AxiomReasonId; 
+
+class InequalityGraph : public context::ContextNotifyObj{
+
+
+  context::Context* d_context;
+
+  struct InequalityEdge {
+    TermId next;
+    ReasonId reason;
+    bool strict;
+    InequalityEdge(TermId n, bool s, ReasonId r)
+      : next(n),
+        reason(r),
+        strict(s)
+    {}
+    bool operator==(const InequalityEdge& other) const {
+      return next == other.next && reason == other.reason && strict == other.strict; 
+    }
+  };
+
+  class InequalityNode {
+    TermId d_id;
+    unsigned d_bitwidth;
+    bool d_isConstant;
+  public:
+    InequalityNode(TermId id, unsigned bitwidth, bool isConst)
+      : d_id(id),
+        d_bitwidth(bitwidth),
+        d_isConstant(isConst)
+    {}
+    TermId getId() const { return d_id; }
+    unsigned getBitwidth() const { return d_bitwidth; }
+    bool isConstant() const { return d_isConstant; }
+  };
+
+  struct ModelValue {
+    TermId parent;
+    ReasonId reason;
+    BitVector value; 
+    ModelValue()
+      : parent(UndefinedTermId),
+        reason(UndefinedReasonId),
+        value(0, 0u)
+    {}
+    
+    ModelValue(const BitVector& val, TermId p, ReasonId r)
+      : parent(p),
+        reason(r),
+        value(val)
+    {}
+  };
+  
+  typedef context::CDHashMap<TermId, ModelValue> ModelValues;
+
+  struct QueueComparator {
+    const ModelValues* d_model;
+    QueueComparator(const ModelValues* model)
+      : d_model(model)
+    {}
+    bool operator() (TermId left, TermId right) const {
+      Assert (d_model->find(left) != d_model->end() &&
+              d_model->find(right) != d_model->end());
+      
+      return (*(d_model->find(left))).second.value < (*(d_model->find(right))).second.value; 
+    }
+  }; 
+
+  typedef __gnu_cxx::hash_map<TNode, ReasonId, TNodeHashFunction> ReasonToIdMap;
+  typedef __gnu_cxx::hash_map<TNode, TermId, TNodeHashFunction> TermNodeToIdMap;
+
+  typedef std::vector<InequalityEdge> Edges; 
+  typedef __gnu_cxx::hash_set<TermId> TermIdSet;
+
+  typedef std::priority_queue<TermId, std::vector<TermId>, QueueComparator> BFSQueue; 
+  typedef __gnu_cxx::hash_set<TNode, TNodeHashFunction> TNodeSet;
+  typedef __gnu_cxx::hash_set<Node, NodeHashFunction> NodeSet;
+
+  std::vector<InequalityNode> d_ineqNodes;
+  std::vector< Edges > d_ineqEdges;
+
+  // to keep the explanation nodes alive
+  NodeSet d_reasonSet; 
+  std::vector<TNode> d_reasonNodes;
+  ReasonToIdMap d_reasonToIdMap;
+  
+  std::vector<Node> d_termNodes;
+  TermNodeToIdMap d_termNodeToIdMap;
+
+  context::CDO<bool> d_inConflict;
+  std::vector<TNode> d_conflict;
+  bool d_signed; 
+
+  ModelValues  d_modelValues;
+  void initializeModelValue(TNode node); 
+  void setModelValue(TermId term, const ModelValue& mv);
+  ModelValue getModelValue(TermId term) const;
+  bool hasModelValue(TermId id) const; 
+  bool hasReason(TermId id) const; 
+  
+  /** 
+   * Registers the term by creating its corresponding InequalityNode
+   * and adding the min <= term <= max default edges. 
+   * 
+   * @param term 
+   * 
+   * @return 
+   */
+  TermId registerTerm(TNode term);
+  TNode getTermNode(TermId id) const; 
+  TermId getTermId(TNode node) const;
+  bool isRegistered(TNode term) const; 
+  
+  ReasonId registerReason(TNode reason);
+  TNode getReasonNode(ReasonId id) const;
+  
+  
+  Edges& getEdges(TermId id) { Assert (id < d_ineqEdges.size()); return d_ineqEdges[id]; }
+  InequalityNode& getInequalityNode(TermId id) { Assert (id < d_ineqNodes.size()); return d_ineqNodes[id]; }
+  const InequalityNode& getInequalityNode(TermId id) const { Assert (id < d_ineqNodes.size()); return d_ineqNodes[id]; }
+  unsigned getBitwidth(TermId id) const { return getInequalityNode(id).getBitwidth(); }
+  bool isConst(TermId id) const { return getInequalityNode(id).isConstant(); }
+  
+  BitVector getValue(TermId id) const; 
+    
+  void addEdge(TermId a, TermId b, bool strict, TermId reason);
+  
+  void setConflict(const std::vector<ReasonId>& conflict);
+  /** 
+   * If necessary update the value in the model of the current queue element. 
+   * 
+   * @param id current queue element we are updating
+   * @param start node we started with, to detect cycles
+   * 
+   * @return 
+   */
+  bool updateValue(TermId id, ModelValue new_mv, TermId start, bool& changed);
+  /** 
+   * Update the current model starting with the start term. 
+   * 
+   * @param queue 
+   * @param start 
+   * 
+   * @return 
+   */
+  bool processQueue(BFSQueue& queue, TermId start);
+  /** 
+   * Return the reasons why from <= to. If from is undefined we just
+   * explain the current value of to. 
+   * 
+   * @param from 
+   * @param to 
+   * @param explanation 
+   */
+  void computeExplanation(TermId from, TermId to, std::vector<ReasonId>& explanation); 
+  //  void splitDisequality(TNode diseq); 
+
+  /**
+     Disequality reasoning
+   */
+  
+  /*** The currently asserted disequalities */
+  context::CDQueue<TNode> d_disequalities;
+  NodeSet d_disequalitiesAlreadySplit; 
+  Node makeDiseqSplitLemma(TNode diseq); 
+  /** Backtracking mechanisms **/
+  std::vector<std::pair<TermId, InequalityEdge> > d_undoStack;
+  context::CDO<unsigned> d_undoStackIndex; 
+  
+  void contextNotifyPop() {
+    backtrack();
+  }
+
+  void backtrack(); 
+
+public:
+  
+  InequalityGraph(context::Context* c, bool s = false)
+    : ContextNotifyObj(c), 
+      d_context(c),
+      d_ineqNodes(),
+      d_ineqEdges(),
+      d_inConflict(c, false),
+      d_conflict(),
+      d_signed(s),
+      d_modelValues(c),
+      d_disequalities(c),
+      d_disequalitiesAlreadySplit(),
+      d_undoStack(),
+      d_undoStackIndex(c)
+  {}
+  /** 
+   * Add a new inequality to the graph 
+   * 
+   * @param a 
+   * @param b 
+   * @param strict 
+   * @param reason 
+   * 
+   * @return 
+   */
+  bool addInequality(TNode a, TNode b, bool strict, TNode reason);
+  /** 
+   * Add a new disequality to the graph. This may lead in a lemma. 
+   * 
+   * @param a 
+   * @param b 
+   * @param reason 
+   * 
+   * @return 
+   */
+  bool addDisequality(TNode a, TNode b, TNode reason); 
+  void getConflict(std::vector<TNode>& conflict);
+  virtual ~InequalityGraph() throw(AssertionException) {}
+  /** 
+   * Check that the currently asserted disequalities that have not been split on
+   * are still true in the current model. 
+   */
+  void checkDisequalities(std::vector<Node>& lemmas);
+  /** 
+   * Return true if a < b is entailed by the current set of assertions. 
+   * 
+   * @param a 
+   * @param b 
+   * 
+   * @return 
+   */
+  bool isLessThan(TNode a, TNode b);
+  /** 
+   * Returns true if the term has a value in the model (i.e. if we have seen it)
+   * 
+   * @param a 
+   * 
+   * @return 
+   */
+  bool hasValueInModel(TNode a) const;
+  /** 
+   * Return the value of a in the current model. 
+   * 
+   * @param a 
+   * 
+   * @return 
+   */
+  BitVector getValueInModel(TNode a) const;
+
+  void getAllValuesInModel(std::vector<Node>& assignments); 
+}; 
+
+}
+}
+}
+
+#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 4dbba0797..ed90e0ebe 100644
--- a/src/theory/bv/bv_subtheory.h
+++ b/src/theory/bv/bv_subtheory.h
@@ -32,8 +32,9 @@ class TheoryModel;
 namespace bv {
 
 enum SubTheory {
-  SUB_EQUALITY = 1,
-  SUB_BITBLAST = 2
+  SUB_CORE = 1,
+  SUB_BITBLAST = 2,
+  SUB_INEQUALITY = 3
 };
 
 inline std::ostream& operator << (std::ostream& out, SubTheory subtheory) {
@@ -41,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;
@@ -58,6 +61,7 @@ const bool d_useSatPropagation = true;
 // forward declaration 
 class TheoryBV; 
 
+typedef context::CDQueue<Node> AssertionQueue; 
 /**
  * Abstract base class for bit-vector subtheory solvers
  *
@@ -71,19 +75,34 @@ protected:
 
   /** The bit-vector theory */
   TheoryBV* d_bv;
-
+  AssertionQueue d_assertionQueue;
+  context::CDO<uint32_t>  d_assertionIndex;
 public:
   
   SubtheorySolver(context::Context* c, TheoryBV* bv) :
     d_context(c),
-    d_bv(bv)
+    d_bv(bv),
+    d_assertionQueue(c),
+    d_assertionIndex(c, 0)
   {}
   virtual ~SubtheorySolver() {}
-
-  virtual bool  addAssertions(const std::vector<TNode>& assertions, Theory::Effort e) = 0;
-  virtual void  explain(TNode literal, std::vector<TNode>& assumptions) = 0;
-  virtual void  preRegister(TNode node) {}
-  virtual void  collectModelInfo(TheoryModel* m) = 0; 
+  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(Theory::Effort e) {}
+  virtual void collectModelInfo(TheoryModel* m) = 0;
+  virtual Node getModelValue(TNode var) = 0; 
+  virtual bool isComplete() = 0;
+  virtual EqualityStatus getEqualityStatus(TNode a, TNode b) = 0;
+  virtual void addSharedTerm(TNode node) {} 
+  bool done() { return d_assertionQueue.size() == d_assertionIndex; }
+  TNode get() {
+    Assert (!done()); 
+    TNode res = d_assertionQueue[d_assertionIndex];
+    d_assertionIndex = d_assertionIndex + 1;
+    return res; 
+  }
+  virtual void assertFact(TNode fact) { d_assertionQueue.push_back(fact); }
 }; 
 
 }
diff --git a/src/theory/bv/bv_subtheory_bitblast.cpp b/src/theory/bv/bv_subtheory_bitblast.cpp
index f48a03975..30eaaa764 100644
--- a/src/theory/bv/bv_subtheory_bitblast.cpp
+++ b/src/theory/bv/bv_subtheory_bitblast.cpp
@@ -30,13 +30,23 @@ using namespace CVC4::theory::bv::utils;
 BitblastSolver::BitblastSolver(context::Context* c, TheoryBV* bv)
   : SubtheorySolver(c, bv),
     d_bitblaster(new Bitblaster(c, bv)),
-    d_bitblastQueue(c)
+    d_bitblastQueue(c),
+    d_statistics()
 {}
 
 BitblastSolver::~BitblastSolver() {
   delete d_bitblaster;
 }
 
+BitblastSolver::Statistics::Statistics()
+  : d_numCallstoCheck("theory::bv::BitblastSolver::NumCallsToCheck", 0)
+{
+  StatisticsRegistry::registerStat(&d_numCallstoCheck);
+}
+BitblastSolver::Statistics::~Statistics() {
+  StatisticsRegistry::unregisterStat(&d_numCallstoCheck);
+}
+
 void BitblastSolver::preRegister(TNode node) {
   if ((node.getKind() == kind::EQUAL ||
        node.getKind() == kind::BITVECTOR_ULT ||
@@ -52,22 +62,23 @@ void BitblastSolver::explain(TNode literal, std::vector<TNode>& assumptions) {
   d_bitblaster->explain(literal, assumptions);
 }
 
-bool BitblastSolver::addAssertions(const std::vector<TNode>& assertions, Theory::Effort e) {
-  Debug("bitvector::bitblaster") << "BitblastSolver::addAssertions (" << e << ")" << std::endl;
 
+bool BitblastSolver::check(Theory::Effort e) {
+  Debug("bv-bitblast") << "BitblastSolver::check (" << e << ")\n"; 
+  ++(d_statistics.d_numCallstoCheck); 
   //// Eager bit-blasting
   if (options::bitvectorEagerBitblast()) {
-    for (unsigned i = 0; i < assertions.size(); ++i) {
-      TNode atom = assertions[i].getKind() == kind::NOT ? assertions[i][0] : assertions[i];
+    while (!done()) {
+      TNode assertion = get(); 
+      TNode atom = assertion.getKind() == kind::NOT ? assertion[0] : assertion;
       if (atom.getKind() != kind::BITVECTOR_BITOF) {
         d_bitblaster->bbAtom(atom);
       }
+      return true;
     }
-    return true;
   }
 
   //// Lazy bit-blasting
-
   // bit-blast enqueued nodes
   while (!d_bitblastQueue.empty()) {
     TNode atom = d_bitblastQueue.front();
@@ -75,10 +86,11 @@ bool BitblastSolver::addAssertions(const std::vector<TNode>& assertions, Theory:
     d_bitblastQueue.pop();
   }
 
-  // propagation
-  for (unsigned i = 0; i < assertions.size(); ++i) {
-    TNode fact = assertions[i];
-    if (!d_bv->inConflict() && !d_bv->propagatedBy(fact, SUB_BITBLAST)) {
+  // Processing assertions  
+  while (!done()) {
+    TNode fact = get();
+    Debug("bv-bitblast") << "  fact " << fact << ")\n"; 
+    if (!d_bv->inConflict() && (!d_bv->wasPropagatedBySubtheory(fact) || d_bv->getPropagatingSubtheory(fact) != SUB_BITBLAST)) {
       // Some atoms have not been bit-blasted yet
       d_bitblaster->bbAtom(fact);
       // Assert to sat
@@ -103,7 +115,7 @@ bool BitblastSolver::addAssertions(const std::vector<TNode>& assertions, Theory:
     }
   }
 
-  // solving
+  // Solving
   if (e == Theory::EFFORT_FULL || options::bitvectorEagerFullcheck()) {
     Assert(!d_bv->inConflict());
     Debug("bitvector::bitblaster") << "BitblastSolver::addAssertions solving. \n";
@@ -129,5 +141,7 @@ void BitblastSolver::collectModelInfo(TheoryModel* m) {
 }
 
 Node BitblastSolver::getModelValue(TNode node) {
-  return d_bitblaster->getVarValue(node);
+  Node val = d_bitblaster->getVarValue(node);
+  Assert (val != Node() || d_bv->isSharedTerm(node));
+  return val; 
 }
diff --git a/src/theory/bv/bv_subtheory_bitblast.h b/src/theory/bv/bv_subtheory_bitblast.h
index 510006710..b6be84df5 100644
--- a/src/theory/bv/bv_subtheory_bitblast.h
+++ b/src/theory/bv/bv_subtheory_bitblast.h
@@ -30,23 +30,28 @@ class Bitblaster;
  * BitblastSolver
  */
 class BitblastSolver : public SubtheorySolver {
-
+  struct Statistics {
+    IntStat d_numCallstoCheck;
+    Statistics();
+    ~Statistics(); 
+  }; 
   /** Bitblaster */
   Bitblaster* d_bitblaster;
 
   /** Nodes that still need to be bit-blasted */
   context::CDQueue<TNode> d_bitblastQueue;
-
+  Statistics d_statistics; 
 public:
   BitblastSolver(context::Context* c, TheoryBV* bv);
   ~BitblastSolver();
 
   void  preRegister(TNode node);
-  bool  addAssertions(const std::vector<TNode>& assertions, Theory::Effort e);
+  bool  check(Theory::Effort e);
   void  explain(TNode literal, std::vector<TNode>& assumptions);
   EqualityStatus getEqualityStatus(TNode a, TNode b);
-  void collectModelInfo(TheoryModel* m);
+  void collectModelInfo(TheoryModel* m); 
   Node getModelValue(TNode node);
+  bool isComplete() { return true; }
 };
 
 }
diff --git a/src/theory/bv/bv_subtheory_core.cpp b/src/theory/bv/bv_subtheory_core.cpp
new file mode 100644
index 000000000..f8c26c35a
--- /dev/null
+++ b/src/theory/bv/bv_subtheory_core.cpp
@@ -0,0 +1,401 @@
+/*********************                                                        */
+/*! \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_core.h"
+
+#include "theory/bv/theory_bv.h"
+#include "theory/bv/theory_bv_utils.h"
+#include "theory/bv/slicer.h"
+#include "theory/model.h"
+#include "theory/bv/options.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)
+  : SubtheorySolver(c, bv),
+    d_notify(*this),
+    d_equalityEngine(d_notify, c, "theory::bv::TheoryBV"),
+    d_slicer(new Slicer()),
+    d_isCoreTheory(c, true),
+    d_reasons(c)
+{
+  if (d_useEqualityEngine) {
+
+    // The kinds we are treating as function application in congruence
+    d_equalityEngine.addFunctionKind(kind::BITVECTOR_CONCAT, true);
+    //    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, true);
+    d_equalityEngine.addFunctionKind(kind::BITVECTOR_PLUS, true);
+    d_equalityEngine.addFunctionKind(kind::BITVECTOR_EXTRACT, true);
+    //    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);
+  }
+}
+
+CoreSolver::~CoreSolver() {
+  delete d_slicer; 
+}
+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);
+      if (options::bitvectorCoreSolver()) {
+        d_slicer->processEquality(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);
+  }
+}
+
+Node CoreSolver::getBaseDecomposition(TNode a) {
+  std::vector<Node> a_decomp;
+  d_slicer->getBaseDecomposition(a, a_decomp);
+  Node new_a = utils::mkConcat(a_decomp);
+  Debug("bv-slicer") << "CoreSolver::getBaseDecomposition " << a <<" => " << new_a << "\n"; 
+  return new_a; 
+}
+
+bool CoreSolver::decomposeFact(TNode fact) {
+  Debug("bv-slicer") << "CoreSolver::decomposeFact fact=" << fact << endl;  
+  // 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
+  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];
+  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);
+
+  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;
+  
+  if (fact.getKind() == kind::EQUAL) {
+    // 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);
+        if (!ok) return false;
+      }
+    }
+  }
+  return true; 
+}
+
+bool CoreSolver::check(Theory::Effort e) {
+  Trace("bitvector::core") << "CoreSolver::check \n";
+  Assert (!d_bv->inConflict());
+  ++(d_statistics.d_numCallstoCheck); 
+  bool ok = true; 
+  std::vector<Node> core_eqs;
+  while (! done()) {
+    TNode fact = get(); 
+    
+    // update whether we are in the core fragment
+    if (d_isCoreTheory && !d_slicer->isCoreTerm(fact)) {
+      d_isCoreTheory = false; 
+    }
+    
+    // only reason about equalities
+    if (fact.getKind() == kind::EQUAL || (fact.getKind() == kind::NOT && fact[0].getKind() == kind::EQUAL)) {
+      if (options::bitvectorCoreSolver()) {
+        ok = decomposeFact(fact);
+      } else {
+        ok = assertFactToEqualityEngine(fact, fact);
+      }
+    } else {
+      ok = assertFactToEqualityEngine(fact, fact); 
+    }
+    if (!ok)
+      return false; 
+  }
+  
+  if (Theory::fullEffort(e) && isComplete()) {
+    buildModel();
+  }
+  
+  return true;
+}
+
+void CoreSolver::buildModel() {
+  if (options::bitvectorCoreSolver()) {
+    // FIXME
+    return; 
+  }
+  Debug("bv-core") << "CoreSolver::buildModel() \n"; 
+  d_modelValues.clear(); 
+  TNodeSet constants;
+  TNodeSet constants_in_eq_engine; 
+  // collect constants in equality engine
+  eq::EqClassesIterator eqcs_i = eq::EqClassesIterator(&d_equalityEngine); 
+  while (!eqcs_i.isFinished()) {
+    TNode repr = *eqcs_i;
+    if  (repr.getKind() == kind::CONST_BITVECTOR) {
+      // must check if it's just the constant
+      eq::EqClassIterator it(repr, &d_equalityEngine);
+      if (!(++it).isFinished() || true) {
+        constants.insert(repr);
+        constants_in_eq_engine.insert(repr); 
+      }
+    }
+    ++eqcs_i; 
+  }
+  // build repr to value map
+  
+  eqcs_i = eq::EqClassesIterator(&d_equalityEngine);
+  while (!eqcs_i.isFinished()) {
+    TNode repr = *eqcs_i;
+    ++eqcs_i; 
+    TypeNode type = repr.getType(); 
+    if (type.isBitVector() && repr.getKind()!= kind::CONST_BITVECTOR) {
+      Debug("bv-core-model") << "   processing " << repr <<"\n"; 
+      // we need to assign a value for it
+      TypeEnumerator te(type);
+      Node val; 
+      do {
+        val = *te; 
+        ++te;
+        // Debug("bv-core-model") << "  trying value " << val << "\n";
+        // Debug("bv-core-model") << "  is in set? " << constants.count(val) << "\n";
+        // Debug("bv-core-model") << "  enumerator done? " << te.isFinished() << "\n"; 
+      } while (constants.count(val) != 0 && !(te.isFinished()));
+      
+      if (te.isFinished() && constants.count(val) != 0) {
+        // if we cannot enumerate anymore values we just return the lemma stating that
+        // at least two of the representatives are equal.
+        std::vector<TNode> representatives;
+        representatives.push_back(repr);
+
+        for (TNodeSet::const_iterator it = constants_in_eq_engine.begin();
+             it != constants_in_eq_engine.end(); ++it) {
+          TNode constant = *it; 
+          if (utils::getSize(constant) == utils::getSize(repr)) {
+            representatives.push_back(constant); 
+          }
+        }
+        for (ModelValue::const_iterator it = d_modelValues.begin(); it != d_modelValues.end(); ++it) {
+          representatives.push_back(it->first);
+        }
+        std::vector<Node> equalities; 
+        for (unsigned i = 0; i < representatives.size(); ++i) {
+          for (unsigned j = i + 1; j < representatives.size(); ++j) {
+            TNode a = representatives[i];
+            TNode b = representatives[j];
+            if (utils::getSize(a) == utils::getSize(b)) {
+              equalities.push_back(utils::mkNode(kind::EQUAL, a, b));
+            }
+          }
+        }
+        Node lemma = utils::mkOr(equalities);
+        d_bv->lemma(lemma);
+        Debug("bv-core") << "  lemma: " << lemma << "\n"; 
+        return; 
+      }
+      Debug("bv-core-model") << "   " << repr << " => " << val <<"\n" ;
+      constants.insert(val);
+      d_modelValues[repr] = val; 
+    }
+  }
+}
+
+bool CoreSolver::assertFactToEqualityEngine(TNode fact, TNode reason) {
+  // Notify the equality engine 
+  if (d_useEqualityEngine && !d_bv->inConflict() && (!d_bv->wasPropagatedBySubtheory(fact) || !d_bv->getPropagatingSubtheory(fact) == SUB_CORE)) {
+    Debug("bv-slicer-eq") << "CoreSolver::assertFactToEqualityEngine fact=" << fact << endl;
+    // Debug("bv-slicer-eq") << "                     reason=" << reason << endl;
+    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) {
+  Debug("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) {
+  Debug("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_CORE);
+}
+
+void CoreSolver::conflict(TNode a, TNode b) {
+  std::vector<TNode> assumptions;
+  d_equalityEngine.explainEquality(a, b, true, assumptions);
+  Node conflict = flattenAnd(assumptions);
+  d_bv->setConflict(conflict);
+}
+
+void CoreSolver::collectModelInfo(TheoryModel* m) {
+  if (options::bitvectorCoreSolver()) {
+    Unreachable();
+    return; 
+  }
+  if (Debug.isOn("bitvector-model")) {
+    context::CDQueue<Node>::const_iterator it = d_assertionQueue.begin();
+    for (; it!= d_assertionQueue.end(); ++it) {
+      Debug("bitvector-model") << "CoreSolver::collectModelInfo (assert "
+                               << *it << ")\n";
+    }
+  }
+  set<Node> termSet;
+  d_bv->computeRelevantTerms(termSet);
+  m->assertEqualityEngine(&d_equalityEngine, &termSet);
+  if (isComplete()) {
+    Debug("bitvector-model") << "CoreSolver::collectModelInfo complete."; 
+    for (ModelValue::const_iterator it = d_modelValues.begin(); it != d_modelValues.end(); ++it) {
+      Node a = it->first;
+      Node b = it->second;
+      m->assertEquality(a, b, true); 
+    }
+  }
+}
+
+Node CoreSolver::getModelValue(TNode var) {
+  Assert (isComplete());
+  TNode repr = d_equalityEngine.getRepresentative(var);
+  if (repr.getKind() == kind::CONST_BITVECTOR) {
+    return repr; 
+  }
+  if (d_modelValues.find(repr) == d_modelValues.end()) {
+    // it may be a shared term that never gets asserted
+    Assert(d_bv->isSharedTerm(var));
+    return Node(); 
+  }
+  return d_modelValues[repr]; 
+}
+
+CoreSolver::Statistics::Statistics()
+  : d_numCallstoCheck("theory::bv::CoreSolver::NumCallsToCheck", 0)
+{
+  StatisticsRegistry::registerStat(&d_numCallstoCheck);
+}
+CoreSolver::Statistics::~Statistics() {
+  StatisticsRegistry::unregisterStat(&d_numCallstoCheck);
+}
diff --git a/src/theory/bv/bv_subtheory_eq.h b/src/theory/bv/bv_subtheory_core.h
index 2b024cfd4..d314b2fbf 100644
--- a/src/theory/bv/bv_subtheory_eq.h
+++ b/src/theory/bv/bv_subtheory_core.h
@@ -18,23 +18,34 @@
 
 #include "cvc4_private.h"
 #include "theory/bv/bv_subtheory.h"
+#include "context/cdhashmap.h"
+#include "context/cdhashset.h"
 
 namespace CVC4 {
 namespace theory {
 namespace bv {
 
+class Slicer; 
+class Base; 
 /**
  * Bitvector equality solver
  */
-class EqualitySolver : public SubtheorySolver {
+class CoreSolver : public SubtheorySolver {
+  typedef __gnu_cxx::hash_map<TNode, Node, TNodeHashFunction> ModelValue;
+  typedef __gnu_cxx::hash_set<TNode, TNodeHashFunction> TNodeSet; 
 
+  struct Statistics {
+    IntStat d_numCallstoCheck;
+    Statistics();
+    ~Statistics(); 
+  }; 
+  
   // NotifyClass: handles call-back from congruence closure module
-
   class NotifyClass : public eq::EqualityEngineNotify {
-    EqualitySolver& d_solver;
+    CoreSolver& d_solver;
 
   public:
-    NotifyClass(EqualitySolver& solver): d_solver(solver) {}
+    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);
@@ -43,12 +54,12 @@ class EqualitySolver : 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;
 
@@ -58,16 +69,26 @@ class EqualitySolver : public SubtheorySolver {
   /** 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);
+  Slicer* d_slicer;
+  context::CDO<bool> d_isCoreTheory;
+  /** To make sure we keep the explanations */
+  context::CDHashSet<Node, NodeHashFunction> d_reasons;
+  ModelValue d_modelValues;
+  void buildModel(); 
+  bool assertFactToEqualityEngine(TNode fact, TNode reason);  
+  bool decomposeFact(TNode fact);
+  Node getBaseDecomposition(TNode a);
+  Statistics d_statistics; 
+public: 
+  CoreSolver(context::Context* c, TheoryBV* bv);
+  ~CoreSolver();
+  bool  isComplete() { return d_isCoreTheory; }
+  void  setMasterEqualityEngine(eq::EqualityEngine* eq);
   void  preRegister(TNode node);
-  bool  addAssertions(const std::vector<TNode>& assertions, Theory::Effort e);
+  bool  check(Theory::Effort e);
   void  explain(TNode literal, std::vector<TNode>& assumptions);
   void  collectModelInfo(TheoryModel* m);
+  Node  getModelValue(TNode var); 
   void  addSharedTerm(TNode t) {
     d_equalityEngine.addTriggerTerm(t, THEORY_BV);
   }
@@ -82,6 +103,8 @@ public:
     }
     return EQUALITY_UNKNOWN;
   }
+  bool hasTerm(TNode node) const { return d_equalityEngine.hasTerm(node); }
+  void addTermToEqualityEngine(TNode node) { d_equalityEngine.addTerm(node); }
 };
 
 
diff --git a/src/theory/bv/bv_subtheory_eq.cpp b/src/theory/bv/bv_subtheory_eq.cpp
deleted file mode 100644
index 385c2e555..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, true);
-    //    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, true);
-    d_equalityEngine.addFunctionKind(kind::BITVECTOR_PLUS, true);
-    //    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_inequality.cpp b/src/theory/bv/bv_subtheory_inequality.cpp
new file mode 100644
index 000000000..17ac8a2e5
--- /dev/null
+++ b/src/theory/bv/bv_subtheory_inequality.cpp
@@ -0,0 +1,198 @@
+/*********************                                                        */
+/*! \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) {
+  Debug("bv-subtheory-inequality") << "InequalitySolveR::check("<< e <<")\n";
+  ++(d_statistics.d_numCallstoCheck);
+  
+  bool ok = true; 
+  while (!done() && ok) {
+    TNode fact = get();
+    Debug("bv-subtheory-inequality") << "  "<< fact <<"\n"; 
+    if (fact.getKind() == kind::EQUAL) {
+      TNode a = fact[0];
+      TNode b = fact[1];
+      ok = d_inequalityGraph.addInequality(a, b, false, fact);
+      if (ok)
+        ok = d_inequalityGraph.addInequality(b, a, false, fact); 
+    } else if (fact.getKind() == kind::NOT && fact[0].getKind() == kind::EQUAL) {
+      TNode a = fact[0][0];
+      TNode b = fact[0][1];
+      ok = d_inequalityGraph.addDisequality(a, b, fact);
+    }
+    if (fact.getKind() == kind::NOT && fact[0].getKind() == kind::BITVECTOR_ULE) {
+      TNode a = fact[0][1];
+      TNode b = fact[0][0]; 
+      ok = d_inequalityGraph.addInequality(a, b, true, fact);
+      // propagate
+      // if (d_bv->isSharedTerm(a) && d_bv->isSharedTerm(b)) {
+      //   Node neq = utils::mkNode(kind::NOT, utils::mkNode(kind::EQUAL, a, b)); 
+      //   d_bv->storePropagation(neq, SUB_INEQUALITY);
+      //   d_explanations[neq] = fact;
+      // }
+    } else if (fact.getKind() == kind::NOT && fact[0].getKind() == kind::BITVECTOR_ULT) {
+      TNode a = fact[0][1];
+      TNode b = fact[0][0]; 
+      ok = d_inequalityGraph.addInequality(a, b, false, fact);
+    } else if (fact.getKind() == kind::BITVECTOR_ULT) {
+      TNode a = fact[0];
+      TNode b = fact[1]; 
+      ok = d_inequalityGraph.addInequality(a, b, true, fact);
+      // propagate
+      // if (d_bv->isSharedTerm(a) && d_bv->isSharedTerm(b)) {
+      //   Node neq = utils::mkNode(kind::NOT, utils::mkNode(kind::EQUAL, a, b)); 
+      //   d_bv->storePropagation(neq, SUB_INEQUALITY);
+      //   d_explanations[neq] = fact;
+      // }
+    } else if (fact.getKind() == kind::BITVECTOR_ULE) {
+      TNode a = fact[0];
+      TNode b = fact[1]; 
+      ok = d_inequalityGraph.addInequality(a, b, false, fact);
+    }
+  }
+  
+  if (!ok) {
+    std::vector<TNode> conflict;
+    d_inequalityGraph.getConflict(conflict); 
+    d_bv->setConflict(utils::flattenAnd(conflict));
+    return false; 
+  }
+
+  if (isComplete() && Theory::fullEffort(e)) {
+    // make sure all the disequalities we didn't split on are still satisifed
+    // and split on the ones that are not
+    std::vector<Node> lemmas;
+    d_inequalityGraph.checkDisequalities(lemmas);
+    for(unsigned i = 0; i < lemmas.size(); ++i) {
+      d_bv->lemma(lemmas[i]); 
+    }
+  }
+  return true; 
+}
+
+EqualityStatus InequalitySolver::getEqualityStatus(TNode a, TNode b) {
+  Node a_lt_b = utils::mkNode(kind::BITVECTOR_ULT, a, b);
+  Node b_lt_a = utils::mkNode(kind::BITVECTOR_ULT, b, a);
+
+  // if an inequality containing the terms has been asserted then we know
+  // the equality is false
+  if (d_assertionSet.contains(a_lt_b) || d_assertionSet.contains(b_lt_a)) {
+    return EQUALITY_FALSE; 
+  }
+  
+  if (!d_inequalityGraph.hasValueInModel(a) ||
+      !d_inequalityGraph.hasValueInModel(b)) {
+    return EQUALITY_UNKNOWN; 
+  }
+
+  // TODO: check if this disequality is entailed by inequalities via transitivity
+  
+  BitVector a_val = d_inequalityGraph.getValueInModel(a);
+  BitVector b_val = d_inequalityGraph.getValueInModel(b);
+  
+  if (a_val == b_val) {
+    return EQUALITY_TRUE_IN_MODEL; 
+  } else {
+    return EQUALITY_FALSE_IN_MODEL; 
+  }
+}
+
+void InequalitySolver::assertFact(TNode fact) {
+  d_assertionQueue.push_back(fact);
+  d_assertionSet.insert(fact);
+  if (!isInequalityOnly(fact)) {
+    d_isComplete = false; 
+  }
+}
+
+bool InequalitySolver::isInequalityOnly(TNode node) {
+  if (d_ineqTermCache.find(node) != d_ineqTermCache.end()) {
+    return d_ineqTermCache[node]; 
+  }
+  
+  if (node.getKind() == kind::NOT) {
+    node = node[0]; 
+  }
+  
+  if (node.getKind() != kind::EQUAL &&
+      node.getKind() != kind::BITVECTOR_ULT &&
+      node.getKind() != kind::BITVECTOR_ULE &&
+      node.getKind() != kind::CONST_BITVECTOR &&
+      node.getKind() != kind::SELECT &&
+      node.getKind() != kind::STORE &&
+      node.getMetaKind() != kind::metakind::VARIABLE) {
+    return false; 
+  }
+  bool res = true; 
+  for (unsigned i = 0; i < node.getNumChildren(); ++i) {
+    res = res && isInequalityOnly(node[i]);
+  }
+  d_ineqTermCache[node] = res; 
+  return res; 
+}
+
+void InequalitySolver::explain(TNode literal, std::vector<TNode>& assumptions) {
+  Assert (d_explanations.find(literal) != d_explanations.end());
+  TNode explanation = d_explanations[literal];
+  assumptions.push_back(explanation);
+  Debug("bv-inequality-explain") << "InequalitySolver::explain " << literal << " with " << explanation <<"\n"; 
+}
+
+void InequalitySolver::propagate(Theory::Effort e) {
+  Assert (false); 
+}
+
+void InequalitySolver::collectModelInfo(TheoryModel* m) {
+  Debug("bitvector-model") << "InequalitySolver::collectModelInfo \n"; 
+  std::vector<Node> model;
+  d_inequalityGraph.getAllValuesInModel(model);
+  for (unsigned i = 0; i < model.size(); ++i) {
+    Assert (model[i].getKind() == kind::EQUAL); 
+    m->assertEquality(model[i][0], model[i][1], true); 
+  }
+}
+
+Node InequalitySolver::getModelValue(TNode var) {
+  Assert (isComplete());
+  if (!d_inequalityGraph.hasValueInModel(var)) {
+    Assert (d_bv->isSharedTerm(var));
+    return Node(); 
+  }
+  BitVector val = d_inequalityGraph.getValueInModel(var);
+  return utils::mkConst(val); 
+}
+
+InequalitySolver::Statistics::Statistics()
+  : d_numCallstoCheck("theory::bv::InequalitySolver::NumCallsToCheck", 0)
+{
+  StatisticsRegistry::registerStat(&d_numCallstoCheck);
+}
+InequalitySolver::Statistics::~Statistics() {
+  StatisticsRegistry::unregisterStat(&d_numCallstoCheck);
+}
+
diff --git a/src/theory/bv/bv_subtheory_inequality.h b/src/theory/bv/bv_subtheory_inequality.h
new file mode 100644
index 000000000..b02233b74
--- /dev/null
+++ b/src/theory/bv/bv_subtheory_inequality.h
@@ -0,0 +1,69 @@
+/*********************                                                        */
+/*! \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 "theory/bv/bv_subtheory.h"
+#include "theory/bv/bv_inequality_graph.h"
+#include "context/cdhashset.h"
+
+namespace CVC4 {
+namespace theory {
+namespace bv {
+
+class InequalitySolver: public SubtheorySolver {
+  struct Statistics {
+    IntStat d_numCallstoCheck;
+    Statistics();
+    ~Statistics(); 
+  }; 
+
+  context::CDHashSet<Node, NodeHashFunction> d_assertionSet; 
+  InequalityGraph d_inequalityGraph;
+  context::CDHashMap<Node, TNode, NodeHashFunction> d_explanations; 
+  context::CDO<bool> d_isComplete;
+  __gnu_cxx::hash_map<TNode, bool, TNodeHashFunction> d_ineqTermCache; 
+  bool isInequalityOnly(TNode node); 
+  Statistics d_statistics; 
+public:
+  InequalitySolver(context::Context* c, TheoryBV* bv)
+    : SubtheorySolver(c, bv),
+      d_assertionSet(c),
+      d_inequalityGraph(c),
+      d_explanations(c),
+      d_isComplete(c, true),
+      d_ineqTermCache(),
+      d_statistics()
+  {}
+  
+  bool check(Theory::Effort e);
+  void propagate(Theory::Effort e); 
+  void explain(TNode literal, std::vector<TNode>& assumptions);
+  bool isComplete() { return d_isComplete; }
+  void collectModelInfo(TheoryModel* m); 
+  Node getModelValue(TNode var); 
+  EqualityStatus getEqualityStatus(TNode a, TNode b);
+  void assertFact(TNode fact); 
+}; 
+
+}
+}
+}
+
+#endif /* __CVC4__THEORY__BV__BV_SUBTHEORY__INEQUALITY_H */ 
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/options b/src/theory/bv/options
index 72db63c09..cdc02c9ad 100644
--- a/src/theory/bv/options
+++ b/src/theory/bv/options
@@ -14,4 +14,10 @@ option bitvectorShareLemmas --bitblast-share-lemmas bool
 option bitvectorEagerFullcheck --bitblast-eager-fullcheck bool
  check the bitblasting eagerly
 
+option bitvectorInequalitySolver --bv-inequality-solver bool
+ turn on the inequality solver for the bit-vector theory 
+
+option bitvectorCoreSolver --bv-core-solver bool
+ turn on the core solver for the bit-vector theory 
+ 
 endmodule
diff --git a/src/theory/bv/slicer.cpp b/src/theory/bv/slicer.cpp
new file mode 100644
index 000000000..2837b075f
--- /dev/null
+++ b/src/theory/bv/slicer.cpp
@@ -0,0 +1,615 @@
+/*********************                                                        */
+/*! \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 "theory/bv/theory_bv_utils.h"
+#include "theory/rewriter.h"
+#include "theory/bv/options.h"
+using namespace CVC4;
+using namespace CVC4::theory;
+using namespace CVC4::theory::bv;
+using namespace std; 
+
+
+const TermId CVC4::theory::bv::UndefinedId = -1; 
+
+/**
+ * Base
+ * 
+ */
+Base::Base(uint32_t size) 
+  : d_size(size),
+    d_repr(size/32 + (size % 32 == 0? 0 : 1), 0)
+{
+  Assert (d_size > 0); 
+}
+
+  
+void Base::sliceAt(Index index) {
+  Index vector_index = index / 32;
+  if (vector_index == d_repr.size())
+    return;
+  
+  Index int_index = index % 32;
+  uint32_t bit_mask = utils::pow2(int_index); 
+  d_repr[vector_index] = d_repr[vector_index] | bit_mask; 
+}
+
+void Base::sliceWith(const Base& other) {
+  Assert (d_size == other.d_size);
+  for (unsigned i = 0; i < d_repr.size(); ++i) {
+    d_repr[i] = d_repr[i] | other.d_repr[i]; 
+  }
+}
+
+bool Base::isCutPoint (Index index) const {
+  // there is an implicit cut point at the end and begining of the bv
+  if (index == d_size || index == 0)
+    return true;
+    
+  Index vector_index = index / 32;
+  Assert (vector_index < d_size); 
+  Index int_index = index % 32;
+  uint32_t bit_mask = utils::pow2(int_index); 
+
+  return (bit_mask & d_repr[vector_index]) != 0; 
+}
+
+void Base::diffCutPoints(const Base& other, Base& res) const {
+  Assert (d_size == other.d_size && res.d_size == d_size);
+  for (unsigned i = 0; i < d_repr.size(); ++i) {
+    Assert (res.d_repr[i] == 0); 
+    res.d_repr[i] = d_repr[i] ^ other.d_repr[i]; 
+  }
+}
+
+bool Base::isEmpty() const {
+  for (unsigned i = 0; i< d_repr.size(); ++i) {
+    if (d_repr[i] != 0)
+      return false;
+  }
+  return true;
+}
+
+std::string Base::debugPrint() const {
+  std::ostringstream os;
+  os << "[";
+  bool first = true; 
+  for (int i = d_size - 1; i >= 0; --i) {
+    if (isCutPoint(i)) {
+      if (first)
+        first = false;
+      else
+        os <<"| "; 
+        
+      os << i ; 
+    }
+  }
+  os << "]"; 
+  return os.str(); 
+}
+
+/**
+ * ExtractTerm
+ *
+ */
+
+std::string ExtractTerm::debugPrint() const {
+  ostringstream os;
+  os << "id" << id << "[" << high << ":" << low <<"] ";  
+  return os.str(); 
+}
+
+/**
+ * NormalForm
+ *
+ */
+
+std::pair<TermId, Index> NormalForm::getTerm(Index index, const UnionFind& uf) const {
+  Assert (index < base.getBitwidth()); 
+  Index count = 0;
+  for (unsigned i = 0; i < decomp.size(); ++i) {
+    Index size = uf.getBitwidth(decomp[i]); 
+    if ( count + size > index && index >= count) {
+      return pair<TermId, Index>(decomp[i], count); 
+    }
+    count += size; 
+  }
+  Unreachable(); 
+}
+
+
+
+std::string NormalForm::debugPrint(const UnionFind& uf) const {
+  ostringstream os;
+  os << "NF " << base.debugPrint() << endl;
+  os << "("; 
+  for (int i = decomp.size() - 1; i>= 0; --i) {
+    os << decomp[i] << "[" << uf.getBitwidth(decomp[i]) <<"]";
+    os << (i != 0? ", " : "");  
+  }
+  os << ") \n"; 
+  return os.str(); 
+}
+/**
+ * UnionFind::Node
+ * 
+ */
+
+std::string UnionFind::Node::debugPrint() const {
+  ostringstream os;
+  os << "Repr " << d_repr << " ["<< d_bitwidth << "] ";
+  os << "( " << d_ch1 <<", " << d_ch0 << ")" << endl; 
+  return os.str(); 
+}
+
+
+/**
+ * UnionFind
+ * 
+ */
+TermId UnionFind::addTerm(Index bitwidth) {
+  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; 
+}
+/** 
+ * 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) {
+  Debug("bv-slicer") << "UnionFind::unionTerms " << t1.debugPrint() << " and \n"
+                     << "                      " << t2.debugPrint() << endl;
+  Assert (t1.getBitwidth() == t2.getBitwidth());
+  
+  NormalForm nf1(t1.getBitwidth());
+  NormalForm nf2(t2.getBitwidth());
+  
+  getNormalForm(t1, nf1);
+  getNormalForm(t2, nf2);
+
+  Assert (nf1.decomp.size() == nf2.decomp.size());
+  Assert (nf1.base == nf2.base);
+  
+  for (unsigned i = 0; i < nf1.decomp.size(); ++i) {
+    merge (nf1.decomp[i], nf2.decomp[i]); 
+  } 
+}
+
+/** 
+ * Merge the two terms in the union find. Both t1 and t2
+ * should be root terms. 
+ * 
+ * @param t1 
+ * @param t2 
+ */
+void UnionFind::merge(TermId t1, TermId t2) {
+  Debug("bv-slicer-uf") << "UnionFind::merge (" << t1 <<", " << t2 << ")" << endl;
+  ++(d_statistics.d_numMerges);
+  t1 = find(t1);
+  t2 = find(t2); 
+
+  if (t1 == t2)
+    return;
+
+  Assert (! hasChildren(t1) && ! hasChildren(t2));
+  setRepr(t1, t2); 
+  d_representatives.erase(t1);
+  d_statistics.d_numRepresentatives += -1; 
+}
+
+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; 
+}
+/** 
+ * Splits the representative of the term between i-1 and i
+ * 
+ * @param id the id of the term
+ * @param i the index we are splitting at
+ * 
+ * @return 
+ */
+void UnionFind::split(TermId id, Index i) {
+  Debug("bv-slicer-uf") << "UnionFind::split " << id << " at " << i << endl;
+  id = find(id); 
+  Debug("bv-slicer-uf") << "   node: " << d_nodes[id].debugPrint() << endl;
+
+  if (i == 0 || i == getBitwidth(id)) {
+    // nothing to do 
+    return;
+  }
+  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);
+    setChildren(id, top_id, bottom_id);
+
+  } else {
+    Index cut = getCutPoint(id); 
+    if (i < cut )
+      split(getChild(id, 0), i);
+    else
+      split(getChild(id, 1), i - cut); 
+  }
+  ++(d_statistics.d_numSplits);
+}
+
+void UnionFind::getNormalForm(const ExtractTerm& term, NormalForm& nf) {
+  nf.clear(); 
+  getDecomposition(term, nf.decomp);
+  // 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::getDecomposition(const ExtractTerm& term, Decomposition& decomp) {
+  // making sure the term is aligned
+  TermId id = find(term.id); 
+
+  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); 
+    getDecomposition(child_ex, decomp); 
+  }
+  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);
+    getDecomposition(child_ex, decomp); 
+  }
+  else {
+    // the extract is split over the two children
+    ExtractTerm low_child(getChild(id, 0), cut - 1, term.low);
+    getDecomposition(low_child, decomp);
+    ExtractTerm high_child(getChild(id, 1), term.high - cut, 0);
+    getDecomposition(high_child, decomp); 
+  }
+}
+/** 
+ * May cause reslicings of the decompositions. Must not assume the decompositons
+ * are the current normal form. 
+ * 
+ * @param d1 
+ * @param d2 
+ * @param common 
+ */
+void UnionFind::handleCommonSlice(const Decomposition& decomp1, const Decomposition& decomp2, TermId common) {
+  Debug("bv-slicer") << "UnionFind::handleCommonSlice common = " << common << endl; 
+  Index common_size = getBitwidth(common); 
+  // find starting points of common slice
+  Index start1 = 0;
+  for (unsigned j = 0; j < decomp1.size(); ++j) {
+    if (decomp1[j] == common)
+      break;
+    start1 += getBitwidth(decomp1[j]); 
+  }
+
+  Index start2 = 0; 
+  for (unsigned j = 0; j < decomp2.size(); ++j) {
+    if (decomp2[j] == common)
+      break;
+    start2 += getBitwidth(decomp2[j]); 
+  }
+  if (start1 > start2) {
+    Index temp = start1;
+    start1 = start2;
+    start2 = temp; 
+  }
+
+  if (start2 - start1 < common_size) {
+    Index overlap = start1 + common_size - start2;
+    Assert (overlap > 0);
+    Index diff = common_size - overlap;
+    Assert (diff >= 0);
+    Index granularity = utils::gcd(diff, overlap);
+    // split the common part 
+    for (unsigned i = 0; i < common_size; i+= granularity) {
+      split(common, i); 
+    }
+  }
+
+}
+
+void UnionFind::alignSlicings(const ExtractTerm& term1, const ExtractTerm& term2) {
+  Debug("bv-slicer") << "UnionFind::alignSlicings " << term1.debugPrint() << endl;
+  Debug("bv-slicer") << "                         " << term2.debugPrint() << endl;
+  NormalForm nf1(term1.getBitwidth());
+  NormalForm nf2(term2.getBitwidth());
+  
+  getNormalForm(term1, nf1);
+  getNormalForm(term2, nf2);
+
+  Assert (nf1.base.getBitwidth() == nf2.base.getBitwidth());
+  
+  // first check if the two have any common slices 
+  std::vector<TermId> intersection; 
+  utils::intersect(nf1.decomp, nf2.decomp, intersection); 
+  for (unsigned i = 0; i < intersection.size(); ++i) {
+    // handle common slice may change the normal form 
+    handleCommonSlice(nf1.decomp, nf2.decomp, intersection[i]); 
+  }
+  // propagate cuts to a fixpoint 
+  bool changed;
+  Base cuts(term1.getBitwidth()); 
+  do {
+    changed = false; 
+    // we need to update the normal form which may have changed 
+    getNormalForm(term1, nf1);
+    getNormalForm(term2, nf2); 
+
+    // align the cuts points of the two slicings
+    // FIXME: this can be done more efficiently
+    cuts.sliceWith(nf1.base);
+    cuts.sliceWith(nf2.base); 
+
+    for (unsigned i = 0; i < cuts.getBitwidth(); ++i) {
+      if (cuts.isCutPoint(i)) {
+        if (!nf1.base.isCutPoint(i)) {
+          pair<TermId, Index> pair1 = nf1.getTerm(i, *this);
+          split(pair1.first, i - pair1.second);
+          changed = true; 
+        }
+        if (!nf2.base.isCutPoint(i)) {
+          pair<TermId, Index> pair2 = nf2.getTerm(i, *this);
+          split(pair2.first, i - pair2.second);
+          changed = true; 
+        }
+      }
+    }
+  } while (changed); 
+}
+/** 
+ * Given an extract term a[i:j] makes sure a is sliced
+ * at indices i and j. 
+ * 
+ * @param term 
+ */
+void UnionFind::ensureSlicing(const ExtractTerm& term) {
+  //Debug("bv-slicer") << "Slicer::ensureSlicing " << term.debugPrint() << endl;
+  TermId id = find(term.id);
+  split(id, term.high + 1);
+  split(id, term.low);
+}
+
+/**
+ * Slicer
+ * 
+ */
+
+ExtractTerm Slicer::registerTerm(TNode node) {
+  Index low = 0, high = utils::getSize(node) - 1; 
+  TNode n = node; 
+  if (node.getKind() == kind::BITVECTOR_EXTRACT) {
+    n = node[0];
+    high = utils::getExtractHigh(node);
+    low = utils::getExtractLow(node); 
+  }
+  if (d_nodeToId.find(n) == d_nodeToId.end()) {
+    TermId id = d_unionFind.addTerm(utils::getSize(n)); 
+    d_nodeToId[n] = id;
+    d_idToNode[id] = n; 
+  }
+  TermId id = d_nodeToId[n];
+  ExtractTerm res(id, high, low); 
+  Debug("bv-slicer") << "Slicer::registerTerm " << node << " => " << res.debugPrint() << endl;
+  return res; 
+}
+
+void Slicer::processEquality(TNode eq) {
+  Debug("bv-slicer") << "Slicer::processEquality: " << eq << endl;
+  
+  Assert (eq.getKind() == kind::EQUAL);
+  TNode a = eq[0];
+  TNode b = eq[1];
+  ExtractTerm a_ex= registerTerm(a);
+  ExtractTerm b_ex= registerTerm(b);
+  
+  d_unionFind.ensureSlicing(a_ex);
+  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) {
+  Debug("bv-slicer") << "Slicer::getBaseDecomposition " << node << endl;
+  
+  Index high = utils::getSize(node) - 1;
+  Index low = 0;
+  TNode top = node; 
+  if (node.getKind() == kind::BITVECTOR_EXTRACT) {
+    high = utils::getExtractHigh(node);
+    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);
+  
+  // construct actual extract nodes
+  unsigned size = utils::getSize(node); 
+  Index current_low = size;
+  Index current_high = size; 
+  for (int i = nf.decomp.size() - 1; i >= 0; --i) {
+    Index current_size = d_unionFind.getBitwidth(nf.decomp[i]); 
+    current_low -= current_size; 
+    Node current = Rewriter::rewrite(utils::mkExtract(node, current_high - 1, current_low));
+    current_high = current_low;
+    decomp.push_back(current); 
+  }
+
+  Debug("bv-slicer") << "as [";
+  for (unsigned i = 0; i < decomp.size(); ++i) {
+    Debug("bv-slicer") << decomp[i] <<" "; 
+  }
+  Debug("bv-slicer") << "]" << endl;
+
+}
+
+bool Slicer::isCoreTerm(TNode node) {
+  if (d_coreTermCache.find(node) == d_coreTermCache.end()) {
+    Kind kind = node.getKind();
+    bool not_core;
+    if (options::bitvectorCoreSolver()) {
+      not_core = (kind != kind::BITVECTOR_EXTRACT && kind != kind::BITVECTOR_CONCAT); 
+    } else {
+      not_core = true; 
+    }
+    if (not_core &&
+        kind != kind::EQUAL &&
+        kind != kind::NOT &&
+        kind != kind::STORE &&
+        kind != kind::SELECT &&
+        node.getMetaKind() != kind::metakind::VARIABLE &&
+        kind != kind::CONST_BITVECTOR) {
+      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]; 
+}
+unsigned Slicer::d_numAddedEqualities = 0; 
+
+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) {
+    int size = 0;
+    // no need to count the last child since the end cut point is implicit 
+    for (int i = t1.getNumChildren() - 1; i >= 1 ; --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() - 1; i >= 1; --i) {
+      size = size + utils::getSize(t2[i]);
+      base2.sliceAt(size); 
+    }
+  }
+
+  base1.sliceWith(base2); 
+  if (!base1.isEmpty()) {
+    // 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 = utils::mkExtract(t1, i-1, last);
+        Node extract2 = utils::mkExtract(t2, i-1, last);
+        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);
+  }
+  d_numAddedEqualities += equalities.size() - 1; 
+} 
+
+std::string UnionFind::debugPrint(TermId id) {
+  ostringstream os; 
+  if (hasChildren(id)) {
+    TermId id1 = find(getChild(id, 1));
+    TermId id0 = find(getChild(id, 0));
+    os << debugPrint(id1);
+    os << debugPrint(id0); 
+  } else {
+    if (getRepr(id) == UndefinedId) {
+      os <<"id"<< id <<"[" << getBitwidth(id) <<"] "; 
+    } else {
+      os << debugPrint(find(id));
+    }
+  }
+  return os.str(); 
+}
+
+UnionFind::Statistics::Statistics():
+  d_numNodes("theory::bv::slicer::NumberOfNodes", 0),
+  d_numRepresentatives("theory::bv::slicer::NumberOfRepresentatives", 0),
+  d_numSplits("theory::bv::slicer::NumberOfSplits", 0),
+  d_numMerges("theory::bv::slicer::NumberOfMerges", 0),
+  d_avgFindDepth("theory::bv::slicer::AverageFindDepth"),
+  d_numAddedEqualities("theory::bv::slicer::NumberOfEqualitiesAdded", Slicer::d_numAddedEqualities)
+{
+  StatisticsRegistry::registerStat(&d_numRepresentatives);
+  StatisticsRegistry::registerStat(&d_numSplits);
+  StatisticsRegistry::registerStat(&d_numMerges);
+  StatisticsRegistry::registerStat(&d_avgFindDepth);
+  StatisticsRegistry::registerStat(&d_numAddedEqualities);
+}
+
+UnionFind::Statistics::~Statistics() {
+  StatisticsRegistry::unregisterStat(&d_numRepresentatives);
+  StatisticsRegistry::unregisterStat(&d_numSplits);
+  StatisticsRegistry::unregisterStat(&d_numMerges);
+  StatisticsRegistry::unregisterStat(&d_avgFindDepth);
+  StatisticsRegistry::unregisterStat(&d_numAddedEqualities);
+}
diff --git a/src/theory/bv/slicer.h b/src/theory/bv/slicer.h
new file mode 100644
index 000000000..88254b983
--- /dev/null
+++ b/src/theory/bv/slicer.h
@@ -0,0 +1,255 @@
+/*********************                                                        */
+/*! \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 <math.h>
+
+#include "util/bitvector.h"
+#include "util/statistics_registry.h"
+#include "util/index.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 Index TermId;
+extern const TermId UndefinedId;
+
+
+/** 
+ * Base
+ * 
+ */
+class Base {
+  Index d_size;
+  std::vector<uint32_t> d_repr;
+public:
+  Base(Index size);
+  void sliceAt(Index index); 
+  void sliceWith(const Base& other);
+  bool isCutPoint(Index index) const;
+  void diffCutPoints(const Base& other, Base& res) const;
+  bool isEmpty() const;
+  std::string debugPrint() const;
+  Index getBitwidth() const { return d_size; }
+  void clear() {
+    for (unsigned i = 0; i < d_repr.size(); ++i) {
+      d_repr[i] = 0; 
+    }
+  }
+  bool operator==(const Base& other) const {
+    if (other.getBitwidth() != getBitwidth())
+      return false;
+    for (unsigned i = 0; i < d_repr.size(); ++i) {
+      if (d_repr[i] != other.d_repr[i])
+        return false;
+    }
+    return true; 
+  }
+}; 
+
+/**
+ * UnionFind
+ * 
+ */
+typedef __gnu_cxx::hash_set<TermId> TermSet;
+typedef std::vector<TermId> Decomposition; 
+
+struct ExtractTerm {
+  TermId id;
+  Index high;
+  Index low;
+  ExtractTerm(TermId i, Index h, Index l)
+    : id (i),
+      high(h),
+      low(l)
+  {
+    Assert (h >= l && id != UndefinedId); 
+  }
+  Index getBitwidth() const { return high - low + 1; }
+  std::string debugPrint() const; 
+};
+
+class UnionFind; 
+
+struct NormalForm {
+  Base base;
+  Decomposition decomp;
+
+  NormalForm(Index bitwidth)
+    : base(bitwidth),
+      decomp()
+  {}
+  /** 
+   * Returns the term in the decomposition on which the index i
+   * falls in
+   * @param i 
+   * 
+   * @return 
+   */
+  std::pair<TermId, Index> getTerm(Index i, const UnionFind& uf) const;
+  std::string debugPrint(const UnionFind& uf) const;
+  void clear() { base.clear(); decomp.clear(); }
+};
+
+
+class UnionFind {
+  class Node {
+    Index d_bitwidth;
+    TermId d_ch1, d_ch0;
+    TermId d_repr;
+  public:
+    Node(Index b)
+  : d_bitwidth(b),
+    d_ch1(UndefinedId),
+    d_ch0(UndefinedId), 
+    d_repr(UndefinedId)
+    {}
+    
+    TermId getRepr() const { return d_repr; }
+    Index getBitwidth() const { return d_bitwidth; }
+    bool hasChildren() const { return d_ch1 != UndefinedId && d_ch0 != UndefinedId; }
+
+    TermId getChild(Index i) const {
+      Assert (i < 2);
+      return i == 0? d_ch0 : d_ch1;
+    }
+    void setRepr(TermId id) {
+      Assert (! hasChildren());
+      d_repr = id;
+    }
+    void setChildren(TermId ch1, TermId ch0) {
+      Assert (d_repr == UndefinedId && !hasChildren());
+      d_ch1 = ch1;
+      d_ch0 = ch0; 
+    }
+    std::string debugPrint() const;
+  };
+  
+  /// 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
+  TermSet d_representatives;
+  
+  void getDecomposition(const ExtractTerm& term, Decomposition& decomp);
+  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(); 
+  }
+  TermId getChild(TermId id, Index i) const {
+    Assert (id < d_nodes.size());
+    return d_nodes[id].getChild(i); 
+  }
+  Index getCutPoint(TermId id) const {
+    return getBitwidth(getChild(id, 0)); 
+  }
+  bool hasChildren(TermId id) const {
+    Assert (id < d_nodes.size());
+    return d_nodes[id].hasChildren(); 
+  }
+  /// setter methods for the internal nodes
+  void setRepr(TermId id, TermId new_repr) {
+    Assert (id < d_nodes.size());
+    d_nodes[id].setRepr(new_repr); 
+  }
+  void setChildren(TermId id, TermId ch1, TermId ch0) {
+    Assert (id < d_nodes.size() && getBitwidth(id) == getBitwidth(ch1) + getBitwidth(ch0));
+    d_nodes[id].setChildren(ch1, ch0); 
+  }
+
+  class Statistics {
+  public:
+    IntStat d_numNodes; 
+    IntStat d_numRepresentatives;
+    IntStat d_numSplits;
+    IntStat d_numMerges;
+    AverageStat d_avgFindDepth;
+    ReferenceStat<unsigned> d_numAddedEqualities; 
+    //IntStat d_numAddedEqualities; 
+    Statistics();
+    ~Statistics();
+  };
+
+  Statistics d_statistics
+;
+  
+public:
+  UnionFind()
+    : d_nodes(),
+      d_representatives()
+  {}
+
+  TermId addTerm(Index bitwidth);
+  void unionTerms(const ExtractTerm& t1, const ExtractTerm& t2); 
+  void merge(TermId t1, TermId t2);
+  TermId find(TermId t1); 
+  void split(TermId term, Index i);
+
+  void getNormalForm(const ExtractTerm& term, NormalForm& nf);
+  void alignSlicings(const ExtractTerm& term1, const ExtractTerm& term2);
+  void ensureSlicing(const ExtractTerm& term);
+  Index getBitwidth(TermId id) const {
+    Assert (id < d_nodes.size());
+    return d_nodes[id].getBitwidth(); 
+  }
+  std::string debugPrint(TermId id);
+  friend class Slicer; 
+};
+
+class Slicer {
+  __gnu_cxx::hash_map<TermId, TNode> d_idToNode;
+  __gnu_cxx::hash_map<TNode, TermId, TNodeHashFunction> d_nodeToId;
+  __gnu_cxx::hash_map<TNode, bool, TNodeHashFunction> d_coreTermCache;
+  UnionFind d_unionFind;
+  ExtractTerm registerTerm(TNode node); 
+public:
+  Slicer()
+    : d_idToNode(),
+      d_nodeToId(),
+      d_coreTermCache(),
+      d_unionFind()
+  {}
+  
+  void getBaseDecomposition(TNode node, std::vector<Node>& decomp);
+  void processEquality(TNode eq);
+  bool isCoreTerm (TNode node);
+  static void splitEqualities(TNode node, std::vector<Node>& equalities);
+  static unsigned d_numAddedEqualities; 
+}; 
+
+
+}/* 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 e28ef3ddf..b202b7eca 100644
--- a/src/theory/bv/theory_bv.cpp
+++ b/src/theory/bv/theory_bv.cpp
@@ -17,10 +17,14 @@
 
 #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"
 #include "theory/bv/theory_bv_rewrite_rules_normalization.h"
+#include "theory/bv/bv_subtheory_core.h"
+#include "theory/bv/bv_subtheory_inequality.h"
+#include "theory/bv/bv_subtheory_bitblast.h"
 #include "theory/model.h"
 
 using namespace CVC4;
@@ -31,46 +35,68 @@ using namespace CVC4::context;
 using namespace std;
 using namespace CVC4::theory::bv::utils;
 
-
-
-
 TheoryBV::TheoryBV(context::Context* c, context::UserContext* u, OutputChannel& out, Valuation valuation, const LogicInfo& logicInfo, QuantifiersEngine* qe)
   : Theory(THEORY_BV, c, u, out, valuation, logicInfo, qe),
     d_context(c),
     d_alreadyPropagatedSet(c),
     d_sharedTermsSet(c),
-    d_bitblastSolver(c, this),
-    d_equalitySolver(c, this),
+    d_subtheories(),
+    d_subtheoryMap(),
     d_statistics(),
     d_conflict(c, false),
     d_literalsToPropagate(c),
     d_literalsToPropagateIndex(c, 0),
     d_propagatedBy(c)
-  {}
-
-TheoryBV::~TheoryBV() {}
+  {
+    SubtheorySolver* core_solver = new CoreSolver(c, this); 
+    d_subtheories.push_back(core_solver);
+    d_subtheoryMap[SUB_CORE] = core_solver;
+
+    if (options::bitvectorInequalitySolver()) {
+      SubtheorySolver* ineq_solver = new InequalitySolver(c, this); 
+      d_subtheories.push_back(ineq_solver);
+      d_subtheoryMap[SUB_INEQUALITY] = ineq_solver;
+    }
+    
+    SubtheorySolver* bb_solver = new BitblastSolver(c, this); 
+    d_subtheories.push_back(bb_solver);
+    d_subtheoryMap[SUB_BITBLAST] = bb_solver;
+  }
 
+TheoryBV::~TheoryBV() {
+  for (unsigned i = 0; i < d_subtheories.size(); ++i) {
+    delete d_subtheories[i]; 
+  }
+}
 
 void TheoryBV::setMasterEqualityEngine(eq::EqualityEngine* eq) {
-  d_equalitySolver.setMasterEqualityEngine(eq);
+  dynamic_cast<CoreSolver*>(d_subtheoryMap[SUB_CORE])->setMasterEqualityEngine(eq);
 }
 
 TheoryBV::Statistics::Statistics():
   d_avgConflictSize("theory::bv::AvgBVConflictSize"),
   d_solveSubstitutions("theory::bv::NumberOfSolveSubstitutions", 0),
-  d_solveTimer("theory::bv::solveTimer")
+  d_solveTimer("theory::bv::solveTimer"),
+  d_numCallsToCheckFullEffort("theory::bv::NumberOfFullCheckCalls", 0),
+  d_numCallsToCheckStandardEffort("theory::bv::NumberOfStandardCheckCalls", 0)
 {
   StatisticsRegistry::registerStat(&d_avgConflictSize);
   StatisticsRegistry::registerStat(&d_solveSubstitutions);
   StatisticsRegistry::registerStat(&d_solveTimer);
+  StatisticsRegistry::registerStat(&d_numCallsToCheckFullEffort);
+  StatisticsRegistry::registerStat(&d_numCallsToCheckStandardEffort);
 }
 
 TheoryBV::Statistics::~Statistics() {
   StatisticsRegistry::unregisterStat(&d_avgConflictSize);
   StatisticsRegistry::unregisterStat(&d_solveSubstitutions);
   StatisticsRegistry::unregisterStat(&d_solveTimer);
+  StatisticsRegistry::unregisterStat(&d_numCallsToCheckFullEffort);
+  StatisticsRegistry::unregisterStat(&d_numCallsToCheckStandardEffort);
 }
 
+
+
 void TheoryBV::preRegisterTerm(TNode node) {
   Debug("bitvector-preregister") << "TheoryBV::preRegister(" << node << ")" << std::endl;
 
@@ -78,9 +104,9 @@ void TheoryBV::preRegisterTerm(TNode node) {
     // don't use the equality engine in the eager bit-blasting
     return;
   }
-
-  d_bitblastSolver.preRegister(node);
-  d_equalitySolver.preRegister(node);
+  for (unsigned i = 0; i < d_subtheories.size(); ++i) {
+    d_subtheories[i]->preRegister(node); 
+  }
 }
 
 void TheoryBV::sendConflict() {
@@ -98,51 +124,65 @@ void TheoryBV::sendConflict() {
 void TheoryBV::check(Effort e)
 {
   Debug("bitvector") << "TheoryBV::check(" << e << ")" << std::endl;
-
+  if (Theory::fullEffort(e)) {
+    ++(d_statistics.d_numCallsToCheckFullEffort); 
+  } else {
+    ++(d_statistics.d_numCallsToCheckStandardEffort); 
+  }
   // if we are already in conflict just return the conflict
   if (inConflict()) {
     sendConflict();
     return;
   }
 
-  // getting the new assertions
-  std::vector<TNode> new_assertions;
   while (!done()) {
-    Assertion assertion = get();
-    TNode fact = assertion.assertion;
-    new_assertions.push_back(fact);
-    Debug("bitvector-assertions") << "TheoryBV::check assertion " << fact << "\n";
-  }
-
-  if (!inConflict()) {
-    // sending assertions to the equality solver first
-    d_equalitySolver.addAssertions(new_assertions, e);
+    TNode fact = get().assertion;
+    for (unsigned i = 0; i < d_subtheories.size(); ++i) {
+      d_subtheories[i]->assertFact(fact); 
+    }
   }
 
-  if (!inConflict()) {
-    // sending assertions to the bitblast solver
-    d_bitblastSolver.addAssertions(new_assertions, e);
-  }
+  bool ok = true;
+  bool complete = false;
+  for (unsigned i = 0; i < d_subtheories.size(); ++i) {
+    Assert (!inConflict()); 
+    ok = d_subtheories[i]->check(e);
+    complete = d_subtheories[i]->isComplete(); 
 
-  if (inConflict()) {
-    sendConflict();
+    if (!ok) {
+      // if we are in a conflict no need to check with other theories
+      Assert (inConflict());
+      sendConflict();
+      return; 
+    }
+    if (complete) {
+      // if the last subtheory was complete we stop
+      return; 
+    }
   }
 }
 
 void TheoryBV::collectModelInfo( TheoryModel* m, bool fullModel ){
   Assert(!inConflict());
   //  Assert (fullModel); // can only query full model
-  d_equalitySolver.collectModelInfo(m); 
-  d_bitblastSolver.collectModelInfo(m); 
-  
+  for (unsigned i = 0; i < d_subtheories.size(); ++i) {
+    if (d_subtheories[i]->isComplete()) {
+      d_subtheories[i]->collectModelInfo(m);
+      return; 
+    }
+  }
 }
 
 Node TheoryBV::getModelValue(TNode var) {
   Assert(!inConflict());
-  return d_bitblastSolver.getModelValue(var);
+  for (unsigned i = 0; i < d_subtheories.size(); ++i) {
+    if (d_subtheories[i]->isComplete()) {
+      return d_subtheories[i]->getModelValue(var); 
+    }
+  }
+  Unreachable(); 
 }
 
-
 void TheoryBV::propagate(Effort e) {
   Debug("bitvector") << indent() << "TheoryBV::propagate()" << std::endl;
 
@@ -193,16 +233,25 @@ Theory::PPAssertStatus TheoryBV::ppAssert(TNode in, SubstitutionMap& outSubstitu
   return PP_ASSERT_STATUS_UNSOLVED;
 }
 
-
 Node TheoryBV::ppRewrite(TNode t)
 {
   if (RewriteRule<BitwiseEq>::applies(t)) {
     Node result = RewriteRule<BitwiseEq>::run<false>(t);
     return Rewriter::rewrite(result);
   }
+
+  if (options::bitvectorCoreSolver() && t.getKind() == kind::EQUAL) {
+    std::vector<Node> equalities;
+    Slicer::splitEqualities(t, equalities);
+    return utils::mkAnd(equalities); 
+  }
+  
   return t;
 }
 
+void TheoryBV::presolve() {
+  Debug("bitvector") << "TheoryBV::presolve" << endl; 
+}
 
 bool TheoryBV::storePropagation(TNode literal, SubTheory subtheory)
 {
@@ -226,6 +275,7 @@ bool TheoryBV::storePropagation(TNode literal, SubTheory subtheory)
       // Safe to ignore this one, subtheory should produce a conflict
       return true;
     }
+ 
     d_propagatedBy[literal] = subtheory;
   }
 
@@ -233,7 +283,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();
@@ -247,15 +297,9 @@ 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)) {
-    Debug("bitvector::explain") << "TheoryBV::explain(" << literal << "): EQUALITY" << std::endl;
-    d_equalitySolver.explain(literal, assumptions);
-  } else {
-    Assert(propagatedBy(literal, SUB_BITBLAST));
-    Debug("bitvector::explain") << "TheoryBV::explain(" << literal << ") : BITBLASTER" << std::endl;
-    d_bitblastSolver.explain(literal, assumptions);
-  }
+  Assert (wasPropagatedBySubtheory(literal));
+  SubTheory sub = getPropagatingSubtheory(literal);
+  d_subtheoryMap[sub]->explain(literal, assumptions);
 }
 
 
@@ -280,7 +324,9 @@ 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);
+    for (unsigned i = 0; i < d_subtheories.size(); ++i) {
+      d_subtheories[i]->addSharedTerm(t);
+    }
   }
 }
 
@@ -290,12 +336,13 @@ EqualityStatus TheoryBV::getEqualityStatus(TNode a, TNode b)
   if (options::bitvectorEagerBitblast()) {
     return EQUALITY_UNKNOWN;
   }
-
-  EqualityStatus status = d_equalitySolver.getEqualityStatus(a, b);
-  if (status == EQUALITY_UNKNOWN) {
-    status = d_bitblastSolver.getEqualityStatus(a, b);
+  
+  for (unsigned i = 0; i < d_subtheories.size(); ++i) {
+    EqualityStatus status = d_subtheories[i]->getEqualityStatus(a, b);
+    if (status != EQUALITY_UNKNOWN) {
+      return status; 
+    }
   }
-
-  return status;
+  return EQUALITY_UNKNOWN; ;
 }
 
diff --git a/src/theory/bv/theory_bv.h b/src/theory/bv/theory_bv.h
index ffb043bb6..ff8b3a8b1 100644
--- a/src/theory/bv/theory_bv.h
+++ b/src/theory/bv/theory_bv.h
@@ -25,15 +25,16 @@
 #include "context/cdhashset.h"
 #include "theory/bv/theory_bv_utils.h"
 #include "util/statistics_registry.h"
-#include "context/cdqueue.h"
 #include "theory/bv/bv_subtheory.h"
-#include "theory/bv/bv_subtheory_eq.h"
-#include "theory/bv/bv_subtheory_bitblast.h"
 
 namespace CVC4 {
 namespace theory {
 namespace bv {
 
+class CoreSolver;
+class InequalitySolver;
+class BitblastSolver; 
+
 class TheoryBV : public Theory {
 
   /** The context we are using */
@@ -42,9 +43,9 @@ class TheoryBV : public Theory {
   /** Context dependent set of atoms we already propagated */
   context::CDHashSet<Node, NodeHashFunction> d_alreadyPropagatedSet;
   context::CDHashSet<Node, NodeHashFunction> d_sharedTermsSet;
-
-  BitblastSolver d_bitblastSolver;
-  EqualitySolver d_equalitySolver;
+  
+  std::vector<SubtheorySolver*> d_subtheories;
+  __gnu_cxx::hash_map<SubTheory, SubtheorySolver*, std::hash<int> > d_subtheoryMap; 
 public:
 
   TheoryBV(context::Context* c, context::UserContext* u, OutputChannel& out, Valuation valuation, const LogicInfo& logicInfo, QuantifiersEngine* qe);
@@ -67,6 +68,7 @@ public:
   PPAssertStatus ppAssert(TNode in, SubstitutionMap& outSubstitutions);
   Node ppRewrite(TNode t);
 
+  void presolve();
 private:
 
   class Statistics {
@@ -74,6 +76,8 @@ private:
     AverageStat d_avgConflictSize;
     IntStat     d_solveSubstitutions;
     TimerStat   d_solveTimer;
+    IntStat d_numCallsToCheckFullEffort;
+    IntStat d_numCallsToCheckStandardEffort; 
     Statistics();
     ~Statistics();
   };
@@ -99,10 +103,14 @@ private:
   typedef context::CDHashMap<Node, SubTheory, NodeHashFunction> PropagatedMap;
   PropagatedMap d_propagatedBy;
 
-  bool propagatedBy(TNode literal, SubTheory subtheory) const {
+  bool wasPropagatedBySubtheory(TNode literal) const {
+    return d_propagatedBy.find(literal) != d_propagatedBy.end(); 
+  }
+  
+  SubTheory getPropagatingSubtheory(TNode literal) const {
+    Assert(wasPropagatedBySubtheory(literal)); 
     PropagatedMap::const_iterator find = d_propagatedBy.find(literal);
-    if (find == d_propagatedBy.end()) return false;
-    else return (*find).second == subtheory;
+    return (*find).second;
   }
 
   /** Should be called to propagate the literal.  */
@@ -115,6 +123,8 @@ private:
 
   void addSharedTerm(TNode t);
 
+  bool isSharedTerm(TNode t) { return d_sharedTermsSet.contains(t); }
+  
   EqualityStatus getEqualityStatus(TNode a, TNode b);
 
   Node getModelValue(TNode var);
@@ -136,10 +146,13 @@ private:
 
   void sendConflict();
 
+  void lemma(TNode node) { d_out->lemma(node); }
+  
   friend class Bitblaster;
   friend class BitblastSolver;
   friend class EqualitySolver;
-
+  friend class CoreSolver;
+  friend class InequalitySolver; 
 };/* class TheoryBV */
 
 }/* CVC4::theory::bv namespace */
diff --git a/src/theory/bv/theory_bv_utils.h b/src/theory/bv/theory_bv_utils.h
index 7d851d0fb..f8b9f010e 100644
--- a/src/theory/bv/theory_bv_utils.h
+++ b/src/theory/bv/theory_bv_utils.h
@@ -31,6 +31,12 @@ namespace theory {
 namespace bv {
 namespace utils {
 
+inline uint32_t pow2(uint32_t power) {
+  Assert (power < 32); 
+  uint32_t one = 1;
+  return one << power; 
+}
+
 inline unsigned getExtractHigh(TNode node) {
   return node.getOperator().getConst<BitVectorExtract>().high;
 }
@@ -63,28 +69,6 @@ inline Node mkVar(unsigned size) {
   return nm->mkSkolem("bv_$$", nm->mkBitVectorType(size), "is a variable created by the theory of bitvectors"); 
 }
 
-inline Node mkAnd(std::vector<TNode>& children) {
-  std::set<TNode> distinctChildren;
-  distinctChildren.insert(children.begin(), children.end());
-  
-  if (children.size() == 0) {
-    return mkTrue();
-  }
-  
-  if (children.size() == 1) {
-    return *children.begin();
-  }
-  
-  NodeBuilder<> conjunction(kind::AND);
-  std::set<TNode>::const_iterator it = distinctChildren.begin();
-  std::set<TNode>::const_iterator it_end = distinctChildren.end();
-  while (it != it_end) {
-    conjunction << *it;
-    ++ it;
-  }
-
-  return conjunction;
-}
 
 inline Node mkSortedNode(Kind kind, std::vector<Node>& children) {
   Assert (kind == kind::BITVECTOR_AND ||
@@ -149,14 +133,6 @@ inline Node mkXor(TNode node1, TNode node2) {
 }
 
 
-inline Node mkAnd(std::vector<Node>& children) {
-  if(children.size() > 1) {
-    return NodeManager::currentNM()->mkNode(kind::AND, children);
-  } else {
-    return children[0];
-  }
-}
-
 inline Node mkExtract(TNode node, unsigned high, unsigned low) {
   Node extractOp = NodeManager::currentNM()->mkConst<BitVectorExtract>(BitVectorExtract(high, low));
   std::vector<Node> children;
@@ -262,7 +238,6 @@ inline Node mkConjunction(const std::set<TNode> nodes) {
   return conjunction;
 }
 
-
 inline unsigned isPow2Const(TNode node) {
   if (node.getKind() != kind::CONST_BITVECTOR) {
     return false; 
@@ -272,6 +247,109 @@ inline unsigned isPow2Const(TNode node) {
   return bv.isPow2(); 
 }
 
+typedef __gnu_cxx::hash_set<TNode, TNodeHashFunction> TNodeSet;
+
+inline Node mkOr(const std::vector<Node>& nodes) {
+  std::set<TNode> all;
+  all.insert(nodes.begin(), nodes.end());
+
+  if (all.size() == 0) {
+    return mkTrue(); 
+  }
+  
+  if (all.size() == 1) {
+    // All the same, or just one
+    return nodes[0];
+  }
+  
+
+  NodeBuilder<> disjunction(kind::OR);
+  std::set<TNode>::const_iterator it = all.begin();
+  std::set<TNode>::const_iterator it_end = all.end();
+  while (it != it_end) {
+    disjunction << *it;
+    ++ it;
+  }
+
+  return disjunction; 
+}/* mkOr() */
+
+                 
+inline Node mkAnd(const std::vector<TNode>& conjunctions) {
+  std::set<TNode> all;
+  all.insert(conjunctions.begin(), conjunctions.end());
+
+  if (all.size() == 0) {
+    return mkTrue(); 
+  }
+  
+  if (all.size() == 1) {
+    // All the same, or just one
+    return conjunctions[0];
+  }
+  
+
+  NodeBuilder<> conjunction(kind::AND);
+  std::set<TNode>::const_iterator it = all.begin();
+  std::set<TNode>::const_iterator it_end = all.end();
+  while (it != it_end) {
+    conjunction << *it;
+    ++ it;
+  }
+
+  return conjunction;
+}/* mkAnd() */
+
+inline Node mkAnd(const std::vector<Node>& conjunctions) {
+  std::set<TNode> all;
+  all.insert(conjunctions.begin(), conjunctions.end());
+
+  if (all.size() == 0) {
+    return mkTrue(); 
+  }
+  
+  if (all.size() == 1) {
+    // All the same, or just one
+    return conjunctions[0];
+  }
+  
+
+  NodeBuilder<> conjunction(kind::AND);
+  std::set<TNode>::const_iterator it = all.begin();
+  std::set<TNode>::const_iterator it_end = all.end();
+  while (it != it_end) {
+    conjunction << *it;
+    ++ it;
+  }
+
+  return conjunction;
+}/* mkAnd() */
+
+
+
+inline Node flattenAnd(std::vector<TNode>& queue) {
+  TNodeSet nodes;
+  while(!queue.empty()) {
+    TNode current = queue.back();
+    queue.pop_back();
+    if (current.getKind() ==  kind::AND) {
+      for (unsigned i = 0; i < current.getNumChildren(); ++i) {
+        if (nodes.count(current[i]) == 0) {
+          queue.push_back(current[i]);
+        }
+      }
+    } else {
+      nodes.insert(current); 
+    }
+  }
+  std::vector<TNode> children; 
+  for (TNodeSet::const_iterator it = nodes.begin(); it!= nodes.end(); ++it) {
+    children.push_back(*it); 
+  }
+  return mkAnd(children); 
+}
+
+
 // neeed a better name, this is not technically a ground term 
 inline bool isBVGroundTerm(TNode node) {
   if (node.getNumChildren() == 0) {
@@ -350,27 +428,7 @@ inline Node mkConjunction(const std::vector<TNode>& nodes) {
 }
 
 
-inline Node mkAnd(const std::vector<TNode>& conjunctions) {
-  Assert(conjunctions.size() > 0);
-
-  std::set<TNode> all;
-  all.insert(conjunctions.begin(), conjunctions.end());
-
-  if (all.size() == 1) {
-    // All the same, or just one
-    return conjunctions[0];
-  }
-
-  NodeBuilder<> conjunction(kind::AND);
-  std::set<TNode>::const_iterator it = all.begin();
-  std::set<TNode>::const_iterator it_end = all.end();
-  while (it != it_end) {
-    conjunction << *it;
-    ++ it;
-  }
 
-  return conjunction;
-}/* mkAnd() */
 
 
 // Turn a set into a string
@@ -406,6 +464,35 @@ inline std::string vectorToString(const std::vector<Node>& nodes) {
   return out.str();
 }
 
+// FIXME: dumb code 
+inline void intersect(const std::vector<uint32_t>& v1,
+                      const std::vector<uint32_t>& v2,
+                      std::vector<uint32_t>& intersection) {
+  for (unsigned i = 0; i < v1.size(); ++i) {
+    bool found = false;
+    for (unsigned j = 0; j < v2.size(); ++j) {
+      if (v2[j] == v1[i]) {
+        found = true;
+        break;
+      }
+    }
+    if (found) {
+      intersection.push_back(v1[i]); 
+    }
+  }
+}
+
+template <class T>
+inline T gcd(T a, T b) {
+  while (b != 0) {
+    T t = b;
+    b = a % t;
+    a = t;
+  }
+  return a;
+}
+
+
 }
 }
 }
diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp
index b89ca8fa4..1c297eda6 100644
--- a/src/theory/theory_engine.cpp
+++ b/src/theory/theory_engine.cpp
@@ -1194,8 +1194,12 @@ Node TheoryEngine::getExplanation(TNode node) {
 
 theory::LemmaStatus TheoryEngine::lemma(TNode node, bool negated, bool removable) {
   if(Dump.isOn("t-lemmas")) {
+    Node n = node;
+    if (negated) {
+      n = node.negate();
+    }
     Dump("t-lemmas") << CommentCommand("theory lemma: expect valid")
-                     << QueryCommand(node.toExpr());
+                     << QueryCommand(n.toExpr());
   }
 
   // Share with other portfolio threads
diff --git a/src/util/bitvector.h b/src/util/bitvector.h
index 4cbcba50e..c9661c0c7 100644
--- a/src/util/bitvector.h
+++ b/src/util/bitvector.h
@@ -178,10 +178,23 @@ 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); 
+  }
+  
   /** 
    * Total division function that returns 0 when the denominator is 0.  
    */
   BitVector unsignedDivTotal (const BitVector& y) const {
+
     CheckArgument(d_size == y.d_size, y);
     if (y.d_value == 0) {
       return BitVector(d_size, 0u);
@@ -190,6 +203,7 @@ public:
     CheckArgument(y.d_value > 0, y);
     return BitVector(d_size, d_value.floorDivideQuotient(y.d_value)); 
   }
+  
   /** 
    * Total division function that returns 0 when the denominator is 0.  
    */
diff --git a/src/util/index.h b/src/util/index.h
index 4c03af5b0..252f7066b 100644
--- a/src/util/index.h
+++ b/src/util/index.h
@@ -21,6 +21,7 @@
 
 #include <stdint.h>
 #include <boost/static_assert.hpp>
+#include <limits>
 
 namespace CVC4 {
 
diff --git a/src/util/integer_cln_imp.h b/src/util/integer_cln_imp.h
index b5452ae00..81c0428cb 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 176604268..85d49f921 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/record.i b/src/util/record.i
index 2805d2fdf..368519f5b 100644
--- a/src/util/record.i
+++ b/src/util/record.i
@@ -19,6 +19,8 @@
 %ignore CVC4::Record::operator!=(const Record&) const;
 %rename(getField) CVC4::Record::operator[](size_t) const;
 
+#ifdef SWIGJAVA
+
 // These Object arrays are always of two elements, the first is a String and the second a
 // Type.  (On the C++ side, it is a std::pair<std::string, Type>.)
 %typemap(jni) std::pair<std::string, CVC4::Type> "jobjectArray";
@@ -33,8 +35,6 @@
       jenv->SetObjectArrayElement($result, 1, jenv->NewObject(clazz, methodid, reinterpret_cast<long>(new CVC4::Type($1.second)), true));
     };
 
-#ifdef SWIGJAVA
-
 // Instead of Record::begin() and end(), create an
 // iterator() method on the Java side that returns a Java-style
 // Iterator.
@@ -79,6 +79,15 @@
 // getNext() just allows C++ iterator access from Java-side next(), make it private
 %javamethodmodifiers CVC4::JavaIteratorAdapter<CVC4::Record>::getNext() "private";
 
+// map the types appropriately.  for records, the "payload" of the iterator is an Object[].
+// These Object arrays are always of two elements, the first is a String and the second a
+// Type.  (On the C++ side, it is a std::pair<std::string, SExpr>.)
+%typemap(jni) CVC4::Record::const_iterator::value_type = std::pair<std::string, CVC4::Type>;
+%typemap(jtype) CVC4::Record::const_iterator::value_type = std::pair<std::string, CVC4::Type>;
+%typemap(jstype) CVC4::Record::const_iterator::value_type = std::pair<std::string, CVC4::Type>;
+%typemap(javaout) CVC4::Record::const_iterator::value_type = std::pair<std::string, CVC4::Type>;
+%typemap(out) CVC4::Record::const_iterator::value_type = std::pair<std::string, CVC4::Type>;
+
 #endif /* SWIGJAVA */
 
 %include "util/record.h"
diff --git a/src/util/utility.h b/src/util/utility.h
index 5ce185b5b..089be478d 100644
--- a/src/util/utility.h
+++ b/src/util/utility.h
@@ -67,7 +67,6 @@ inline InputIterator find_if_unique(InputIterator first, InputIterator last, Pre
   return (match2 == last) ? match : last;
 }
 
-
 }/* CVC4 namespace */
 
 #endif /* __CVC4__UTILITY_H */