1 files changed, 27 insertions, 20 deletions

diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp
index 6fbd4a417..6dfc9f22d 100644
--- a/src/theory/theory_engine.cpp
+++ b/src/theory/theory_engine.cpp
@@ -69,8 +69,6 @@ TheoryEngine::TheoryEngine(context::Context* context,
   d_propagationMapTimestamp(context, 0),
   d_propagatedLiterals(context),
   d_propagatedLiteralsIndex(context, 0),
-  d_decisionRequests(context),
-  d_decisionRequestsIndex(context, 0),
   d_combineTheoriesTime("TheoryEngine::combineTheoriesTime"),
   d_inPreregister(false),
   d_factsAsserted(context, false),
@@ -285,7 +283,7 @@ void TheoryEngine::check(Theory::Effort effort) {
 #endif
 #define CVC4_FOR_EACH_THEORY_STATEMENT(THEORY) \
     if (theory::TheoryTraits<THEORY>::hasCheck && d_logicInfo.isTheoryEnabled(THEORY)) { \
-       reinterpret_cast<theory::TheoryTraits<THEORY>::theory_class*>(theoryOf(THEORY))->check(effort); \
+       theoryOf(THEORY)->check(effort); \
        if (d_inConflict) { \
          break; \
        } \
@@ -392,7 +390,7 @@ void TheoryEngine::combineTheories() {
 #endif
 #define CVC4_FOR_EACH_THEORY_STATEMENT(THEORY) \
   if (theory::TheoryTraits<THEORY>::isParametric && d_logicInfo.isTheoryEnabled(THEORY)) { \
-     reinterpret_cast<theory::TheoryTraits<THEORY>::theory_class*>(theoryOf(THEORY))->getCareGraph(careGraph); \
+    theoryOf(THEORY)->getCareGraph(careGraph); \
   }
 
   // Call on each parametric theory to give us its care graph
@@ -456,7 +454,7 @@ void TheoryEngine::propagate(Theory::Effort effort) {
 #endif
 #define CVC4_FOR_EACH_THEORY_STATEMENT(THEORY) \
   if (theory::TheoryTraits<THEORY>::hasPropagate && d_logicInfo.isTheoryEnabled(THEORY)) { \
-    reinterpret_cast<theory::TheoryTraits<THEORY>::theory_class*>(theoryOf(THEORY))->propagate(effort); \
+    theoryOf(THEORY)->propagate(effort); \
   }
 
   // Propagate for each theory using the statement above
@@ -478,6 +476,25 @@ void TheoryEngine::propagate(Theory::Effort effort) {
   }
 }
 
+Node TheoryEngine::getNextDecisionRequest() {
+  // 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>::hasGetNextDecisionRequest && d_logicInfo.isTheoryEnabled(THEORY)) { \
+    Node n = theoryOf(THEORY)->getNextDecisionRequest(); \
+    if(! n.isNull()) { \
+      return n; \
+    } \
+  }
+
+  // Request decision from each theory using the statement above
+  CVC4_FOR_EACH_THEORY;
+
+  return TNode();
+}
+
 bool TheoryEngine::properConflict(TNode conflict) const {
   bool value;
   if (conflict.getKind() == kind::AND) {
@@ -573,7 +590,7 @@ bool TheoryEngine::presolve() {
 #endif
 #define CVC4_FOR_EACH_THEORY_STATEMENT(THEORY) \
     if (theory::TheoryTraits<THEORY>::hasPresolve) { \
-      reinterpret_cast<theory::TheoryTraits<THEORY>::theory_class*>(theoryOf(THEORY))->presolve(); \
+      theoryOf(THEORY)->presolve(); \
       if(d_inConflict) { \
         return true; \
       } \
@@ -597,7 +614,7 @@ void TheoryEngine::postsolve() {
 #endif
 #define CVC4_FOR_EACH_THEORY_STATEMENT(THEORY) \
     if (theory::TheoryTraits<THEORY>::hasPostsolve) { \
-      reinterpret_cast<theory::TheoryTraits<THEORY>::theory_class*>(theoryOf(THEORY))->postsolve(); \
+      theoryOf(THEORY)->postsolve(); \
       Assert(! d_inConflict, "conflict raised during postsolve()"); \
     }
 
@@ -616,7 +633,7 @@ void TheoryEngine::notifyRestart() {
 #endif
 #define CVC4_FOR_EACH_THEORY_STATEMENT(THEORY) \
   if (theory::TheoryTraits<THEORY>::hasNotifyRestart && d_logicInfo.isTheoryEnabled(THEORY)) { \
-    reinterpret_cast<theory::TheoryTraits<THEORY>::theory_class*>(theoryOf(THEORY))->notifyRestart(); \
+    theoryOf(THEORY)->notifyRestart(); \
   }
 
   // notify each theory using the statement above
@@ -630,8 +647,8 @@ void TheoryEngine::ppStaticLearn(TNode in, NodeBuilder<>& learned) {
 #undef CVC4_FOR_EACH_THEORY_STATEMENT
 #endif
 #define CVC4_FOR_EACH_THEORY_STATEMENT(THEORY) \
-  if (theory::TheoryTraits<THEORY>::hasStaticLearning) { \
-    reinterpret_cast<theory::TheoryTraits<THEORY>::theory_class*>(theoryOf(THEORY))->ppStaticLearn(in, learned); \
+  if (theory::TheoryTraits<THEORY>::hasPpStaticLearn) { \
+    theoryOf(THEORY)->ppStaticLearn(in, learned); \
   }
 
   // static learning for each theory using the statement above
@@ -1027,16 +1044,6 @@ bool TheoryEngine::propagate(TNode literal, theory::TheoryId theory) {
 }
 
 
-void TheoryEngine::propagateAsDecision(TNode literal, theory::TheoryId theory) {
-  Debug("theory") << "EngineOutputChannel::propagateAsDecision(" << literal << ", " << theory << ")" << std::endl;
-
-  d_propEngine->checkTime();
-
-  Assert(d_propEngine->isSatLiteral(literal.getKind() == kind::NOT ? literal[0] : literal), "OutputChannel::propagateAsDecision() requires a SAT literal (or negation of one)");
-
-  d_decisionRequests.push_back(literal);
-}
-
 theory::EqualityStatus TheoryEngine::getEqualityStatus(TNode a, TNode b) {
   Assert(a.getType().isComparableTo(b.getType()));
   if (d_sharedTerms.isShared(a) && d_sharedTerms.isShared(b)) {