diff options
Diffstat (limited to 'src/theory/theory_engine.cpp')
-rw-r--r-- | src/theory/theory_engine.cpp | 89 |
1 files changed, 57 insertions, 32 deletions
diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp index a3aee985d..c19bdda91 100644 --- a/src/theory/theory_engine.cpp +++ b/src/theory/theory_engine.cpp @@ -124,6 +124,50 @@ void TheoryEngine::preRegister(TNode preprocessed) { // } } +void TheoryEngine::printAssertions(const char* tag) { + if (Debug.isOn(tag)) { + for (TheoryId theoryId = THEORY_FIRST; theoryId < THEORY_LAST; ++theoryId) { + Theory* theory = d_theoryTable[theoryId]; + if (theory && d_logicInfo.isTheoryEnabled(theoryId)) { + Debug(tag) << "--------------------------------------------" << std::endl; + Debug(tag) << "Assertions of " << theory->getId() << ": " << std::endl; + context::CDList<Assertion>::const_iterator it = theory->facts_begin(), it_end = theory->facts_end(); + for (unsigned i = 0; it != it_end; ++ it, ++i) { + if ((*it).isPreregistered) { + Debug(tag) << "[" << i << "]: "; + } else { + Debug(tag) << "(" << i << "): "; + } + Debug(tag) << (*it).assertion << endl; + } + + if (d_logicInfo.isSharingEnabled()) { + Debug(tag) << "Shared terms of " << theory->getId() << ": " << std::endl; + context::CDList<TNode>::const_iterator it = theory->shared_terms_begin(), it_end = theory->shared_terms_end(); + for (unsigned i = 0; it != it_end; ++ it, ++i) { + Debug(tag) << "[" << i << "]: " << (*it) << endl; + } + } + } + } + + } +} + +template<typename T, bool doAssert> +class scoped_vector_clear { + vector<T>& d_v; +public: + scoped_vector_clear(vector<T>& v) + : d_v(v) { + Assert(!doAssert || d_v.empty()); + } + ~scoped_vector_clear() { + d_v.clear(); + } + +}; + /** * Check all (currently-active) theories for conflicts. * @param effort the effort level to use @@ -143,12 +187,12 @@ void TheoryEngine::check(Theory::Effort effort) { } \ } + // make sure d_propagatedSharedLiterals is cleared on exit + scoped_vector_clear<SharedLiteral, true> clear_shared_literals(d_propagatedSharedLiterals); + // Do the checking try { - // Clear any leftover propagated shared literals - d_propagatedSharedLiterals.clear(); - // Mark the output channel unused (if this is FULL_EFFORT, and nothing // is done by the theories, no additional check will be needed) d_outputChannelUsed = false; @@ -159,32 +203,10 @@ void TheoryEngine::check(Theory::Effort effort) { while (true) { Debug("theory") << "TheoryEngine::check(" << effort << "): running check" << std::endl; + Assert(d_propagatedSharedLiterals.empty()); if (Debug.isOn("theory::assertions")) { - for (TheoryId theoryId = THEORY_FIRST; theoryId < THEORY_LAST; ++theoryId) { - Theory* theory = d_theoryTable[theoryId]; - if (theory && d_logicInfo.isTheoryEnabled(theoryId)) { - Debug("theory::assertions") << "--------------------------------------------" << std::endl; - Debug("theory::assertions") << "Assertions of " << theory->getId() << ": " << std::endl; - context::CDList<Assertion>::const_iterator it = theory->facts_begin(), it_end = theory->facts_end(); - for (unsigned i = 0; it != it_end; ++ it, ++i) { - if ((*it).isPreregistered) { - Debug("theory::assertions") << "[" << i << "]: "; - } else { - Debug("theory::assertions") << "(" << i << "): "; - } - Debug("theory::assertions") << (*it).assertion << endl; - } - - if (d_logicInfo.isSharingEnabled()) { - Debug("theory::assertions") << "Shared terms of " << theory->getId() << ": " << std::endl; - context::CDList<TNode>::const_iterator it = theory->shared_terms_begin(), it_end = theory->shared_terms_end(); - for (unsigned i = 0; it != it_end; ++ it, ++i) { - Debug("theory::assertions") << "[" << i << "]: " << (*it) << endl; - } - } - } - } + printAssertions("theory::assertions"); } // Do the checking @@ -232,9 +254,6 @@ void TheoryEngine::check(Theory::Effort effort) { } } - // Clear any leftover propagated shared literals - d_propagatedSharedLiterals.clear(); - Debug("theory") << "TheoryEngine::check(" << effort << "): done, we are " << (d_inConflict ? "unsat" : "sat") << (d_lemmasAdded ? " with new lemmas" : " with no new lemmas") << std::endl; } catch(const theory::Interrupted&) { @@ -243,6 +262,9 @@ void TheoryEngine::check(Theory::Effort effort) { } void TheoryEngine::outputSharedLiterals() { + + scoped_vector_clear<SharedLiteral, false> clear_shared_literals(d_propagatedSharedLiterals); + // Assert all the shared literals for (unsigned i = 0; i < d_propagatedSharedLiterals.size(); ++ i) { const SharedLiteral& eq = d_propagatedSharedLiterals[i]; @@ -258,8 +280,6 @@ void TheoryEngine::outputSharedLiterals() { } } } - // Clear the equalities - d_propagatedSharedLiterals.clear(); } @@ -269,7 +289,9 @@ void TheoryEngine::combineTheories() { TimerStat::CodeTimer combineTheoriesTimer(d_combineTheoriesTime); + // Care graph we'll be building CareGraph careGraph; + #ifdef CVC4_FOR_EACH_THEORY_STATEMENT #undef CVC4_FOR_EACH_THEORY_STATEMENT #endif @@ -278,6 +300,7 @@ void TheoryEngine::combineTheories() { reinterpret_cast<theory::TheoryTraits<THEORY>::theory_class*>(theoryOf(THEORY))->getCareGraph(careGraph); \ } + // Call on each parametric theory to give us its care graph CVC4_FOR_EACH_THEORY; // Now add splitters for the ones we are interested in @@ -833,6 +856,8 @@ Node TheoryEngine::getExplanation(TNode node) { } Assert(properExplanation(node, explanation)); + Debug("theory::explain") << "TheoryEngine::getExplanation(" << node << ") => " << explanation << std::endl; + return explanation; } |