diff options
Diffstat (limited to 'src/theory/theory_engine.cpp')
-rw-r--r-- | src/theory/theory_engine.cpp | 47 |
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)) { |