Subtypes of graph_nodet can override DOT output

This commit introduces a virtual pretty() method to graph_nodet, whose
default implementation has the same behaviour as before (only outputting
the node's graph index with no attributes when dumped to a Graphviz DOT
file). Subtypes of graph_nodet can override this method to provide a
more informative representation of themselves when grapht::output_dot()
is called.

Author: karkhaz

src/util/graph.h

@@ -16,6 +16,7 @@ Author: Daniel Kroening, [email protected]
 #include <cassert>
 #include <functional>
 #include <iosfwd>
+#include <iostream>
 #include <list>
 #include <map>
 #include <queue>
@@ -60,6 +61,36 @@ class graph_nodet
   {
     out.erase(n);
   }
+
+  /// \brief Node with attributes suitable for Graphviz DOT format
+  ///
+  /// Derived types may override this function to produce more informative DOT
+  /// diagrams than the default implementation, which displays only the node
+  /// index. The return value should either be an empty string, or a single line
+  /// representing this node that can be parsed by `dot`. This line would
+  /// typically be the node index, followed by whitespace, followed by a list of
+  /// node attributes within square brackets. Here is a sample implementation
+  /// for a fictional node type with `is_evil()` and `is_pink()` functions:
+  ///
+  ///     std::stringstream ss;
+  ///     ss << std::to_string(idx)
+  ///        << " [shape=\"" << is_evil() ? "box" : "diamond"
+  ///        << "\", color=\"" << is_pink() ? "#e91e63" : "#9c27b0"
+  ///        << "\", label=\"this is node " << std::to_string(idx)
+  ///        << "\"]";
+  ///     return ss.str();
+  ///
+  /// If this function returns an empty string for a particular node,
+  /// grapht::output_dot() method will not output this node at all, nor any of
+  /// its incoming or outgoing edges.
+  virtual std::string pretty(node_indext idx) const
+  {
+    return std::to_string(idx);
+  }
+
+  virtual ~graph_nodet()
+  {
+  }
 };
 
 /// A node type with an extra bit
@@ -877,9 +908,14 @@ void output_dot_generic(
   const std::function<
     void(const node_index_type &, std::function<void(const node_index_type &)>)>
     &for_each_succ,
-  const std::function<std::string(const node_index_type &)> node_to_string)
+  const std::function<std::string(const node_index_type &)> node_to_string,
+  const std::function<std::string(const node_index_type &)> node_to_pretty)
 {
   for_each_node([&](const node_index_type &i) {
+    const std::string pretty = node_to_pretty(i);
+    if(pretty == "")
+      return;
+    out << pretty << ";\n";
     for_each_succ(i, [&](const node_index_type &n) {
       out << node_to_string(i) << " -> " << node_to_string(n) << '\n';
     });
@@ -924,8 +960,14 @@ void grapht<N>::output_dot(std::ostream &out) const
     for_each_successor(i, f);
   };
 
-  const auto to_string = [](const node_indext &i) { return std::to_string(i); };
-  output_dot_generic<node_indext>(out, for_each_node, for_each_succ, to_string);
+  const auto to_string = [&](const node_indext &i) {
+    return std::to_string(i);
+  };
+  const auto to_pretty_string = [&](const node_indext &i) {
+    return nodes[i].pretty(i);
+  };
+  output_dot_generic<node_indext>(
+    out, for_each_node, for_each_succ, to_string, to_pretty_string);
 }
 
 #endif // CPROVER_UTIL_GRAPH_H