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

3 files changed, 5 insertions, 6 deletions

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");
   }