2 files changed, 16 insertions, 16 deletions

diff --git a/src/theory/booleans/theory_bool.cpp b/src/theory/booleans/theory_bool.cpp
index 44f5d60a6..878b18478 100644
--- a/src/theory/booleans/theory_bool.cpp
+++ b/src/theory/booleans/theory_bool.cpp
@@ -24,7 +24,7 @@ namespace CVC4 {
 namespace theory {
 namespace booleans {
 
-Node TheoryBool::getValue(TNode n, Valuation* valuation) {
+Node TheoryBool::getValue(TNode n) {
   NodeManager* nodeManager = NodeManager::currentNM();
 
   switch(n.getKind()) {
@@ -38,14 +38,14 @@ Node TheoryBool::getValue(TNode n, Valuation* valuation) {
     Unreachable();
 
   case kind::NOT: // 1 arg
-    return nodeManager->mkConst(! valuation->getValue(n[0]).getConst<bool>());
+    return nodeManager->mkConst(! d_valuation.getValue(n[0]).getConst<bool>());
 
   case kind::AND: { // 2+ args
     for(TNode::iterator i = n.begin(),
             iend = n.end();
           i != iend;
           ++i) {
-      if(! valuation->getValue(*i).getConst<bool>()) {
+      if(! d_valuation.getValue(*i).getConst<bool>()) {
         return nodeManager->mkConst(false);
       }
     }
@@ -53,19 +53,19 @@ Node TheoryBool::getValue(TNode n, Valuation* valuation) {
   }
 
   case kind::IFF: // 2 args
-    return nodeManager->mkConst( valuation->getValue(n[0]).getConst<bool>() ==
-                                 valuation->getValue(n[1]).getConst<bool>() );
+    return nodeManager->mkConst( d_valuation.getValue(n[0]).getConst<bool>() ==
+                                 d_valuation.getValue(n[1]).getConst<bool>() );
 
   case kind::IMPLIES: // 2 args
-    return nodeManager->mkConst( (! valuation->getValue(n[0]).getConst<bool>()) ||
-                                 valuation->getValue(n[1]).getConst<bool>() );
+    return nodeManager->mkConst( (! d_valuation.getValue(n[0]).getConst<bool>()) ||
+                                 d_valuation.getValue(n[1]).getConst<bool>() );
 
   case kind::OR: { // 2+ args
     for(TNode::iterator i = n.begin(),
             iend = n.end();
           i != iend;
           ++i) {
-      if(valuation->getValue(*i).getConst<bool>()) {
+      if(d_valuation.getValue(*i).getConst<bool>()) {
         return nodeManager->mkConst(true);
       }
     }
@@ -73,16 +73,16 @@ Node TheoryBool::getValue(TNode n, Valuation* valuation) {
   }
 
   case kind::XOR: // 2 args
-    return nodeManager->mkConst( valuation->getValue(n[0]).getConst<bool>() !=
-                                 valuation->getValue(n[1]).getConst<bool>() );
+    return nodeManager->mkConst( d_valuation.getValue(n[0]).getConst<bool>() !=
+                                 d_valuation.getValue(n[1]).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() );
-    return nodeManager->mkConst( valuation->getValue(n[0]).getConst<bool>() ?
-                                 valuation->getValue(n[1]).getConst<bool>() :
-                                 valuation->getValue(n[2]).getConst<bool>() );
+    return nodeManager->mkConst( d_valuation.getValue(n[0]).getConst<bool>() ?
+                                 d_valuation.getValue(n[1]).getConst<bool>() :
+                                 d_valuation.getValue(n[2]).getConst<bool>() );
 
   default:
     Unhandled(n.getKind());
diff --git a/src/theory/booleans/theory_bool.h b/src/theory/booleans/theory_bool.h
index 4120159df..dfcdd22b8 100644
--- a/src/theory/booleans/theory_bool.h
+++ b/src/theory/booleans/theory_bool.h
@@ -30,8 +30,8 @@ namespace booleans {
 
 class TheoryBool : public Theory {
 public:
-  TheoryBool(context::Context* c, OutputChannel& out) :
-    Theory(THEORY_BOOL, c, out) {
+  TheoryBool(context::Context* c, OutputChannel& out, Valuation valuation) :
+    Theory(THEORY_BOOL, c, out, valuation) {
   }
 
   void preRegisterTerm(TNode n) {
@@ -43,7 +43,7 @@ public:
     Debug("bool") << "bool: end preRegisterTerm(" << n << ")" << std::endl;
   }
 
-  Node getValue(TNode n, Valuation* valuation);
+  Node getValue(TNode n);
 
   std::string identify() const { return std::string("TheoryBool"); }
 };