Merge from theory-break-dependences branch to break Theory and TheoryEngine dependences; now, if you touch theory_engine.h, only a few things in theory need be recompiled (TheoryEngine, SharedTermManager, .... but no theory implementations), along with the PropEngine and SmtEngine. If you touch a specific theory's .h file, only that theory must be recompiled (along with the TheoryEngine, since it uses traits, and SmtEngine, since it tells the TheoryEngine which theory implementations to use).

1 files changed, 14 insertions, 14 deletions

diff --git a/src/theory/booleans/theory_bool.cpp b/src/theory/booleans/theory_bool.cpp
index f8071d45d..44f5d60a6 100644
--- a/src/theory/booleans/theory_bool.cpp
+++ b/src/theory/booleans/theory_bool.cpp
@@ -18,13 +18,13 @@
 
 #include "theory/theory.h"
 #include "theory/booleans/theory_bool.h"
-#include "theory/theory_engine.h"
+#include "theory/valuation.h"
 
 namespace CVC4 {
 namespace theory {
 namespace booleans {
 
-Node TheoryBool::getValue(TNode n, TheoryEngine* engine) {
+Node TheoryBool::getValue(TNode n, Valuation* valuation) {
   NodeManager* nodeManager = NodeManager::currentNM();
 
   switch(n.getKind()) {
@@ -38,14 +38,14 @@ Node TheoryBool::getValue(TNode n, TheoryEngine* engine) {
     Unreachable();
 
   case kind::NOT: // 1 arg
-    return nodeManager->mkConst(! engine->getValue(n[0]).getConst<bool>());
+    return nodeManager->mkConst(! valuation->getValue(n[0]).getConst<bool>());
 
   case kind::AND: { // 2+ args
     for(TNode::iterator i = n.begin(),
             iend = n.end();
           i != iend;
           ++i) {
-      if(! engine->getValue(*i).getConst<bool>()) {
+      if(! valuation->getValue(*i).getConst<bool>()) {
         return nodeManager->mkConst(false);
       }
     }
@@ -53,19 +53,19 @@ Node TheoryBool::getValue(TNode n, TheoryEngine* engine) {
   }
 
   case kind::IFF: // 2 args
-    return nodeManager->mkConst( engine->getValue(n[0]).getConst<bool>() ==
-                                 engine->getValue(n[1]).getConst<bool>() );
+    return nodeManager->mkConst( valuation->getValue(n[0]).getConst<bool>() ==
+                                 valuation->getValue(n[1]).getConst<bool>() );
 
   case kind::IMPLIES: // 2 args
-    return nodeManager->mkConst( (! engine->getValue(n[0]).getConst<bool>()) ||
-                                 engine->getValue(n[1]).getConst<bool>() );
+    return nodeManager->mkConst( (! valuation->getValue(n[0]).getConst<bool>()) ||
+                                 valuation->getValue(n[1]).getConst<bool>() );
 
   case kind::OR: { // 2+ args
     for(TNode::iterator i = n.begin(),
             iend = n.end();
           i != iend;
           ++i) {
-      if(engine->getValue(*i).getConst<bool>()) {
+      if(valuation->getValue(*i).getConst<bool>()) {
         return nodeManager->mkConst(true);
       }
     }
@@ -73,16 +73,16 @@ Node TheoryBool::getValue(TNode n, TheoryEngine* engine) {
   }
 
   case kind::XOR: // 2 args
-    return nodeManager->mkConst( engine->getValue(n[0]).getConst<bool>() !=
-                                 engine->getValue(n[1]).getConst<bool>() );
+    return nodeManager->mkConst( valuation->getValue(n[0]).getConst<bool>() !=
+                                 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( engine->getValue(n[0]).getConst<bool>() ?
-                                 engine->getValue(n[1]).getConst<bool>() :
-                                 engine->getValue(n[2]).getConst<bool>() );
+    return nodeManager->mkConst( valuation->getValue(n[0]).getConst<bool>() ?
+                                 valuation->getValue(n[1]).getConst<bool>() :
+                                 valuation->getValue(n[2]).getConst<bool>() );
 
   default:
     Unhandled(n.getKind());