diff options
Diffstat (limited to 'src/theory')
| -rw-r--r-- | src/theory/theory_engine.cpp | 18 |
1 files changed, 13 insertions, 5 deletions
diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp index 9cd226ba1..9ef228865 100644 --- a/src/theory/theory_engine.cpp +++ b/src/theory/theory_engine.cpp @@ -260,7 +260,6 @@ void TheoryEngine::EngineOutputChannel::conflict(TNode conflictNode, Trace("theory::conflict") << "EngineOutputChannel<" << d_theory << ">::conflict(" << conflictNode << ")" << std::endl; - Trace("dtview::conflict") << ":CONFLICT: " << conflictNode << std::endl; Assert(!proof); // Theory shouldn't be producing proofs yet ++d_statistics.conflicts; d_engine->d_outputChannelUsed = true; @@ -1302,6 +1301,8 @@ void TheoryEngine::assertToTheory(TNode assertion, TNode originalAssertion, theo if (d_propEngine->hasValue(assertion, value)) { if (!value) { Trace("theory::propagate") << "TheoryEngine::assertToTheory(" << assertion << ", " << toTheoryId << ", " << fromTheoryId << "): conflict (no sharing)" << endl; + Trace("dtview::conflict") + << ":THEORY-CONFLICT: " << assertion << std::endl; d_inConflict = true; } else { return; @@ -1352,7 +1353,12 @@ void TheoryEngine::assertToTheory(TNode assertion, TNode originalAssertion, theo // Check for propositional conflicts bool value; if (d_propEngine->hasValue(assertion, value) && !value) { - Trace("theory::propagate") << "TheoryEngine::assertToTheory(" << assertion << ", " << toTheoryId << ", " << fromTheoryId << "): conflict (sharing)" << endl; + Trace("theory::propagate") + << "TheoryEngine::assertToTheory(" << assertion << ", " + << toTheoryId << ", " << fromTheoryId << "): conflict (sharing)" + << endl; + Trace("dtview::conflict") + << ":THEORY-CONFLICT: " << assertion << std::endl; d_inConflict = true; } } @@ -1401,9 +1407,6 @@ void TheoryEngine::assertFact(TNode literal) return; } - Trace("dtview::prop") << std::string(d_context->getLevel(), ' ') << literal - << endl; - // Get the atom bool polarity = literal.getKind() != kind::NOT; TNode atom = polarity ? literal : literal[0]; @@ -1460,6 +1463,9 @@ bool TheoryEngine::propagate(TNode literal, theory::TheoryId theory) { Debug("theory::propagate") << "TheoryEngine::propagate(" << literal << ", " << theory << ")" << endl; + Trace("dtview::prop") << std::string(d_context->getLevel(), ' ') + << ":THEORY-PROP: " << literal << endl; + // spendResource(); if(Dump.isOn("t-propagations")) { @@ -1922,6 +1928,8 @@ void TheoryEngine::conflict(TNode conflict, TheoryId theoryId) { Debug("theory::conflict") << "TheoryEngine::conflict(" << conflict << ", " << theoryId << ")" << endl; + Trace("dtview::conflict") << ":THEORY-CONFLICT: " << conflict << std::endl; + // Mark that we are in conflict d_inConflict = true; |