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, 7 insertions, 2 deletions

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