From: lianah <lianahady@gmail.com>
Date: Wed, 27 Mar 2013 02:14:24 +0000 (-0400)
Subject: added model generation for bv subtheories and bv-inequality solver option
X-Git-Tag: cvc5-1.0.0~7361^2~13
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=2bed73156740d7e93e303b02319c407a1d587109;p=cvc5.git

added model generation for bv subtheories and bv-inequality solver option
---

2bed73156740d7e93e303b02319c407a1d587109
diff --cc src/theory/bv/bitblaster.cpp
index cc589c5c3,4f5325e10..6da3b8efc
--- a/src/theory/bv/bitblaster.cpp
+++ b/src/theory/bv/bitblaster.cpp
@@@ -438,7 -421,7 +438,7 @@@ Node Bitblaster::getVarValue(TNode a) 
      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;
@@@ -453,7 -436,7 +453,7 @@@ void Bitblaster::collectModelInfo(Theor
    __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)) && hasValue(var))  {
 -    if (Theory::theoryOf(var) == theory::THEORY_BV || isSharedTerm(var)) {
++    if (Theory::theoryOf(var) == theory::THEORY_BV || isSharedTerm(var))  {
        Node const_value = getVarValue(var);
        Debug("bitvector-model") << "Bitblaster::collectModelInfo (assert (= "
                                  << var << " "
diff --cc src/theory/bv/bv_inequality_graph.cpp
index 3dfeba140,000000000..6d2ed0cf6
mode 100644,000000..100644
--- a/src/theory/bv/bv_inequality_graph.cpp
+++ b/src/theory/bv/bv_inequality_graph.cpp
@@@ -1,460 -1,0 +1,472 @@@
 +/*********************                                                        */
 +/*! \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::getNewLemmas(std::vector<Node>& new_lemmas) {
 +  for (unsigned i = d_diseqToSplitIndex; i < d_disequalitiesToSplit.size(); ++i)  {
 +    TNode diseq = d_disequalitiesToSplit[i];
 +    if (d_disequalitiesAlreadySplit.find(diseq) == d_disequalitiesAlreadySplit.end()) {
 +        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);
 +        new_lemmas.push_back(lemma);
 +        d_disequalitiesAlreadySplit.insert(diseq); 
 +    }
 +    d_diseqToSplitIndex = d_diseqToSplitIndex + 1; 
 +  }
 +}
 +
 +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(); 
 +  }
 +}
 +
 +void InequalityGraph::checkDisequalities() {
 +  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)) {
 +        // if the disequality is not satisified by the model 
 +        d_disequalitiesToSplit.push_back(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 --cc src/theory/bv/bv_inequality_graph.h
index b23ea7704,000000000..860302aa4
mode 100644,000000..100644
--- a/src/theory/bv/bv_inequality_graph.h
+++ b/src/theory/bv/bv_inequality_graph.h
@@@ -1,300 -1,0 +1,302 @@@
 +/*********************                                                        */
 +/*! \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> Model;
++  typedef context::CDHashMap<TermId, ModelValue> ModelValues;
 +
 +  struct QueueComparator {
-     const Model* d_model;
-     QueueComparator(const Model* model)
++    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; 
 +
-   Model  d_modelValues;
++  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;
 +  context::CDQueue<TNode> d_disequalitiesToSplit; 
 +  context::CDO<unsigned> d_diseqToSplitIndex; 
 +  TNodeSet d_lemmasAdded;
 +  TNodeSet d_disequalitiesAlreadySplit; 
 +  
 +  /** 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_disequalitiesToSplit(c),
 +      d_diseqToSplitIndex(c, 0),
 +      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) {}
 +  /** 
 +   * Get any new lemmas (resulting from disequalities splits) that need
 +   * to be added. 
 +   * 
 +   * @param new_lemmas 
 +   */
 +  void getNewLemmas(std::vector<Node>& new_lemmas);
 +  /** 
 +   * Check that the currently asserted disequalities that have not been split on
 +   * are still true in the current model. 
 +   */
 +  void checkDisequalities();
 +  /** 
 +   * 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; 
++  BitVector getValueInModel(TNode a) const;
++
++  void getAllValuesInModel(std::vector<Node>& assignments); 
 +}; 
 +
 +}
 +}
 +}
 +
 +#endif /* __CVC4__THEORY__BV__BV_INEQUALITY__GRAPH_H */
diff --cc src/theory/bv/bv_subtheory.h
index 4389dc50d,4dbba0797..ed90e0ebe
--- a/src/theory/bv/bv_subtheory.h
+++ b/src/theory/bv/bv_subtheory.h
@@@ -81,27 -76,14 +81,28 @@@ 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 --cc src/theory/bv/bv_subtheory_bitblast.cpp
index c7387daf8,f48a03975..9c4a5c5b6
--- a/src/theory/bv/bv_subtheory_bitblast.cpp
+++ b/src/theory/bv/bv_subtheory_bitblast.cpp
@@@ -62,14 -52,13 +62,15 @@@ void BitblastSolver::explain(TNode lite
    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);
        }
@@@ -85,10 -75,10 +86,11 @@@
      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(); 
++    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
diff --cc src/theory/bv/bv_subtheory_bitblast.h
index b05ac74cd,510006710..b6be84df5
--- a/src/theory/bv/bv_subtheory_bitblast.h
+++ b/src/theory/bv/bv_subtheory_bitblast.h
@@@ -46,11 -42,11 +46,12 @@@ public
    ~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 --cc src/theory/bv/bv_subtheory_core.cpp
index 112f73083,000000000..15720885d
mode 100644,000000..100644
--- a/src/theory/bv/bv_subtheory_core.cpp
+++ b/src/theory/bv/bv_subtheory_core.cpp
@@@ -1,322 -1,0 +1,417 @@@
 +/*********************                                                        */
 +/*! \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"
 +
 +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(c, this)),
 +    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);
 +      // 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<TNode>& explanation) {
 +  std::vector<Node> a_decomp;
 +  d_slicer->getBaseDecomposition(a, a_decomp, explanation);
 +  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
 +
 +  if (fact.getKind() == kind::EQUAL) {
 +    TNode a = fact[0];
 +    TNode b = fact[1];
 +
 +    d_slicer->processEquality(fact); 
 +    std::vector<TNode> explanation_a; 
 +    Node new_a = getBaseDecomposition(a, explanation_a);
 +    Node reason_a = mkAnd(explanation_a);
 +    d_reasons.insert(reason_a);
 +    
 +    std::vector<TNode> explanation_b; 
 +    Node new_b = getBaseDecomposition(b, explanation_b);
 +    Node reason_b = mkAnd(explanation_b);
 +    d_reasons.insert(reason_b);
 +
 +    std::vector<Node> explanation; 
 +    explanation.push_back(fact);
 +    explanation.insert(explanation.end(), explanation_a.begin(), explanation_a.end());
 +    explanation.insert(explanation.end(), explanation_b.begin(), explanation_b.end());
 +    
 +    Node reason = utils::mkAnd(explanation); 
 +    d_reasons.insert(reason);
 +    
 +    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, reason_a);
 +    if (!ok) return false; 
 +    ok = assertFactToEqualityEngine(b_eq_new_b, reason_a);
 +    if (!ok) return false; 
 +    // assert the individual equalities as well
 +    //    a_i == b_i
 +    if (new_a.getKind() == kind::BITVECTOR_CONCAT &&
 +        new_b.getKind() == kind::BITVECTOR_CONCAT) {
 +      Assert (new_a.getNumChildren() == new_b.getNumChildren()); 
 +      for (unsigned i = 0; i < new_a.getNumChildren(); ++i) {
 +        Node eq_i = nm->mkNode(kind::EQUAL, new_a[i], new_b[i]);
 +        // this reason is not very precise!!
 +        ok = assertFactToEqualityEngine(eq_i, reason);
 +        d_reasons.insert(eq_i); 
 +        if (!ok) return false;
 +      }
 +    }
 +    // merge the two terms in the slicer as well
 +    d_slicer->assertEquality(fact); 
 +  } else {
 +    // still need to register the terms
 +    d_slicer->processEquality(fact[0]);
 +    TNode a = fact[0][0];
 +    TNode b = fact[0][1];
 +    std::vector<TNode> explanation_a; 
 +    Node new_a = getBaseDecomposition(a, explanation_a);
 +    Node reason_a = explanation_a.empty()? mkTrue() : mkAnd(explanation_a);
 +    assertFactToEqualityEngine(utils::mkNode(kind::EQUAL, a, new_a), reason_a);
 +
 +    std::vector<TNode> explanation_b; 
 +    Node new_b = getBaseDecomposition(b, explanation_b);
 +    Node reason_b = explanation_b.empty()? mkTrue() : mkAnd(explanation_b);
 +    assertFactToEqualityEngine(utils::mkNode(kind::EQUAL, b, new_b), reason_b);
 +
 +    d_reasons.insert(reason_a);
 +    d_reasons.insert(reason_b); 
 +  }
 +  // finally assert the actual fact to the equality engine
 +  return assertFactToEqualityEngine(fact, fact);
 +}
 +
 +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)) {
 +      // ok = decomposeFact(fact);
 +      ok = assertFactToEqualityEngine(fact, fact); 
 +    } else {
 +      ok = assertFactToEqualityEngine(fact, fact); 
 +    }
 +    if (!ok)
 +      return false; 
 +  }
 +  
 +  // make sure to assert the new splits
 +  // std::vector<Node> new_splits;
 +  // d_slicer->getNewSplits(new_splits);
 +  // for (unsigned i = 0; i < new_splits.size(); ++i) {
 +  //   ok = assertFactToEqualityEngine(new_splits[i], utils::mkTrue());
 +  //   if (!ok)
 +  //     return false; 
 +  // }
++
++  // if we are sat and in full check attempt to construct a model
++  if (Theory::fullEffort(e) && isComplete()) {
++    buildModel();
++  }
++  
 +  return true;
 +}
 +
++void CoreSolver::buildModel() {
++  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()) {
++        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 (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());
++  Assert (d_modelValues.find(var) != d_modelValues.end()); 
++  return d_modelValues[d_equalityEngine.getRepresentative(var)]; 
 +}
 +
 +CoreSolver::Statistics::Statistics()
 +  : d_numCallstoCheck("theory::bv::CoreSolver::NumCallsToCheck", 0)
 +{
 +  StatisticsRegistry::registerStat(&d_numCallstoCheck);
 +}
 +CoreSolver::Statistics::~Statistics() {
 +  StatisticsRegistry::unregisterStat(&d_numCallstoCheck);
 +}
diff --cc src/theory/bv/bv_subtheory_core.h
index 4a9d84f79,000000000..d04dc164f
mode 100644,000000..100644
--- a/src/theory/bv/bv_subtheory_core.h
+++ b/src/theory/bv/bv_subtheory_core.h
@@@ -1,107 -1,0 +1,113 @@@
 +/*********************                                                        */
 +/*! \file bv_subtheory_eq.h
 + ** \verbatim
 + ** Original author: dejan
 + ** Major contributors: none
 + ** Minor contributors (to current version): lianah, mdeters
 + ** This file is part of the CVC4 prototype.
 + ** Copyright (c) 2009-2012  New York University and The University of Iowa
 + ** See the file COPYING in the top-level source directory for licensing
 + ** information.\endverbatim
 + **
 + ** \brief Algebraic solver.
 + **
 + ** Algebraic solver.
 + **/
 +
 +#pragma once
 +
 +#include "cvc4_private.h"
 +#include "theory/bv/bv_subtheory.h"
 +#include "context/cdhashmap.h"
 +#include "context/cdhashset.h"
 +
 +namespace CVC4 {
 +namespace theory {
 +namespace bv {
 +
 +class Slicer; 
 +class Base; 
 +/**
 + * Bitvector equality solver
 + */
 +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 {
 +    CoreSolver& d_solver;
 +
 +  public:
 +    NotifyClass(CoreSolver& solver): d_solver(solver) {}
 +    bool eqNotifyTriggerEquality(TNode equality, bool value);
 +    bool eqNotifyTriggerPredicate(TNode predicate, bool value);
 +    bool eqNotifyTriggerTermEquality(TheoryId tag, TNode t1, TNode t2, bool value);
 +    void eqNotifyConstantTermMerge(TNode t1, TNode t2);
 +    void eqNotifyNewClass(TNode t) { }
 +    void eqNotifyPreMerge(TNode t1, TNode t2) { }
 +    void eqNotifyPostMerge(TNode t1, TNode t2) { }
 +    void eqNotifyDisequal(TNode t1, TNode t2, TNode reason) { }
 +  };
 +
 +
 +  /** The notify class for d_equalityEngine */
 +  NotifyClass d_notify;
 +  
 +  /** Equality engine */
 +  eq::EqualityEngine d_equalityEngine;
 +
 +  /** Store a propagation to the bv solver */
 +  bool storePropagation(TNode literal);
 +  
 +  /** Store a conflict from merging two constants */
 +  void conflict(TNode a, TNode b);
 +
 +  Slicer* d_slicer;
 +  context::CDO<bool> d_isCoreTheory;
 +  /** To make sure we keep the explanations */
-   context::CDHashSet<Node, NodeHashFunction> d_reasons; 
++  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, std::vector<TNode>& explanation);
 +  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  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);
 +  }
 +  EqualityStatus getEqualityStatus(TNode a, TNode b) {
 +    if (d_equalityEngine.areEqual(a, b)) {
 +      // The terms are implied to be equal
 +      return EQUALITY_TRUE;
 +    }
 +    if (d_equalityEngine.areDisequal(a, b, false)) {
 +      // The terms are implied to be dis-equal
 +      return EQUALITY_FALSE;
 +    }
 +    return EQUALITY_UNKNOWN;
 +  }
 +  bool hasTerm(TNode node) const { return d_equalityEngine.hasTerm(node); }
 +  void addTermToEqualityEngine(TNode node) { d_equalityEngine.addTerm(node); }
 +};
 +
 +
 +}
 +}
 +}
diff --cc src/theory/bv/bv_subtheory_inequality.cpp
index 3d7339e88,000000000..27047f6af
mode 100644,000000..100644
--- a/src/theory/bv/bv_subtheory_inequality.cpp
+++ b/src/theory/bv/bv_subtheory_inequality.cpp
@@@ -1,164 -1,0 +1,181 @@@
 +/*********************                                                        */
 +/*! \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);
 +    } 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);
 +    } 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; 
 +  }
 +
 +  // make sure all the disequalities we didn't split on are still satisifed
 +  // and split on the ones that are not
 +  d_inequalityGraph.checkDisequalities();
 +
 +  // send out any lemmas
 +  std::vector<Node> lemmas;
 +  d_inequalityGraph.getNewLemmas(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 (false); 
 +}
 +
 +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());
++  Assert (d_inequalityGraph.hasValueInModel(var)); 
++  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 --cc src/theory/bv/bv_subtheory_inequality.h
index bcf94dc8b,000000000..b19ebb381
mode 100644,000000..100644
--- a/src/theory/bv/bv_subtheory_inequality.h
+++ b/src/theory/bv/bv_subtheory_inequality.h
@@@ -1,66 -1,0 +1,67 @@@
 +/*********************                                                        */
 +/*! \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::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_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) {}
++  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 --cc src/theory/bv/options
index 72db63c09,72db63c09..8e01c6572
--- a/src/theory/bv/options
+++ b/src/theory/bv/options
@@@ -14,4 -14,4 +14,6 @@@ option bitvectorShareLemmas --bitblast-
  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 
  endmodule
diff --cc src/theory/bv/theory_bv.cpp
index 43e290175,e28ef3ddf..8245fdbdc
--- a/src/theory/bv/theory_bv.cpp
+++ b/src/theory/bv/theory_bv.cpp
@@@ -47,28 -46,13 +47,30 @@@ TheoryBV::TheoryBV(context::Context* c
      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;
 +
-     SubtheorySolver* ineq_solver = new InequalitySolver(c, this); 
-     d_subtheories.push_back(ineq_solver);
-     d_subtheoryMap[SUB_INEQUALITY] = ineq_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():
@@@ -163,11 -132,17 +165,24 @@@ void TheoryBV::check(Effort e
  void TheoryBV::collectModelInfo( TheoryModel* m, bool fullModel ){
    Assert(!inConflict());
    //  Assert (fullModel); // can only query full model
 -  d_equalitySolver.collectModelInfo(m); 
 -  d_bitblastSolver.collectModelInfo(m); 
 -  
 +  for (unsigned i = 0; i < d_subtheories.size(); ++i) {
-     d_subtheories[i]->collectModelInfo(m); 
++    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;
  
diff --cc src/theory/bv/theory_bv_utils.h
index 98bc8041d,7d851d0fb..f8b9f010e
--- a/src/theory/bv/theory_bv_utils.h
+++ b/src/theory/bv/theory_bv_utils.h
@@@ -247,83 -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) {