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, 45 insertions, 1 deletions

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() {