Skip to main content

oxidd_dump/dot/
dot_impl.rs

1use std::fmt;
2use std::io;
3use std::ops::Deref;
4
5use oxidd_core::function::{ETagOfFunc, Function, TermOfFunc};
6use oxidd_core::util::EdgeDropGuard;
7use oxidd_core::{Edge, InnerNode, LevelNo, LevelView, Manager};
8
9use super::DotStyle;
10
11/// Dump the entire decision diagram represented by `manager` as Graphviz DOT
12/// code to `file`
13///
14/// To label functions in the decision diagram, you can pass pairs of function
15/// and name (type `D`, implementing [`std::fmt::Display`]).
16pub fn dump_all<'a, 'id, FR: Deref, D>(
17    mut file: impl io::Write,
18    manager: &<FR::Target as Function>::Manager<'id>,
19    functions: impl IntoIterator<Item = (FR, D)>,
20) -> io::Result<()>
21where
22    FR::Target: 'a + Function + DotStyle<ETagOfFunc<'id, FR::Target>>,
23    ETagOfFunc<'id, FR::Target>: fmt::Debug,
24    TermOfFunc<'id, FR::Target>: fmt::Display,
25    D: fmt::Display,
26{
27    writeln!(file, "digraph DD {{")?;
28
29    let mut edges = Vec::new();
30
31    for (level_no, level) in manager.levels().enumerate() {
32        let level_no = level_no as LevelNo;
33        let level_name = manager.var_name(manager.level_to_var(level_no));
34        if level_name.is_empty() {
35            writeln!(
36                file,
37                "  {{ rank = same; l{level_no:x} [label=\"{level_no}\", color=\"#AAAAAA\", shape=none, tooltip=\"level {level_no}\"];"
38            )?;
39        } else {
40            // TODO: escaping for level_name
41            writeln!(
42                file,
43                "  {{ rank = same; l{level_no:x} [label=\"{level_name}\", shape=none, tooltip=\"level {level_no}\"];"
44            )?;
45        }
46
47        for edge in level.iter() {
48            let id = edge.node_id();
49            let node = manager
50                .get_node(edge)
51                .expect_inner("unique tables should not include terminal nodes");
52            let rc = node.ref_count();
53
54            // note outgoing edges
55            // TODO: maybe use a second pass instead?
56            for (idx, child) in node.children().enumerate() {
57                edges.push(('x', id, child.node_id(), idx, child.tag()));
58            }
59
60            // Unreferenced nodes are gray
61            let color = if rc == 0 { ", color=\"#AAAAAA\"" } else { "" };
62            writeln!(
63                file,
64                "    x{id:x} [label=\"\"{color}, tooltip=\"id: {id:#x}, rc: {rc}\"];"
65            )?;
66        }
67
68        writeln!(file, "  }};")?;
69    }
70
71    const TERMINAL_LEVEL: LevelNo = LevelNo::MAX;
72    writeln!(file, "  {{ rank = same; l{TERMINAL_LEVEL:x} [label=\"-\", shape=none, tooltip=\"level {TERMINAL_LEVEL} (terminals)\"];")?;
73    for edge in manager.terminals() {
74        let edge = EdgeDropGuard::new(manager, edge);
75        let id = edge.node_id();
76        let node = manager.get_node(&*edge);
77        let terminal = node.unwrap_terminal();
78        writeln!(
79            file,
80            "    x{id:x} [label=\"{terminal}\", tooltip=\"terminal, id: 0x{id:x}\"];"
81        )?;
82    }
83    writeln!(file, "  }};")?;
84
85    let num_levels = manager.num_levels();
86    if num_levels != 0 {
87        // If `levels` is empty, there is no point in writing the order (even
88        // if there are terminals).
89        write!(file, "  ")?;
90        for level in 0..num_levels {
91            write!(file, "l{level:x} -> ")?;
92        }
93        // spell-checker:ignore invis
94        writeln!(file, "l{TERMINAL_LEVEL:x} [style=invis];")?;
95    }
96
97    for (i, (func, label)) in functions.into_iter().enumerate() {
98        // TODO: escape label string
99        writeln!(file, "  f{i:x} [label=\"{label}\", shape=box];")?;
100        let edge = func.as_edge(manager);
101        edges.push(('f', i, edge.node_id(), 0, edge.tag()));
102    }
103
104    for (parent_type, parent, child, idx, tag) in edges {
105        let (style, bold, color) = FR::Target::edge_style(idx, tag);
106        let bold = if bold { ",bold" } else { "" };
107        writeln!(
108            file,
109            "  {parent_type}{parent:x} -> x{child:x} [style=\"{style}{bold}\", color=\"{color}\", tooltip=\"child {idx}, tag: {tag:?}\"];"
110        )?;
111    }
112
113    writeln!(file, "}}")?;
114    Ok(())
115}