diff options
| -rw-r--r-- | src/prop/minisat/core/Solver.cc | 42 | ||||
| -rw-r--r-- | src/theory/theory_engine.cpp | 18 |
2 files changed, 55 insertions, 5 deletions
diff --git a/src/prop/minisat/core/Solver.cc b/src/prop/minisat/core/Solver.cc index 83f6fb897..6e5dc664e 100644 --- a/src/prop/minisat/core/Solver.cc +++ b/src/prop/minisat/core/Solver.cc @@ -77,6 +77,34 @@ static inline void dtviewPropagationHeaderHelper(size_t level) << " /Propagations/" << std::endl; } +// Writes to Trace macro for propagation tracing +static inline void dtviewBoolPropagationHelper(size_t level, + Lit& l, + CVC4::prop::TheoryProxy* proxy) +{ + Trace("dtview::prop") << std::string( + level + 1 - (options::incrementalSolving() ? 1 : 0), ' ') + << ":BOOL-PROP: " + << proxy->getNode(MinisatSatSolver::toSatLiteral(l)) + << std::endl; +} + +// Writes to Trace macro for conflict tracing +static inline void dtviewPropConflictHelper(size_t level, + Clause& confl, + CVC4::prop::TheoryProxy* proxy) +{ + Trace("dtview::conflict") + << std::string(level + 1 - (options::incrementalSolving() ? 1 : 0), ' ') + << ":PROP-CONFLICT: (or"; + for (int i = 0; i < confl.size(); i++) + { + Trace("dtview::conflict") + << " " << proxy->getNode(MinisatSatSolver::toSatLiteral(confl[i])); + } + Trace("dtview::conflict") << ")" << std::endl; +} + } // namespace //================================================================================================= @@ -1054,6 +1082,14 @@ CRef Solver::propagate(TheoryCheckType type) confl = updateLemmas(); } } else { + // if dumping decision tree, print the conflict + if (Trace.isOn("dtview::conflict")) + { + if (confl != CRef_Undef) + { + dtviewPropConflictHelper(decisionLevel(), ca[confl], proxy); + } + } // Even though in conflict, we still need to discharge the lemmas if (lemmas.size() > 0) { // Remember the trail size @@ -1148,6 +1184,12 @@ CRef Solver::propagateBool() Watcher *i, *j, *end; num_props++; + // if propagation tracing enabled, print boolean propagation + if (Trace.isOn("dtview::prop")) + { + dtviewBoolPropagationHelper(decisionLevel(), p, proxy); + } + for (i = j = (Watcher*)ws, end = i + ws.size(); i != end;){ // Try to avoid inspecting the clause: Lit blocker = i->blocker; 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; |