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.

diff --git a/src/prop/minisat/core/Solver.cc b/src/prop/minisat/core/Solver.cc
index 83f6fb897f8bbd9bd9c9b1aa9252d1cc6009ed45..6e5dc664ebedd7c31d927622564a6e8187e02e6a 100644 (file)
--- 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 9cd226ba1ab3daa7bef94719bd7921851e8ee9bc..9ef228865a34aa66bdd4eac30a40b94545ea3b50 100644 (file)
--- 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;