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

19 files changed, 196 insertions, 98 deletions

diff --git a/src/theory/Makefile.am b/src/theory/Makefile.am
index acf0ed5ee..142aef004 100644
--- a/src/theory/Makefile.am
+++ b/src/theory/Makefile.am
@@ -21,7 +21,10 @@ libtheory_la_SOURCES = \
 	shared_data.cpp \
 	rewriter.h \
 	rewriter_attributes.h \
-	rewriter.cpp 
+	rewriter.cpp \
+	valuation.h \
+	valuation.cpp
+
 nodist_libtheory_la_SOURCES = \
 	rewriter_tables.h \
 	theory_traits.h
@@ -47,7 +50,7 @@ BUILT_SOURCES = \
 
 CLEANFILES = \
 	rewriter_tables.h \
-	theory_traits.h 
+	theory_traits.h
 
 include @top_srcdir@/src/theory/Makefile.subdirs
 
@@ -66,4 +69,3 @@ theory_traits.h: theory_traits_template.h mktheorytraits @top_builddir@/src/theo
 		$< \
 		`cat @top_builddir@/src/theory/.subdirs` \
 	> $@) || (rm -f $@ && exit 1)
-	
\ No newline at end of file
diff --git a/src/theory/arith/theory_arith.cpp b/src/theory/arith/theory_arith.cpp
index 6084e3463..2100e0b38 100644
--- a/src/theory/arith/theory_arith.cpp
+++ b/src/theory/arith/theory_arith.cpp
@@ -22,7 +22,7 @@
 #include "expr/metakind.h"
 #include "expr/node_builder.h"
 
-#include "theory/theory_engine.h"
+#include "theory/valuation.h"
 
 #include "util/rational.h"
 #include "util/integer.h"
@@ -567,7 +567,7 @@ void TheoryArith::propagate(Effort e) {
   // }
 }
 
-Node TheoryArith::getValue(TNode n, TheoryEngine* engine) {
+Node TheoryArith::getValue(TNode n, Valuation* valuation) {
   NodeManager* nodeManager = NodeManager::currentNM();
 
   switch(n.getKind()) {
@@ -578,7 +578,7 @@ Node TheoryArith::getValue(TNode n, TheoryEngine* engine) {
       Node eq = d_removedRows.find(var)->second;
       Assert(n == eq[0]);
       Node rhs = eq[1];
-      return getValue(rhs, engine);
+      return getValue(rhs, valuation);
     }
 
     DeltaRational drat = d_partialModel.getAssignment(var);
@@ -591,7 +591,7 @@ Node TheoryArith::getValue(TNode n, TheoryEngine* engine) {
 
   case kind::EQUAL: // 2 args
     return nodeManager->
-      mkConst( engine->getValue(n[0]) == engine->getValue(n[1]) );
+      mkConst( valuation->getValue(n[0]) == valuation->getValue(n[1]) );
 
   case kind::PLUS: { // 2+ args
     Rational value = d_constants.d_ZERO;
@@ -599,7 +599,7 @@ Node TheoryArith::getValue(TNode n, TheoryEngine* engine) {
             iend = n.end();
           i != iend;
           ++i) {
-      value += engine->getValue(*i).getConst<Rational>();
+      value += valuation->getValue(*i).getConst<Rational>();
     }
     return nodeManager->mkConst(value);
   }
@@ -610,7 +610,7 @@ Node TheoryArith::getValue(TNode n, TheoryEngine* engine) {
             iend = n.end();
           i != iend;
           ++i) {
-      value *= engine->getValue(*i).getConst<Rational>();
+      value *= valuation->getValue(*i).getConst<Rational>();
     }
     return nodeManager->mkConst(value);
   }
@@ -624,24 +624,24 @@ Node TheoryArith::getValue(TNode n, TheoryEngine* engine) {
     Unreachable();
 
   case kind::DIVISION: // 2 args
-    return nodeManager->mkConst( engine->getValue(n[0]).getConst<Rational>() /
-                                 engine->getValue(n[1]).getConst<Rational>() );
+    return nodeManager->mkConst( valuation->getValue(n[0]).getConst<Rational>() /
+                                 valuation->getValue(n[1]).getConst<Rational>() );
 
   case kind::LT: // 2 args
-    return nodeManager->mkConst( engine->getValue(n[0]).getConst<Rational>() <
-                                 engine->getValue(n[1]).getConst<Rational>() );
+    return nodeManager->mkConst( valuation->getValue(n[0]).getConst<Rational>() <
+                                 valuation->getValue(n[1]).getConst<Rational>() );
 
   case kind::LEQ: // 2 args
-    return nodeManager->mkConst( engine->getValue(n[0]).getConst<Rational>() <=
-                                 engine->getValue(n[1]).getConst<Rational>() );
+    return nodeManager->mkConst( valuation->getValue(n[0]).getConst<Rational>() <=
+                                 valuation->getValue(n[1]).getConst<Rational>() );
 
   case kind::GT: // 2 args
-    return nodeManager->mkConst( engine->getValue(n[0]).getConst<Rational>() >
-                                 engine->getValue(n[1]).getConst<Rational>() );
+    return nodeManager->mkConst( valuation->getValue(n[0]).getConst<Rational>() >
+                                 valuation->getValue(n[1]).getConst<Rational>() );
 
   case kind::GEQ: // 2 args
-    return nodeManager->mkConst( engine->getValue(n[0]).getConst<Rational>() >=
-                                 engine->getValue(n[1]).getConst<Rational>() );
+    return nodeManager->mkConst( valuation->getValue(n[0]).getConst<Rational>() >=
+                                 valuation->getValue(n[1]).getConst<Rational>() );
 
   default:
     Unhandled(n.getKind());
diff --git a/src/theory/arith/theory_arith.h b/src/theory/arith/theory_arith.h
index 60d24708c..e29054c16 100644
--- a/src/theory/arith/theory_arith.h
+++ b/src/theory/arith/theory_arith.h
@@ -152,7 +152,7 @@ public:
 
   void notifyEq(TNode lhs, TNode rhs);
 
-  Node getValue(TNode n, TheoryEngine* engine);
+  Node getValue(TNode n, Valuation* valuation);
 
   void shutdown(){ }
 
diff --git a/src/theory/arrays/theory_arrays.cpp b/src/theory/arrays/theory_arrays.cpp
index ad7550a6c..d45320266 100644
--- a/src/theory/arrays/theory_arrays.cpp
+++ b/src/theory/arrays/theory_arrays.cpp
@@ -18,7 +18,7 @@
 
 
 #include "theory/arrays/theory_arrays.h"
-#include "theory/theory_engine.h"
+#include "theory/valuation.h"
 #include "expr/kind.h"
 
 
@@ -60,7 +60,7 @@ void TheoryArrays::check(Effort e) {
   Debug("arrays") << "TheoryArrays::check(): done" << endl;
 }
 
-Node TheoryArrays::getValue(TNode n, TheoryEngine* engine) {
+Node TheoryArrays::getValue(TNode n, Valuation* valuation) {
   NodeManager* nodeManager = NodeManager::currentNM();
 
   switch(n.getKind()) {
@@ -70,7 +70,7 @@ Node TheoryArrays::getValue(TNode n, TheoryEngine* engine) {
 
   case kind::EQUAL: // 2 args
     return nodeManager->
-      mkConst( engine->getValue(n[0]) == engine->getValue(n[1]) );
+      mkConst( valuation->getValue(n[0]) == valuation->getValue(n[1]) );
 
   default:
     Unhandled(n.getKind());
diff --git a/src/theory/arrays/theory_arrays.h b/src/theory/arrays/theory_arrays.h
index d3472f952..5a63fd26c 100644
--- a/src/theory/arrays/theory_arrays.h
+++ b/src/theory/arrays/theory_arrays.h
@@ -43,7 +43,7 @@ public:
   void check(Effort e);
   void propagate(Effort e) { }
   void explain(TNode n) { }
-  Node getValue(TNode n, TheoryEngine* engine);
+  Node getValue(TNode n, Valuation* valuation);
   void shutdown() { }
   std::string identify() const { return std::string("TheoryArrays"); }
 };/* class TheoryArrays */
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());
diff --git a/src/theory/booleans/theory_bool.h b/src/theory/booleans/theory_bool.h
index 5d91842d7..4120159df 100644
--- a/src/theory/booleans/theory_bool.h
+++ b/src/theory/booleans/theory_bool.h
@@ -43,7 +43,7 @@ public:
     Debug("bool") << "bool: end preRegisterTerm(" << n << ")" << std::endl;
   }
 
-  Node getValue(TNode n, TheoryEngine* engine);
+  Node getValue(TNode n, Valuation* valuation);
 
   std::string identify() const { return std::string("TheoryBool"); }
 };
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 */
 
diff --git a/src/theory/bv/theory_bv.cpp b/src/theory/bv/theory_bv.cpp
index 0356e5f27..b600bc8f1 100644
--- a/src/theory/bv/theory_bv.cpp
+++ b/src/theory/bv/theory_bv.cpp
@@ -20,7 +20,7 @@
 #include "theory/bv/theory_bv.h"
 #include "theory/bv/theory_bv_utils.h"
 
-#include "theory/theory_engine.h"
+#include "theory/valuation.h"
 
 using namespace CVC4;
 using namespace CVC4::theory;
@@ -115,7 +115,7 @@ bool TheoryBV::triggerEquality(size_t triggerId) {
   return true;
 }
 
-Node TheoryBV::getValue(TNode n, TheoryEngine* engine) {
+Node TheoryBV::getValue(TNode n, Valuation* valuation) {
   NodeManager* nodeManager = NodeManager::currentNM();
 
   switch(n.getKind()) {
@@ -125,7 +125,7 @@ Node TheoryBV::getValue(TNode n, TheoryEngine* engine) {
 
   case kind::EQUAL: // 2 args
     return nodeManager->
-      mkConst( engine->getValue(n[0]) == engine->getValue(n[1]) );
+      mkConst( valuation->getValue(n[0]) == valuation->getValue(n[1]) );
 
   default:
     Unhandled(n.getKind());
diff --git a/src/theory/bv/theory_bv.h b/src/theory/bv/theory_bv.h
index ed23bf53f..ede98004f 100644
--- a/src/theory/bv/theory_bv.h
+++ b/src/theory/bv/theory_bv.h
@@ -88,7 +88,7 @@ public:
 
   void explain(TNode n) { }
 
-  Node getValue(TNode n, TheoryEngine* engine);
+  Node getValue(TNode n, Valuation* valuation);
 
   std::string identify() const { return std::string("TheoryBV"); }
 };/* class TheoryBV */
diff --git a/src/theory/theory.h b/src/theory/theory.h
index a4682710f..b4c3a897b 100644
--- a/src/theory/theory.h
+++ b/src/theory/theory.h
@@ -36,6 +36,10 @@ namespace CVC4 {
 class TheoryEngine;
 
 namespace theory {
+  class Valuation;
+}/* CVC4::theory namespace */
+
+namespace theory {
 
 /**
  * Base class for T-solvers.  Abstract DPLL(T).
@@ -322,7 +326,8 @@ public:
    * if you *know* that you are responsible handle the Node you're
    * asking for; other theories can use your types, so be careful
    * here!  To be safe, it's best to delegate back to the
-   * TheoryEngine.
+   * TheoryEngine (by way of the Valuation proxy object, which avoids
+   * direct dependence on TheoryEngine).
    *
    * Usually, you need to handle at least the two cases of EQUAL and
    * VARIABLE---EQUAL in case a value of yours is on the LHS of an
@@ -337,7 +342,7 @@ public:
    * and suspect this situation is the case, return Node::null()
    * rather than throwing an exception.
    */
-  virtual Node getValue(TNode n, TheoryEngine* engine) = 0;
+  virtual Node getValue(TNode n, Valuation* valuation) = 0;
 
   /**
    * The theory should only add (via .operator<< or .append()) to the
diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp
index 25fe29c67..97cb8f471 100644
--- a/src/theory/theory_engine.cpp
+++ b/src/theory/theory_engine.cpp
@@ -134,6 +134,7 @@ TheoryEngine::TheoryEngine(context::Context* ctxt, const Options& opts) :
   d_theoryRegistration(opts.theoryRegistration),
   d_hasShutDown(false),
   d_incomplete(ctxt, false),
+  d_valuation(this),
   d_statistics() {
 
   Rewriter::init();
@@ -226,6 +227,49 @@ Node TheoryEngine::preprocess(TNode node) {
   return preprocessed;
 }
 
+/**
+ * Check all (currently-active) theories for conflicts.
+ * @param effort the effort level to use
+ */
+bool TheoryEngine::check(theory::Theory::Effort effort) {
+  d_theoryOut.d_conflictNode = Node::null();
+  d_theoryOut.d_propagatedLiterals.clear();
+
+#ifdef CVC4_FOR_EACH_THEORY_STATEMENT
+#undef CVC4_FOR_EACH_THEORY_STATEMENT
+#endif
+#define CVC4_FOR_EACH_THEORY_STATEMENT(THEORY) \
+  if (theory::TheoryTraits<THEORY>::hasCheck) { \
+     reinterpret_cast<theory::TheoryTraits<THEORY>::theory_class*>(d_theoryTable[THEORY])->check(effort); \
+     if (!d_theoryOut.d_conflictNode.get().isNull()) { \
+       return false; \
+     } \
+  }
+
+  // Do the checking
+  try {
+    CVC4_FOR_EACH_THEORY
+  } catch(const theory::Interrupted&) {
+    Debug("theory") << "TheoryEngine::check() => conflict" << std::endl;
+  }
+
+  return true;
+}
+
+void TheoryEngine::propagate() {
+  // Definition of the statement that is to be run by every theory
+#ifdef CVC4_FOR_EACH_THEORY_STATEMENT
+#undef CVC4_FOR_EACH_THEORY_STATEMENT
+#endif
+#define CVC4_FOR_EACH_THEORY_STATEMENT(THEORY) \
+  if (theory::TheoryTraits<THEORY>::hasPropagate) { \
+      reinterpret_cast<theory::TheoryTraits<THEORY>::theory_class*>(d_theoryTable[THEORY])->propagate(theory::Theory::FULL_EFFORT); \
+  }
+
+  // Propagate for each theory using the statement above
+  CVC4_FOR_EACH_THEORY
+}
+
 /* Our goal is to tease out any ITE's sitting under a theory operator. */
 Node TheoryEngine::removeITEs(TNode node) {
   Debug("ite") << "removeITEs(" << node << ")" << endl;
@@ -294,7 +338,7 @@ Node TheoryEngine::getValue(TNode node) {
   }
 
   // otherwise ask the theory-in-charge
-  return theoryOf(node)->getValue(node, this);
+  return theoryOf(node)->getValue(node, &d_valuation);
 }/* TheoryEngine::getValue(TNode node) */
 
 bool TheoryEngine::presolve() {
diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h
index bb0e9c10e..6a343717a 100644
--- a/src/theory/theory_engine.h
+++ b/src/theory/theory_engine.h
@@ -27,8 +27,8 @@
 #include "prop/prop_engine.h"
 #include "theory/shared_term_manager.h"
 #include "theory/theory.h"
-#include "theory/theory_traits.h"
 #include "theory/rewriter.h"
+#include "theory/valuation.h"
 #include "util/options.h"
 #include "util/stats.h"
 
@@ -144,6 +144,12 @@ class TheoryEngine {
   context::CDO<bool> d_incomplete;
 
   /**
+   * A "valuation proxy" for this TheoryEngine.  Used only in getValue()
+   * for decoupled Theory-to-TheoryEngine communication.
+   */
+  theory::Valuation d_valuation;
+
+  /**
    * Replace ITE forms in a node.
    */
   Node removeITEs(TNode t);
@@ -270,31 +276,7 @@ public:
    * Check all (currently-active) theories for conflicts.
    * @param effort the effort level to use
    */
-  inline bool check(theory::Theory::Effort effort)
-  {
-    d_theoryOut.d_conflictNode = Node::null();
-    d_theoryOut.d_propagatedLiterals.clear();
-
-#ifdef CVC4_FOR_EACH_THEORY_STATEMENT
-#undef CVC4_FOR_EACH_THEORY_STATEMENT
-#endif
-#define CVC4_FOR_EACH_THEORY_STATEMENT(THEORY) \
-    if (theory::TheoryTraits<THEORY>::hasCheck) { \
-       reinterpret_cast<theory::TheoryTraits<THEORY>::theory_class*>(d_theoryTable[THEORY])->check(effort); \
-       if (!d_theoryOut.d_conflictNode.get().isNull()) { \
-         return false; \
-       } \
-    }
-
-    // Do the checking
-    try {
-      CVC4_FOR_EACH_THEORY
-    } catch(const theory::Interrupted&) {
-      Debug("theory") << "TheoryEngine::check() => conflict" << std::endl;
-    }
-
-    return true;
-  }
+  bool check(theory::Theory::Effort effort);
 
   /**
    * Calls staticLearning() on all active theories, accumulating their
@@ -332,20 +314,7 @@ public:
     return d_theoryOut.d_conflictNode;
   }
 
-  inline void propagate() {
-
-    // Definition of the statement that is to be run by every theory
-#ifdef CVC4_FOR_EACH_THEORY_STATEMENT
-#undef CVC4_FOR_EACH_THEORY_STATEMENT
-#endif
-#define CVC4_FOR_EACH_THEORY_STATEMENT(THEORY) \
-    if (theory::TheoryTraits<THEORY>::hasPropagate) { \
-        reinterpret_cast<theory::TheoryTraits<THEORY>::theory_class*>(d_theoryTable[THEORY])->propagate(theory::Theory::FULL_EFFORT); \
-    }
-
-    // Propagate for each theory using the statement above
-    CVC4_FOR_EACH_THEORY
-  }
+  void propagate();
 
   inline Node getExplanation(TNode node, theory::Theory* theory) {
     theory->explain(node);
diff --git a/src/theory/uf/morgan/theory_uf_morgan.cpp b/src/theory/uf/morgan/theory_uf_morgan.cpp
index 33c8bc7b6..5d4d44d0a 100644
--- a/src/theory/uf/morgan/theory_uf_morgan.cpp
+++ b/src/theory/uf/morgan/theory_uf_morgan.cpp
@@ -17,7 +17,7 @@
  **/
 
 #include "theory/uf/morgan/theory_uf_morgan.h"
-#include "theory/theory_engine.h"
+#include "theory/valuation.h"
 #include "expr/kind.h"
 #include "util/congruence_closure.h"
 
@@ -567,7 +567,7 @@ void TheoryUFMorgan::notifyRestart() {
   Debug("uf") << "uf: end notifyDecisionLevelZero()" << endl;
 }
 
-Node TheoryUFMorgan::getValue(TNode n, TheoryEngine* engine) {
+Node TheoryUFMorgan::getValue(TNode n, Valuation* valuation) {
   NodeManager* nodeManager = NodeManager::currentNM();
 
   switch(n.getKind()) {
@@ -585,7 +585,7 @@ Node TheoryUFMorgan::getValue(TNode n, TheoryEngine* engine) {
 
   case kind::EQUAL: // 2 args
     return nodeManager->
-      mkConst( engine->getValue(n[0]) == engine->getValue(n[1]) );
+      mkConst( valuation->getValue(n[0]) == valuation->getValue(n[1]) );
 
   default:
     Unhandled(n.getKind());
diff --git a/src/theory/uf/morgan/theory_uf_morgan.h b/src/theory/uf/morgan/theory_uf_morgan.h
index 2a079603b..47c860c9a 100644
--- a/src/theory/uf/morgan/theory_uf_morgan.h
+++ b/src/theory/uf/morgan/theory_uf_morgan.h
@@ -214,7 +214,7 @@ public:
    * Overloads Node getValue(TNode n); from theory.h.
    * See theory/theory.h for more information about this method.
    */
-  Node getValue(TNode n, TheoryEngine* engine);
+  Node getValue(TNode n, Valuation* valuation);
 
   std::string identify() const { return std::string("TheoryUFMorgan"); }
 
diff --git a/src/theory/uf/tim/theory_uf_tim.h b/src/theory/uf/tim/theory_uf_tim.h
index cdaa7975c..d07f49f03 100644
--- a/src/theory/uf/tim/theory_uf_tim.h
+++ b/src/theory/uf/tim/theory_uf_tim.h
@@ -20,7 +20,6 @@
  **  (http://portal.acm.org/ft_gateway.cfm?id=322198&type=pdf)
  ** This has been extended to work in a context-dependent way.
  ** This interacts heavily with the data-structures given in ecdata.h .
- **
  **/
 
 #include "cvc4_private.h"
@@ -151,7 +150,7 @@ public:
    * Overloads Node getValue(TNode n); from theory.h.
    * See theory/theory.h for more information about this method.
    */
-  Node getValue(TNode n, TheoryEngine* engine) {
+  Node getValue(TNode n, Valuation* valuation) {
     Unimplemented("TheoryUFTim doesn't support model generation");
   }
 
diff --git a/src/theory/valuation.cpp b/src/theory/valuation.cpp
new file mode 100644
index 000000000..20d339b52
--- /dev/null
+++ b/src/theory/valuation.cpp
@@ -0,0 +1,31 @@
+/*********************                                                        */
+/*! \file valuation.cpp
+ ** \verbatim
+ ** Original author: mdeters
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 prototype.
+ ** Copyright (c) 2009, 2010  The Analysis of Computer Systems Group (ACSys)
+ ** Courant Institute of Mathematical Sciences
+ ** New York University
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.\endverbatim
+ **
+ ** \brief A "valuation" proxy for TheoryEngine
+ **
+ ** Implementation of Valuation class.
+ **/
+
+#include "expr/node.h"
+#include "theory/valuation.h"
+#include "theory/theory_engine.h"
+
+namespace CVC4 {
+namespace theory {
+
+Node Valuation::getValue(TNode n) {
+  return d_engine->getValue(n);
+}
+
+}/* CVC4::theory namespace */
+}/* CVC4 namespace */
diff --git a/src/theory/valuation.h b/src/theory/valuation.h
new file mode 100644
index 000000000..2d38c29cd
--- /dev/null
+++ b/src/theory/valuation.h
@@ -0,0 +1,48 @@
+/*********************                                                        */
+/*! \file valuation.h
+ ** \verbatim
+ ** Original author: mdeters
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 prototype.
+ ** Copyright (c) 2009, 2010  The Analysis of Computer Systems Group (ACSys)
+ ** Courant Institute of Mathematical Sciences
+ ** New York University
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.\endverbatim
+ **
+ ** \brief A "valuation" proxy for TheoryEngine
+ **
+ ** A "valuation" proxy for TheoryEngine.  This class breaks the dependence
+ ** of theories' getValue() implementations on TheoryEngine.  getValue()
+ ** takes a Valuation, which delegates to TheoryEngine.
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef __CVC4__THEORY__VALUATION_H
+#define __CVC4__THEORY__VALUATION_H
+
+#include "expr/node.h"
+
+namespace CVC4 {
+
+class TheoryEngine;
+
+namespace theory {
+
+class Valuation {
+  TheoryEngine* d_engine;
+public:
+  Valuation(TheoryEngine* engine) :
+    d_engine(engine) {
+  }
+
+  Node getValue(TNode n);
+
+};/* class Valuation */
+
+}/* CVC4::theory namespace */
+}/* CVC4 namespace */
+
+#endif /* __CVC4__THEORY__VALUATION_H */