2 files changed, 3 insertions, 100 deletions
diff --git a/src/theory/booleans/theory_bool.cpp b/src/theory/booleans/theory_bool.cpp
index 520adc228..f096987db 100644
--- a/src/theory/booleans/theory_bool.cpp
+++ b/src/theory/booleans/theory_bool.cpp
@@ -32,106 +32,8 @@ namespace CVC4 {
 namespace theory {
 namespace booleans {
 
-Node TheoryBool::getValue(TNode n) {
-  NodeManager* nodeManager = NodeManager::currentNM();
+void TheoryBool::collectModelInfo( TheoryModel* m ){
 
-  switch(n.getKind()) {
-  case kind::VARIABLE:
-    // case for Boolean vars is implemented in TheoryEngine (since it
-    // appeals to the PropEngine to get the value)
-    Unreachable();
-
-  case kind::EQUAL: // 2 args
-    // should be handled by IFF
-    Unreachable();
-
-  case kind::NOT: { // 1 arg
-    Node v = d_valuation.getValue(n[0]);
-    return v.isNull() ? Node::null() : nodeManager->mkConst(! v.getConst<bool>());
-  }
-
-  case kind::AND: { // 2+ args
-    bool foundNull = false;
-    for(TNode::iterator i = n.begin(),
-            iend = n.end();
-          i != iend;
-          ++i) {
-      Node v = d_valuation.getValue(*i);
-      if(v.isNull()) {
-        foundNull = true;
-      } else if(! v.getConst<bool>()) {
-        return nodeManager->mkConst(false);
-      }
-    }
-    return foundNull ? Node::null() : nodeManager->mkConst(true);
-  }
-
-  case kind::IFF: { // 2 args
-    Node v0 = d_valuation.getValue(n[0]);
-    Node v1 = d_valuation.getValue(n[1]);
-    if(v0.isNull() || v1.isNull()) {
-      return Node::null();
-    }
-    return nodeManager->mkConst( v0.getConst<bool>() == v1.getConst<bool>() );
-  }
-
-  case kind::IMPLIES: { // 2 args
-    Node v0 = d_valuation.getValue(n[0]);
-    Node v1 = d_valuation.getValue(n[1]);
-    if(v0.isNull() && v1.isNull()) {
-      return Node::null();
-    }
-    bool value = false;
-    if(! v0.isNull()) {
-      value = value || (! v0.getConst<bool>());
-    }
-    if(! v1.isNull()) {
-      value = value || v1.getConst<bool>();
-    }
-    return nodeManager->mkConst(value);
-  }
-
-  case kind::OR: { // 2+ args
-    bool foundNull = false;
-    for(TNode::iterator i = n.begin(),
-            iend = n.end();
-          i != iend;
-          ++i) {
-      Node v = d_valuation.getValue(*i);
-      if(v.isNull()) {
-        foundNull = true;
-      } else if(v.getConst<bool>()) {
-        return nodeManager->mkConst(true);
-      }
-    }
-    return foundNull ? Node::null() : nodeManager->mkConst(false);
-  }
-
-  case kind::XOR: { // 2 args
-    Node v0 = d_valuation.getValue(n[0]);
-    Node v1 = d_valuation.getValue(n[1]);
-    if(v0.isNull() || v1.isNull()) {
-      return Node::null();
-    }
-    return nodeManager->mkConst( v0.getConst<bool>() != v1.getConst<bool>() );
-  }
-
-  case kind::ITE: { // 3 args
-    // all ITEs should be gone except (bool,bool,bool) ones
-    Assert( n[1].getType() == nodeManager->booleanType() &&
-            n[2].getType() == nodeManager->booleanType() );
-    Node v0 = d_valuation.getValue(n[0]);
-    Node v1 = d_valuation.getValue(n[1]);
-    Node v2 = d_valuation.getValue(n[2]);
-    if(v0.isNull()) {
-      return v1 == v2 ? v1 : Node::null();
-    }
-    return nodeManager->mkConst( v0.getConst<bool>() ? v1.getConst<bool>() : v2.getConst<bool>() );
-  }
-
-  default:
-    Unhandled(n.getKind());
-  }
 }
 
 Theory::PPAssertStatus TheoryBool::ppAssert(TNode in, SubstitutionMap& outSubstitutions) {
diff --git a/src/theory/booleans/theory_bool.h b/src/theory/booleans/theory_bool.h
index 40783a6ce..827b0ff57 100644
--- a/src/theory/booleans/theory_bool.h
+++ b/src/theory/booleans/theory_bool.h
@@ -23,6 +23,7 @@
 
 #include "theory/theory.h"
 #include "context/context.h"
+#include "theory/model.h"
 
 namespace CVC4 {
 namespace theory {
@@ -34,7 +35,7 @@ public:
     Theory(THEORY_BOOL, c, u, out, valuation, logicInfo, qe) {
   }
 
-  Node getValue(TNode n);
+  void collectModelInfo( TheoryModel* m );
 
   PPAssertStatus ppAssert(TNode in, SubstitutionMap& outSubstitutions);