1 files changed, 9 insertions, 40 deletions
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);