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
 77
 78
 79
 80
 81
 82
 83
 84
 85
 86
 87
 88
 89
 90
 91
 92
 93
 94
 95
 96
 97
 98
 99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134

use crate::*;
use std::io::Write;

/// `.dot` export procedure for `Bdd`s.
impl Bdd {
    /// Output this `Bdd` as a `.dot` string into the given `output` writer.
    ///
    /// Variable names in the graph are resolved from the given `BddVariableSet`.
    ///
    /// If `zero_pruned` is true, edges leading to `zero` are not shown. This can greatly
    /// simplify the graph without losing information.
    pub fn write_as_dot_string(
        &self,
        output: &mut dyn Write,
        variables: &BddVariableSet,
        zero_pruned: bool,
    ) -> Result<(), std::io::Error> {
        write_bdd_as_dot(output, self, &variables.var_names, zero_pruned)
    }

    /// Convert this `Bdd` to a `.dot` string.
    ///
    /// Variable names in the graph are resolved from the given `BddVariableSet`.
    ///
    /// If `zero_pruned` is true, edges leading to `zero` are not shown. This can greatly
    /// simplify the graph without losing information.
    pub fn to_dot_string(&self, variables: &BddVariableSet, zero_pruned: bool) -> String {
        bdd_to_dot_string(self, &variables.var_names, zero_pruned)
    }
}

/// Write given `Bdd` into the output buffer as `.dot` graph. Use `var_names` to specify
/// custom names for individual variables. If `pruned` is true, the output will only
/// contain edges leading to the `1` terminal node (this is often much easier to read
/// than the full graph while preserving all the information).
fn write_bdd_as_dot(
    output: &mut dyn Write,
    bdd: &Bdd,
    var_names: &[String],
    zero_pruned: bool,
) -> Result<(), std::io::Error> {
    writeln!(output, "digraph G {{")?;
    writeln!(
        output,
        "init__ [label=\"\", style=invis, height=0, width=0];"
    )?;
    writeln!(output, "init__ -> {};", bdd.root_pointer())?;

    /*
       Fortunately, it seem that .dot does not care about ordering of graph elements,
       so we can just go through the BDD and print it as is.

       Note that for BDD slices, this can output unused nodes, but we don't support slices yet anyway.
    */

    // terminal nodes
    if !zero_pruned {
        writeln!(
            output,
            "0 [shape=box, label=\"0\", style=filled, shape=box, height=0.3, width=0.3];"
        )?;
    }
    writeln!(
        output,
        "1 [shape=box, label=\"1\", style=filled, shape=box, height=0.3, width=0.3];"
    )?;

    // decision nodes
    for node_pointer in bdd.pointers().skip(2) {
        // write the node itself
        let var_name = &var_names[bdd.var_of(node_pointer).0 as usize];
        writeln!(output, "{}[label=\"{}\"];", node_pointer, var_name)?;
        let high_link = bdd.high_link_of(node_pointer);
        if !zero_pruned || !high_link.is_zero() {
            // write "high" link
            writeln!(output, "{} -> {} [style=filled];", node_pointer, high_link)?;
        }
        let low_link = bdd.low_link_of(node_pointer);
        if !zero_pruned || !low_link.is_zero() {
            // write "low" link
            writeln!(output, "{} -> {} [style=dotted];", node_pointer, low_link)?;
        }
    }
    writeln!(output, "}}")?;
    Ok(())
}

/// Converts the given BDD to a .dot graph string using given variable names.
///
/// See also: [bdd_as_dot](fn.bdd_as_dot.html)
fn bdd_to_dot_string(bdd: &Bdd, var_names: &[String], zero_pruned: bool) -> String {
    let mut buffer: Vec<u8> = Vec::new();
    write_bdd_as_dot(&mut buffer, bdd, var_names, zero_pruned)
        .expect("Cannot write BDD to .dot string.");
    String::from_utf8(buffer).expect("Invalid UTF formatting in .dot string.")
}

#[cfg(test)]
mod tests {
    use crate::_test_util::{load_expected_results, mk_small_test_bdd};
    use crate::*;

    #[test]
    fn bdd_to_dot() {
        let bdd = mk_small_test_bdd();
        let variables = BddVariableSet::new(&["a", "b", "c", "d", "e"]);
        let dot = bdd.to_dot_string(&variables, false);
        assert_eq!(load_expected_results("bdd_to_dot.dot"), dot);
    }

    #[test]
    fn bdd_to_dot_pruned() {
        let variables = BddVariableSet::new(&["a", "b", "c", "d", "e"]);
        let bdd = mk_small_test_bdd();
        let dot = bdd.to_dot_string(&variables, true);
        assert_eq!(load_expected_results("bdd_to_dot_pruned.dot"), dot);
    }

    #[test]
    fn bdd_universe_bdd_to_dot() {
        let variables = BddVariableSet::new(&["a", "b", "c", "d", "e"]);
        let bdd = variables.eval_expression_string("c & !d");
        let dot = bdd.to_dot_string(&variables, false);
        assert_eq!(load_expected_results("bdd_to_dot.dot"), dot);
    }

    #[test]
    fn bdd_universe_bdd_to_dot_pruned() {
        let variables = BddVariableSet::new(&["a", "b", "c", "d", "e"]);
        let bdd = variables.eval_expression_string("c & !d");
        let dot = bdd.to_dot_string(&variables, true);
        assert_eq!(load_expected_results("bdd_to_dot_pruned.dot"), dot);
    }
}