Skip to content

Commit 0c850ce

Browse files
committed
Fix Bdd::to_dot, add test
1 parent 8dd30ae commit 0c850ce

File tree

1 file changed

+37
-8
lines changed

1 file changed

+37
-8
lines changed

src/dot.rs

Lines changed: 37 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -55,21 +55,20 @@ impl Bdd {
5555
continue;
5656
}
5757

58-
// Note: use " " (space) label to avoid an overlap with "-1" label
59-
6058
let high = self.high(id);
6159
assert!(!high.is_negated());
62-
writeln!(dot, "{} -- {} [label=\" \"];", id, high.index())?;
60+
writeln!(dot, "{} -- {};", id, high.index())?;
6361

6462
let low = self.low(id);
6563
if low.is_negated() {
6664
if low.index() == 1 {
67-
writeln!(dot, "{} -- 0 [label=\" \", style=dashed];", id)?;
65+
assert_eq!(low, self.zero);
66+
writeln!(dot, "{} -- 0 [style=dashed];", id)?;
6867
} else {
69-
writeln!(dot, "{} -- {} [label=\"-1\", style=dotted];", id, low.index())?;
68+
writeln!(dot, "{} -- {} [style=dotted, dir=forward, arrowhead=odot];", id, low.index())?;
7069
}
7170
} else {
72-
writeln!(dot, "{} -- {} [label=\" \", style=dashed];", id, low.index())?;
71+
writeln!(dot, "{} -- {} [style=dashed];", id, low.index())?;
7372
}
7473
}
7574

@@ -84,9 +83,9 @@ impl Bdd {
8483
for (i, &root) in roots.iter().enumerate() {
8584
if root.is_negated() {
8685
if root.index() == 1 {
87-
writeln!(dot, "r{} -- 0 [style=dashed];", i)?;
86+
writeln!(dot, "r{} -- 0;", i)?;
8887
} else {
89-
writeln!(dot, "r{} -- {} [style=dashed];", i, root.index())?;
88+
writeln!(dot, "r{} -- {} [dir=forward, arrowhead=odot];", i, root.index())?;
9089
}
9190
} else {
9291
writeln!(dot, "r{} -- {};", i, root.index())?;
@@ -97,3 +96,33 @@ impl Bdd {
9796
Ok(dot)
9897
}
9998
}
99+
100+
#[cfg(test)]
101+
mod tests {
102+
use super::*;
103+
104+
//noinspection RsConstantConditionIf
105+
#[test]
106+
fn test_to_dot() {
107+
let bdd = Bdd::default();
108+
109+
let f = bdd.cube([-1, 2, 3]);
110+
println!("f = {}", bdd.to_bracket_string(f));
111+
112+
let dot = bdd.to_dot(&[f, bdd.zero, bdd.one]).unwrap();
113+
println!("DOT for f:");
114+
print!("{}", dot);
115+
116+
if false {
117+
std::fs::write("bdd.dot", dot).unwrap();
118+
for format in ["png", "pdf"] {
119+
std::process::Command::new("dot")
120+
.arg(format!("-T{}", format))
121+
.arg("-O")
122+
.arg("bdd.dot")
123+
.status()
124+
.unwrap();
125+
}
126+
}
127+
}
128+
}

0 commit comments

Comments
 (0)