Crate biodivine_lib_bdd

This crate provides a basic implementation of binary decision diagrams (BDDs) — a symbolic data structure for representing boolean functions or other equivalent objects (such as bit-vector sets).

Compared to other popular implementations, every BDD owns its memory. It is thus trivial to serialise, but also to share between threads. This makes it useful for applications that process high number of BDDs concurrently.

We currently provide support for explicit operations as well as evaluation of basic boolean expressions and a custom bdd macro for hybrid usage:

use biodivine_lib_bdd::*;

let vars = BddVariableSet::new(vec!["a", "b", "c"]);
let a = vars.mk_var_by_name("a");
let b = vars.mk_var_by_name("b");
let c = vars.mk_var_by_name("c");

let f1 = a.iff(&b.not()).or(&c.xor(&a));
let f2 = vars.eval_expression_string("(a <=> !b) | c ^ a");
let f3 = bdd!((a <=> (!b)) | (c ^ a));

assert!(!f1.is_false());
assert_eq!(f1.cardinality(), 6.0);
assert_eq!(f1, f2);
assert_eq!(f2, f3);
assert!(f1.iff(&f2).is_true());
assert!(f1.iff(&f3).is_true());

Additionally, we provide serialisation into a custom string and binary formats as well as .dot. For a more detailed description, see the tutorial module documentation. There is also an experimental support for converting BDDs back into boolean expressions.

Modules

boolean_expression	Boolean expressions are simple structures that represent boolean formulas explicitly.
tutorial	This is a documentation-only module with several sub-modules describing how to use this crate.

Macros

bdd	A macro for simplifying Bdd operations. It evaluates given expression over Bdds where you can use standard boolean operators !, &, |, ^, => and <=>.

Structs

Bdd	An array-based encoding of the binary decision diagram implementing basic logical operations.
BddValuation	Exactly describes one assignment of boolean values to variables of a Bdd.
BddValuationIterator	Exhaustively iterates over all valuations with a certain number of variables.
BddVariable	Identifies one of the variables that can appear as a decision condition in the Bdd.
BddVariableSet	Maintains the set of variables that can appear in a Bdd. Used to create new Bdds for basic formulas.
BddVariableSetBuilder	Used to safely initialize BddVariableSet.