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.

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;