2 files changed, 25 insertions, 39 deletions

diff --git a/src/theory/bv/theory_bv.cpp b/src/theory/bv/theory_bv.cpp
index 273b406e6..da2dd77f6 100644
--- a/src/theory/bv/theory_bv.cpp
+++ b/src/theory/bv/theory_bv.cpp
@@ -57,13 +57,13 @@ TheoryBV::Statistics::Statistics():
 {
   StatisticsRegistry::registerStat(&d_avgConflictSize);
   StatisticsRegistry::registerStat(&d_solveSubstitutions);
-  StatisticsRegistry::registerStat(&d_solveTimer); 
+  StatisticsRegistry::registerStat(&d_solveTimer);
 }
 
 TheoryBV::Statistics::~Statistics() {
   StatisticsRegistry::unregisterStat(&d_avgConflictSize);
   StatisticsRegistry::unregisterStat(&d_solveSubstitutions);
-  StatisticsRegistry::unregisterStat(&d_solveTimer); 
+  StatisticsRegistry::unregisterStat(&d_solveTimer);
 }
 
 void TheoryBV::preRegisterTerm(TNode node) {
@@ -75,7 +75,7 @@ void TheoryBV::preRegisterTerm(TNode node) {
   }
 
   d_bitblastSolver.preRegister(node);
-  d_equalitySolver.preRegister(node); 
+  d_equalitySolver.preRegister(node);
 }
 
 void TheoryBV::sendConflict() {
@@ -94,54 +94,40 @@ void TheoryBV::check(Effort e)
 {
   BVDebug("bitvector") << "TheoryBV::check(" << e << ")" << std::endl;
 
-  // if we are already in conflict just return the conflict 
+  // if we are already in conflict just return the conflict
   if (inConflict()) {
     sendConflict();
     return;
   }
-  
+
   // getting the new assertions
-  std::vector<TNode> new_assertions; 
+  std::vector<TNode> new_assertions;
   while (!done()) {
     Assertion assertion = get();
     TNode fact = assertion.assertion;
     new_assertions.push_back(fact);
-    BVDebug("bitvector-assertions") << "TheoryBV::check assertion " << fact << "\n"; 
+    BVDebug("bitvector-assertions") << "TheoryBV::check assertion " << fact << "\n";
   }
 
   if (!inConflict()) {
     // sending assertions to the equality solver first
     d_equalitySolver.addAssertions(new_assertions, e);
   }
-  
+
   if (!inConflict()) {
     // sending assertions to the bitblast solver
     d_bitblastSolver.addAssertions(new_assertions, e);
   }
-  
+
   if (inConflict()) {
     sendConflict();
   }
 }
 
+void TheoryBV::collectModelInfo( TheoryModel* m ){
 
-Node TheoryBV::getValue(TNode n) {
-  //NodeManager* nodeManager = NodeManager::currentNM();
-
-  switch(n.getKind()) {
-
-  case kind::VARIABLE:
-    Unhandled(kind::VARIABLE);
-
-  case kind::EQUAL: // 2 args
-    Unhandled(kind::VARIABLE);
-
-  default:
-    Unhandled(n.getKind());
-  }
 }
 
-
 void TheoryBV::propagate(Effort e) {
   BVDebug("bitvector") << indent() << "TheoryBV::propagate()" << std::endl;
 
@@ -166,14 +152,14 @@ void TheoryBV::propagate(Effort e) {
 Theory::PPAssertStatus TheoryBV::ppAssert(TNode in, SubstitutionMap& outSubstitutions) {
   switch(in.getKind()) {
   case kind::EQUAL:
-    
+
     if (in[0].getMetaKind() == kind::metakind::VARIABLE && !in[1].hasSubterm(in[0])) {
-      ++(d_statistics.d_solveSubstitutions); 
+      ++(d_statistics.d_solveSubstitutions);
       outSubstitutions.addSubstitution(in[0], in[1]);
       return PP_ASSERT_STATUS_SOLVED;
     }
     if (in[1].getMetaKind() == kind::metakind::VARIABLE && !in[0].hasSubterm(in[1])) {
-      ++(d_statistics.d_solveSubstitutions); 
+      ++(d_statistics.d_solveSubstitutions);
       outSubstitutions.addSubstitution(in[1], in[0]);
       return PP_ASSERT_STATUS_SOLVED;
     }
@@ -243,14 +229,14 @@ bool TheoryBV::storePropagation(TNode literal, SubTheory subtheory)
 
 
 void TheoryBV::explain(TNode literal, std::vector<TNode>& assumptions) {
-  // Ask the appropriate subtheory for the explanation 
+  // Ask the appropriate subtheory for the explanation
   if (propagatedBy(literal, SUB_EQUALITY)) {
     BVDebug("bitvector::explain") << "TheoryBV::explain(" << literal << "): EQUALITY" << std::endl;
-    d_equalitySolver.explain(literal, assumptions); 
+    d_equalitySolver.explain(literal, assumptions);
   } else {
     Assert(propagatedBy(literal, SUB_BITBLAST));
-    BVDebug("bitvector::explain") << "TheoryBV::explain(" << literal << ") : BITBLASTER" << std::endl;    
-    d_bitblastSolver.explain(literal, assumptions); 
+    BVDebug("bitvector::explain") << "TheoryBV::explain(" << literal << ") : BITBLASTER" << std::endl;
+    d_bitblastSolver.explain(literal, assumptions);
   }
 }
 
@@ -263,7 +249,7 @@ Node TheoryBV::explain(TNode node) {
   explain(node, assumptions);
   // this means that it is something true at level 0
   if (assumptions.size() == 0) {
-    return utils::mkTrue(); 
+    return utils::mkTrue();
   }
   // return the explanation
   Node explanation = mkAnd(assumptions);
@@ -274,9 +260,9 @@ Node TheoryBV::explain(TNode node) {
 
 void TheoryBV::addSharedTerm(TNode t) {
   Debug("bitvector::sharing") << indent() << "TheoryBV::addSharedTerm(" << t << ")" << std::endl;
-  d_sharedTermsSet.insert(t); 
+  d_sharedTermsSet.insert(t);
   if (!Options::current()->bitvectorEagerBitblast && d_useEqualityEngine) {
-    d_equalitySolver.addSharedTerm(t); 
+    d_equalitySolver.addSharedTerm(t);
   }
 }
 
diff --git a/src/theory/bv/theory_bv.h b/src/theory/bv/theory_bv.h
index 761c11e3d..611927b2b 100644
--- a/src/theory/bv/theory_bv.h
+++ b/src/theory/bv/theory_bv.h
@@ -57,10 +57,10 @@ public:
   void check(Effort e);
 
   void propagate(Effort e);
-  
+
   Node explain(TNode n);
 
-  Node getValue(TNode n);
+  void collectModelInfo( TheoryModel* m );
 
   std::string identify() const { return std::string("TheoryBV"); }
 
@@ -124,7 +124,7 @@ private:
   }
 
   void setConflict(Node conflict = Node::null()) {
-    d_conflict = true; 
+    d_conflict = true;
     d_conflictNode = conflict;
   }
 
@@ -136,8 +136,8 @@ private:
 
   friend class Bitblaster;
   friend class BitblastSolver;
-  friend class EqualitySolver; 
-  
+  friend class EqualitySolver;
+
 };/* class TheoryBV */
 
 }/* CVC4::theory::bv namespace */