From edf6aaa87da179948e6b233d16fa37d2aea58bbb Mon Sep 17 00:00:00 2001
From: Morgan Deters <mdeters@gmail.com>
Date: Sat, 26 Feb 2011 21:24:18 +0000
Subject: 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).

---
 src/theory/builtin/theory_builtin.cpp | 10 +++++-----
 src/theory/builtin/theory_builtin.h   |  2 +-
 2 files changed, 6 insertions(+), 6 deletions(-)

(limited to 'src/theory/builtin')

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 */
 
-- 
cgit v1.2.3