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).

2 files changed, 6 insertions, 6 deletions

diff --git a/src/theory/builtin/theory_builtin.cpp b/src/theory/builtin/theory_builtin.cpp
index 489c97e67..a276fa0ce 100644
--- a/src/theory/builtin/theory_builtin.cpp
+++ b/src/theory/builtin/theory_builtin.cpp
@@ -17,7 +17,7 @@
  **/
 
 #include "theory/builtin/theory_builtin.h"
-#include "theory/theory_engine.h"
+#include "theory/valuation.h"
 #include "expr/kind.h"
 
 using namespace std;
@@ -26,7 +26,7 @@ namespace CVC4 {
 namespace theory {
 namespace builtin {
 
-Node TheoryBuiltin::getValue(TNode n, TheoryEngine* engine) {
+Node TheoryBuiltin::getValue(TNode n, Valuation* valuation) {
   switch(n.getKind()) {
 
   case kind::VARIABLE:
@@ -39,7 +39,7 @@ Node TheoryBuiltin::getValue(TNode n, TheoryEngine* engine) {
     Assert(n[0].getKind() == kind::TUPLE &&
            n[1].getKind() == kind::TUPLE);
     return NodeManager::currentNM()->
-      mkConst( getValue(n[0], engine) == getValue(n[1], engine) );
+      mkConst( getValue(n[0], valuation) == getValue(n[1], valuation) );
   }
 
   case kind::TUPLE: { // 2+ args
@@ -48,14 +48,14 @@ Node TheoryBuiltin::getValue(TNode n, TheoryEngine* engine) {
           iend = n.end();
         i != iend;
         ++i) {
-      nb << engine->getValue(*i);
+      nb << valuation->getValue(*i);
     }
     return Node(nb);
   }
 
   default:
     // all other "builtins" should have been rewritten away or handled
-    // by theory engine, or handled elsewhere.
+    // by the valuation, or handled elsewhere.
     Unhandled(n.getKind());
   }
 }
diff --git a/src/theory/builtin/theory_builtin.h b/src/theory/builtin/theory_builtin.h
index baa1493b6..5b9810326 100644
--- a/src/theory/builtin/theory_builtin.h
+++ b/src/theory/builtin/theory_builtin.h
@@ -31,7 +31,7 @@ class TheoryBuiltin : public Theory {
 public:
   TheoryBuiltin(context::Context* c, OutputChannel& out) :
     Theory(THEORY_BUILTIN, c, out) {}
-  Node getValue(TNode n, TheoryEngine* engine);
+  Node getValue(TNode n, Valuation* valuation);
   std::string identify() const { return std::string("TheoryBuiltin"); }
 };/* class TheoryBuiltin */