Trace tags for dumping the decision tree in org-mode format (#2871)

This would add tracing options to print the decision tree in [org-mode](https://orgmode.org/) format which can be viewed with emacs or [vim-orgmode](https://github.com/jceb/vim-orgmode).

In the raw format, the number of asterisks denote the decision level of a decision, and within a propagation node, the number of spaces denote the level. Most viewers render the asterisks as indented bullets.

There are some options for controlling verbosity:
`dtview` - prints the decisions (basic option)
`dtview::command` - also prints smt-lib commands as they're issued
`dtview::conflict` - also prints conflicts
`dtview::prop` - also prints propagations

Example usage:
`cvc4 -t dtview -t dtview::command -t dtview::conflict -t dtview::prop <example smt2 file> &> example-trace.org`

The resulting file when opened with an org-mode viewer has collapsible nodes, where "..." marks a node with children.

diff --git a/src/prop/minisat/core/Solver.cc b/src/prop/minisat/core/Solver.cc
index 5b097dc39544cec9a6a9069abdf99e2f8cb33b94..6126983fa3f41a2f11197e2a251939d2c56501d6 100644 (file)
--- a/src/prop/minisat/core/Solver.cc
+++ b/src/prop/minisat/core/Solver.cc
@@ -56,6 +56,27 @@ bool assertionLevelOnly()
 {
   return options::unsatCores() && options::incrementalSolving();
 }
+
+//=================================================================================================
+// Helper functions for decision tree tracing
+
+// Writes to Trace macro for decision tree tracing
+static inline void dtviewDecisionHelper(size_t level,
+                                        const Node& node,
+                                        const char* decisiontype)
+{
+  Trace("dtview") << std::string(level - (options::incrementalSolving() ? 1 : 0), '*')
+                  << " " << node << " :" << decisiontype << "-DECISION:" << std::endl;
+}
+
+// Writes to Trace macro for propagation tracing
+static inline void dtviewPropagationHeaderHelper(size_t level)
+{
+  Trace("dtview::prop") << std::string(level + 1 - (options::incrementalSolving() ? 1 : 0),
+                                       '*')
+                        << " /Propagations/" << std::endl;
+}
+
 }  // namespace
 
 //=================================================================================================
@@ -607,6 +628,20 @@ Lit Solver::pickBranchLit()
             << "getNextTheoryDecisionRequest(): now deciding on " << nextLit
             << std::endl;
         decisions++;
+
+        // org-mode tracing -- theory decision
+        if (Trace.isOn("dtview"))
+        {
+          dtviewDecisionHelper(context->getLevel(),
+                               proxy->getNode(MinisatSatSolver::toSatLiteral(nextLit)),
+                               "THEORY");
+        }
+
+        if (Trace.isOn("dtview::prop"))
+        {
+          dtviewPropagationHeaderHelper(context->getLevel());
+        }
+
         return nextLit;
       } else {
         Debug("theoryDecision")
@@ -631,10 +666,23 @@ Lit Solver::pickBranchLit()
       decisions++;
       Var next = var(nextLit);
       if(polarity[next] & 0x2) {
-        return mkLit(next, polarity[next] & 0x1);
-      } else {
-        return nextLit;
+        nextLit = mkLit(next, polarity[next] & 0x1);
       }
+
+      // org-mode tracing -- decision engine decision
+      if (Trace.isOn("dtview"))
+      {
+        dtviewDecisionHelper(context->getLevel(),
+                             proxy->getNode(MinisatSatSolver::toSatLiteral(nextLit)),
+                             "DE");
+      }
+
+      if (Trace.isOn("dtview::prop"))
+      {
+        dtviewPropagationHeaderHelper(context->getLevel());
+      }
+
+      return nextLit;
     }
 
     Var next = var_Undef;
@@ -668,12 +716,32 @@ Lit Solver::pickBranchLit()
       // Check with decision engine if it can tell polarity
       lbool dec_pol = MinisatSatSolver::toMinisatlbool
         (proxy->getDecisionPolarity(MinisatSatSolver::toSatVariable(next)));
+      Lit decisionLit;
       if(dec_pol != l_Undef) {
         Assert(dec_pol == l_True || dec_pol == l_False);
-        return mkLit(next, (dec_pol == l_True) );
+        decisionLit = mkLit(next, (dec_pol == l_True));
       }
-      // If it can't use internal heuristic to do that
-      return mkLit(next, rnd_pol ? drand(random_seed) < 0.5 : (polarity[next] & 0x1));
+      else
+      {
+        // If it can't use internal heuristic to do that
+        decisionLit = mkLit(
+            next, rnd_pol ? drand(random_seed) < 0.5 : (polarity[next] & 0x1));
+      }
+
+      // org-mode tracing -- decision engine decision
+      if (Trace.isOn("dtview"))
+      {
+        dtviewDecisionHelper(context->getLevel(),
+                             proxy->getNode(MinisatSatSolver::toSatLiteral(decisionLit)),
+                             "DE");
+      }
+
+      if (Trace.isOn("dtview::prop"))
+      {
+        dtviewPropagationHeaderHelper(context->getLevel());
+      }
+
+      return decisionLit;
     }
 }
 

diff --git a/src/prop/minisat/core/Solver.h b/src/prop/minisat/core/Solver.h
index b6da9b9c800173ff9378cfcfa20f537d7bccf30e..aa3b96c57edc04c0083e94e25df0fc10de197f12 100644 (file)
--- a/src/prop/minisat/core/Solver.h
+++ b/src/prop/minisat/core/Solver.h
@@ -455,6 +455,7 @@ protected:
     // Returns a random integer 0 <= x < size. Seed must never be 0.
     static inline int irand(double& seed, int size) {
         return (int)(drand(seed) * size); }
+
 };
 
 

diff --git a/src/smt/command.cpp b/src/smt/command.cpp
index 76ce1bda9e96fa148e029b55a9c91921ea30fc79..d8301283f6c2f22212502ffe34dc276dc1f8577f 100644 (file)
--- a/src/smt/command.cpp
+++ b/src/smt/command.cpp
@@ -265,6 +265,8 @@ void EchoCommand::invoke(SmtEngine* smtEngine)
 void EchoCommand::invoke(SmtEngine* smtEngine, std::ostream& out)
 {
   out << d_output << std::endl;
+  Trace("dtview::command") << "* ~COMMAND: echo |" << d_output << "|~"
+                           << std::endl;
   d_commandStatus = CommandSuccess::instance();
   printResult(out,
               smtEngine->getOption("command-verbosity:" + getCommandName())
@@ -393,6 +395,8 @@ CheckSatCommand::CheckSatCommand(const Expr& expr) : d_expr(expr) {}
 Expr CheckSatCommand::getExpr() const { return d_expr; }
 void CheckSatCommand::invoke(SmtEngine* smtEngine)
 {
+  Trace("dtview::command") << "* ~COMMAND: " << getCommandName() << "~"
+                           << std::endl;
   try
   {
     d_result = smtEngine->checkSat(d_expr);
@@ -413,6 +417,7 @@ void CheckSatCommand::printResult(std::ostream& out, uint32_t verbosity) const
   }
   else
   {
+    Trace("dtview::command") << "* RESULT: " << d_result << std::endl;
     out << d_result << endl;
   }
 }
@@ -453,6 +458,8 @@ const std::vector<Expr>& CheckSatAssumingCommand::getTerms() const
 
 void CheckSatAssumingCommand::invoke(SmtEngine* smtEngine)
 {
+  Trace("dtview::command") << "* ~COMMAND: (check-sat-assuming ( " << d_terms
+                           << " )~" << std::endl;
   try
   {
     d_result = smtEngine->checkSat(d_terms);
@@ -466,6 +473,7 @@ void CheckSatAssumingCommand::invoke(SmtEngine* smtEngine)
 
 Result CheckSatAssumingCommand::getResult() const
 {
+  Trace("dtview::command") << "* ~RESULT: " << d_result << "~" << std::endl;
   return d_result;
 }
 

diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp
index 7a72367de608d213d9dd1ca5c17a990b02935c13..0a70ddab44d4e81bb77bdaa247436cc2b3199a66 100644 (file)
--- a/src/theory/theory_engine.cpp
+++ b/src/theory/theory_engine.cpp
@@ -259,6 +259,7 @@ 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;
@@ -1399,6 +1400,9 @@ 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];