1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76

//! Utilities for saving the current BDD as a graphviz file for visualization

use super::{
    hash_select::{HashMap, HashSet},
    DDManager, ZERO,
};
use crate::bdd_node::{DDNode, NodeID, VarID};

impl DDManager {
    /// Collect all nodes that are part of the specified function
    fn collect_nodes(&self, f: NodeID) -> HashSet<NodeID> {
        let mut nodes = HashSet::<NodeID>::default();

        let mut stack = vec![f];

        while !stack.is_empty() {
            let x = stack.pop().unwrap();

            if nodes.contains(&x) {
                continue;
            }

            let node = self.nodes.get(&x).unwrap();

            stack.push(node.low);
            stack.push(node.high);
            nodes.insert(x);
        }

        nodes
    }

    /// Generate graphviz for the provided function, not including any graph nodes not part of the function.
    /// TODO: Graphviz of all functions in DDManager
    pub fn graphviz(&self, f: NodeID) -> String {
        let nodes = self.collect_nodes(f);

        let mut by_var: HashMap<VarID, Vec<DDNode>> = HashMap::default();
        for id in nodes.iter() {
            let node = self.nodes.get(id).unwrap();
            by_var.entry(node.var).or_default().push(*node);
        }

        let mut graph = String::new();
        graph += "digraph G {\n";
        graph += "newrank=true;\n";
        graph += "\"1\" [shape = \"box\"];\n";
        graph += "\"0\" [shape = \"box\"];\n";

        let mut edges = String::new();
        for (var, nodes) in by_var {
            if var == ZERO.var {
                continue;
            }
            graph += format!("subgraph cluster_{} {{\nrank=same;\n", var.0).as_str();
            for node in nodes {
                graph += format!(
                    "\"{}\" [label=\"Var:{}\\n{}\"];\n",
                    node.id.0, var.0, node.id.0
                )
                .as_str();
                edges += format!(
                    "\"{}\" -> \"{}\" [style = \"dotted\"];\n",
                    node.id.0, node.low.0
                )
                .as_str();
                edges += format!("\"{}\" -> \"{}\";\n", node.id.0, node.high.0).as_str();
            }
            graph += "}\n\n";
        }

        graph += edges.as_str();
        graph += "}\n";
        graph
    }
}