diff options
Diffstat (limited to 'src/prop')
-rw-r--r-- | src/prop/minisat/core/Solver.cc | 42 |
1 files changed, 42 insertions, 0 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; |