oxidd_dump/
dot.rs

1//! Visual representation using [dot]
2//!
3//! [dot]: https://graphviz.org/docs/layouts/dot/
4
5use std::fmt;
6use std::io;
7
8use oxidd_core::function::Function;
9use oxidd_core::util::EdgeDropGuard;
10use oxidd_core::Edge;
11use oxidd_core::HasLevel;
12use oxidd_core::InnerNode;
13use oxidd_core::LevelNo;
14use oxidd_core::LevelView;
15use oxidd_core::Manager;
16use oxidd_core::Tag;
17
18/// Edge styles
19#[derive(Clone, Copy, PartialEq, Eq, Debug)]
20pub enum EdgeStyle {
21    #[allow(missing_docs)]
22    Solid,
23    #[allow(missing_docs)]
24    Dashed,
25    #[allow(missing_docs)]
26    Dotted,
27}
28
29impl fmt::Display for EdgeStyle {
30    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
31        let str = match self {
32            EdgeStyle::Solid => "solid",
33            EdgeStyle::Dashed => "dashed",
34            EdgeStyle::Dotted => "dotted",
35        };
36        write!(f, "{str}")
37    }
38}
39
40/// RGB colors
41///
42/// `Color(0, 0, 0)` is black, `Color(255, 255, 255)` is white.
43#[derive(Clone, Copy, PartialEq, Eq, Debug)]
44pub struct Color(pub u8, pub u8, pub u8);
45
46impl Color {
47    #[allow(missing_docs)]
48    pub const BLACK: Self = Color(0, 0, 0);
49}
50
51impl fmt::Display for Color {
52    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
53        write!(f, "#{:02X}{:02X}{:02X}", self.0, self.1, self.2)
54    }
55}
56
57/// Styling attributes defined by the node type
58pub trait DotStyle<T: Tag> {
59    /// Get the style for the `n`-th outgoing edge, tagged with `tag`
60    ///
61    /// Returns the edge style (solid/dashed/dotted), whether it is bold, and
62    /// the color.
63    ///
64    /// The default implementation distinguishes three kinds of edges (all
65    /// non-bold and black):
66    ///
67    /// 1. If the edge is tagged (i.e. `tag` is not the default value) then the
68    ///    edge is dotted.
69    /// 2. If the edge is untagged and the second edge (`no == 1`), then it is
70    ///    dashed
71    /// 3. Otherwise the edge is solid
72    fn edge_style(no: usize, tag: T) -> (EdgeStyle, bool, Color) {
73        (
74            if tag != Default::default() {
75                EdgeStyle::Dotted
76            } else if no == 1 {
77                EdgeStyle::Dashed
78            } else {
79                EdgeStyle::Solid
80            },
81            false,
82            Color::BLACK,
83        )
84    }
85}
86
87/// Dump the entire decision diagram represented by `manager` as Graphviz DOT
88/// code to `file`
89///
90/// `variables` contains pairs of edges representing the variable and names
91/// (`VD`, implementing [`std::fmt::Display`]). `functions` contains pairs of
92/// edges representing the function and names (`FD`, implementing
93/// [`std::fmt::Display`]). In both cases, the order of elements does not
94/// matter.
95pub fn dump_all<'a, 'id, F, VD, FD>(
96    mut file: impl io::Write,
97    manager: &F::Manager<'id>,
98    variables: impl IntoIterator<Item = (&'a F, VD)>,
99    functions: impl IntoIterator<Item = (&'a F, FD)>,
100) -> io::Result<()>
101where
102    F: 'a + Function + DotStyle<<<F::Manager<'id> as Manager>::Edge as Edge>::Tag>,
103    <F::Manager<'id> as Manager>::InnerNode: HasLevel,
104    <<F::Manager<'id> as Manager>::Edge as Edge>::Tag: fmt::Debug,
105    <F::Manager<'id> as Manager>::Terminal: fmt::Display,
106    VD: fmt::Display + Clone,
107    FD: fmt::Display,
108{
109    writeln!(file, "digraph DD {{")?;
110
111    let mut last_level = LevelNo::MAX;
112    let mut levels = vec![None; manager.num_levels() as usize];
113
114    for (f, label) in variables {
115        let node = manager
116            .get_node(f.as_edge(manager))
117            .expect_inner("variables must not be const terminals");
118        levels[node.level() as usize] = Some(label);
119    }
120
121    let mut edges = Vec::new();
122
123    for level in manager.levels() {
124        for edge in level.iter() {
125            let id = edge.node_id();
126            let node = manager
127                .get_node(edge)
128                .expect_inner("unique tables should not include terminal nodes");
129            let rc = node.ref_count();
130            let level = node.level();
131
132            // note outgoing edges
133            // TODO: maybe use a second pass instead?
134            for (idx, child) in node.children().enumerate() {
135                edges.push(('x', id, child.node_id(), idx, child.tag()));
136            }
137
138            if level != last_level {
139                if last_level != LevelNo::MAX {
140                    // No closing braces before the first level
141                    writeln!(file, "  }};")?;
142                }
143
144                if let Some(level_name) = &levels[level as usize] {
145                    // TODO: escaping for level_name
146                    writeln!(
147                        file,
148                        "  {{ rank = same; l{level:x} [label=\"{level_name}\", shape=none, tooltip=\"level {level}\"];"
149                    )?;
150                } else {
151                    writeln!(
152                        file,
153                        "  {{ rank = same; l{level:x} [label=\"{level}\", color=\"#AAAAAA\", shape=none, tooltip=\"level {level}\"];"
154                    )?;
155                }
156                last_level = level;
157            }
158
159            // Unreferenced nodes are gray
160            let color = if rc == 0 { ", color=\"#AAAAAA\"" } else { "" };
161            writeln!(
162                file,
163                "    x{id:x} [label=\"\"{color}, tooltip=\"id: {id:#x}, rc: {rc}\"];"
164            )?;
165        }
166    }
167    writeln!(file, "  }};")?;
168
169    const TERMINAL_LEVEL: LevelNo = LevelNo::MAX;
170    writeln!(file, "  {{ rank = same; l{TERMINAL_LEVEL:x} [label=\"-\", shape=none, tooltip=\"level {TERMINAL_LEVEL} (terminals)\"];")?;
171    for edge in manager.terminals() {
172        let edge = EdgeDropGuard::new(manager, edge);
173        let id = edge.node_id();
174        let node = manager.get_node(&*edge);
175        let terminal = node.unwrap_terminal();
176        writeln!(
177            file,
178            "    x{id:x} [label=\"{terminal}\", tooltip=\"terminal, id: 0x{id:x}\"];"
179        )?;
180    }
181    writeln!(file, "  }};")?;
182
183    if !levels.is_empty() {
184        // If `levels` is empty, there is no point in writing the order (even
185        // if there are terminals).
186        write!(file, "  ")?;
187        for level in 0..levels.len() {
188            write!(file, "l{level:x} -> ")?;
189        }
190        // spell-checker:ignore invis
191        writeln!(file, "l{TERMINAL_LEVEL:x} [style=invis];")?;
192    }
193
194    for (i, (func, label)) in functions.into_iter().enumerate() {
195        // TODO: escape label string
196        writeln!(file, "  f{i:x} [label=\"{label}\", shape=box];")?;
197        let edge = func.as_edge(manager);
198        edges.push(('f', i, edge.node_id(), 0, edge.tag()));
199    }
200
201    for (parent_type, parent, child, idx, tag) in edges {
202        let (style, bold, color) = F::edge_style(idx, tag);
203        let bold = if bold { ",bold" } else { "" };
204        writeln!(
205            file,
206            "  {parent_type}{parent:x} -> x{child:x} [style=\"{style}{bold}\", color=\"{color}\", tooltip=\"child {idx}, tag: {tag:?}\"];"
207        )?;
208    }
209
210    writeln!(file, "}}")?;
211    Ok(())
212}
oxidd_dump/dot.rs

oxidd_dump/
dot.rs
