biodivine_lib_bdd/tutorial/
p04_bdd_serialisation.rs

1//! # Serialising and visualising `Bdd`s
2//!
3//! We currently provide three ways to inspect `Bdd`s. Human-friendly way is to export the
4//! `Bdd` as a **`.dot` graph file** which can be then rendered into an SVG using tools like
5//! [graph-viz](http://www.webgraphviz.com/). Aside from `.dot`, we have two very basic
6//! formats for serialising `Bdd`s. They both essentially just dump the corresponding node
7//! array. However, the difference is that one format is **string-based**, which means it
8//! can be easily used inside things like JSON or XML. The second format uses the same
9//! layout, but is fully **binary**, hence it takes up much less space compared to the
10//! string-based format (and is faster).
11//!
12//! ## `String` serialisation
13//!
14//! Given a `Bdd`, we can create a string where each node is serialised as three
15//! numbers, `variable,low_link,high_link` and nodes are written as present in the `Bdd`
16//! array, separated by `|`:
17//!
18//! ```rust
19//! use biodivine_lib_bdd::{Bdd, BddVariableSet};
20//! let variables = BddVariableSet::new(&["a", "b"]);
21//! let bdd = variables.eval_expression_string("a & !b");
22//! let bdd_string = bdd.to_string();
23//!
24//! assert_eq!("|2,0,0|2,1,1|1,1,0|0,0,2|", bdd_string);
25//! assert_eq!(bdd, Bdd::from_string(&bdd_string));
26//! ```
27//!
28//! Both serialisation and deserialization methods have a "streaming" variant where
29//! you can provide your own custom `Read`/`Write` implementations.
30//!
31//! ## `u8` serialisation
32//!
33//! A `Bdd` can be also written to a byte array. This is much more compact for large `Bdd`s
34//! and has the advantage of predictable size:
35//!
36//! ```rust
37//! use biodivine_lib_bdd::{Bdd, BddVariableSet};
38//! let variables = BddVariableSet::new(&["a", "b"]);
39//! let bdd = variables.eval_expression_string("a & !b");
40//! let bdd_bytes: Vec<u8> = bdd.to_bytes();
41//!
42//! assert_eq!(bdd_bytes.len(), bdd.size() * 10);
43//! assert_eq!(bdd, Bdd::from_bytes(&mut &bdd_bytes[..]))
44//! ```
45//!
46//! As in the case of `String` serialisation, each method can be also used with a
47//! custom `Read`/`Write` object.
48//!
49//! ## `.dot` visualisation
50//!
51//! In order to output `Bdd` as a `.dot` graph, we have to specify a `BddVariableSet` as it provides
52//! specific variable names used in the graph:
53//!
54//! ```rust
55//! use biodivine_lib_bdd::BddVariableSet;
56//!
57//! let variables = BddVariableSet::new(&["a", "b", "c"]);
58//! let bdd = variables.eval_expression_string("a & !(b | c)");
59//! let dot = bdd.to_dot_string(&variables, true);
60//! ```
61//!
62//! The method takes an extra boolean parameter, `pruned`. If set to `true`, edges leading to the
63//! zero terminal are not included in the graph. This makes it much more readable, since these
64//! edges can be inferred from context anyway.
65//!
66//!
biodivine_lib_bdd/tutorial/p04_bdd_serialisation.rs

biodivine_lib_bdd/tutorial/
p04_bdd_serialisation.rs
