ddnnife 0.10.0

d-DNNF toolkit
Documentation 
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

use crate::{Ddnnf, NodeType};
use std::io::Write;

/// Takes a Ddnnf, transforms it into a corresponding markdown mermaid representation,
/// and saves it into the provided file name.
///
/// We als add a legend that describes the mermaidified nodes
pub fn write_as_mermaid_md(
    ddnnf: &mut Ddnnf,
    features: &[i32],
    mut output: impl Write,
) -> std::io::Result<()> {
    for node in ddnnf.nodes.iter_mut() {
        node.temp.clone_from(&node.count);
    }

    ddnnf.operate_on_partial_config_marker(features, Ddnnf::calc_count_marked_node);

    let config = format!(
        "```mermaid\n\t\
    graph TD
        subgraph pad1 [ ]
            subgraph pad2 [ ]
                subgraph legend[Legend]
                    nodes(\"<font color=white> Node Type <font color=cyan> \
                    Node Number <font color=greeny> Count <font color=red> Temp Count \
                    <font color=orange> Query {features:?}\")
                    style legend fill:none, stroke:none
                end
                style pad2 fill:none, stroke:none
            end
            style pad1 fill:none, stroke:none
        end
        classDef marked stroke:#d90000, stroke-width:4px\n\n"
    );
    output.write_all(config.as_bytes()).unwrap();
    let marking = ddnnf.get_marked_nodes_clone(features);
    output.write_all(mermaidify_nodes(ddnnf, &marking).as_bytes())?;
    output.write_all(b"```").unwrap();

    Ok(())
}

/// Adds the nodes its children to the mermaid graph
fn mermaidify_nodes(ddnnf: &Ddnnf, marking: &[usize]) -> String {
    let mut result = String::new();

    for (position, node) in ddnnf.nodes.iter().enumerate().rev() {
        result = format!(
            "{}{}",
            result,
            match &node.ntype {
                NodeType::And { children } | NodeType::Or { children } => {
                    let mut mm_node = format!(
                        "\t\t{}{} --> ",
                        mermaidify_type(ddnnf, position),
                        marking_insert(marking, position)
                    );

                    let mut children_series = children.clone();
                    children_series.sort_unstable();

                    if !children_series.is_empty() {
                        for (i, &child) in children_series.iter().enumerate() {
                            if ddnnf.nodes[child].ntype == NodeType::True {
                                continue;
                            }
                            mm_node.push_str(&child.to_string());
                            if i != children_series.len() - 1 {
                                mm_node.push_str(" & ");
                            } else {
                                mm_node.push_str(";\n");
                            }
                        }
                    }
                    mm_node
                }
                NodeType::Literal { literal: _ } | NodeType::False => {
                    format!(
                        "\t\t{}{};\n",
                        mermaidify_type(ddnnf, position),
                        marking_insert(marking, position)
                    )
                }
                _ => String::new(),
            }
        );
    }

    result
}

/// Each node in the mermaid graph contains information about
///     1) NodeType,
///     2) Position in the flattened graph,
///     3) Count (of the model)
///     4) Current Temp Count
fn mermaidify_type(ddnnf: &Ddnnf, position: usize) -> String {
    let node = &ddnnf.nodes[position];
    let mut mm_node = format!(
        "{}{}",
        position,
        match node.ntype {
            NodeType::And { children: _ } => String::from("(\"∧"),
            NodeType::Or { children: _ } => String::from("(\"∨"),
            NodeType::Literal { literal } => {
                if literal.is_negative() {
                    format!("(\"¬L{}", literal.abs())
                } else {
                    format!("(\"L{literal}")
                }
            }
            NodeType::True => String::from("(\"T"),
            NodeType::False => String::from("(\"F"),
        }
    );

    let meta_info = format!(
        " <font color=cyan>{} <font color=greeny>{} <font color=red>{}\")",
        position, node.count, node.temp
    );
    mm_node.push_str(&meta_info);
    mm_node
}

fn marking_insert(marking: &[usize], position: usize) -> &str {
    if marking.binary_search(&position).is_ok() {
        ":::marked"
    } else {
        ""
    }
}