diff options
author | makaimann <makaim@stanford.edu> | 2020-02-21 22:13:31 -0800 |
---|---|---|
committer | GitHub <noreply@github.com> | 2020-02-21 22:13:31 -0800 |
commit | a626d85e490256a5d872fec49910cdb43e85c16d (patch) | |
tree | 8fa55a5d8c71cb1b841ac58e2b8801fc0da7550e /src/prop/minisat/core | |
parent | a98cd6d50308d1dde1086f0c1502e022bd30ba1b (diff) |
Dump boolean propagations and conflicts for decision tree org-mode viewer (#3788)
PR #2871 added trace tags for dumping the decision tree in org-mode format. However, it only dumped theory propagations/conflicts. This could be confusing because it would appear to backtrack without reaching a conflict (but actually the conflict was at the propositional level). This commit also adds dumping of boolean propagations and conflicts.
Diffstat (limited to 'src/prop/minisat/core')
-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; |