Crate ruddy 

Ruddy is a minimalistic, high-performance Rust library for (reduced and ordered) binary decision diagrams (BDDs), which are a compact representation of Boolean functions.

The name Ruddy is a blend of BuDDy (one of the first widely used BDD libraries) and Rust. However, Ruddy is not affiliated with the developers of BuDDy in any formal way.

Features

Most popular BDD implementations use a shared representation, where all BDD nodes are stored in a single pool managed by a manager. This allows graphs shared between BDDs to be stored only once in memory. An alternative is the split representation, where each BDD owns its nodes (e.g., as an array).

When BDDs do not meaningfully share nodes, split representations can be faster and more memory-efficient. Ruddy implements both representations, letting users choose what works best for their use case.

Currently, Ruddy supports the following features:

• Binary logical operators (conjunction, xor, …) and negation.
• Existential and universal quantification, also combined with a binary operator (also called relational product).
• Satisfying valuations and paths iterators along with methods to count them.
• Export to DOT.
• Conversion between split and shared BDDs.
• Binary and text (de)serialization of split BDDs.

Usage

An example of using the Ruddy split implementation:

use ruddy::split::Bdd;
use ruddy::VariableId;

// Create two variables v0 and v1.
let v0 = VariableId::new(0);
let v1 = VariableId::new(1);

// Make the BDDs representing `v0=true` and `v1=true`.
let a = Bdd::new_literal(v0, true);
let b = Bdd::new_literal(v1, true);

// Calculate BDD `a => b`.
let imp = a.implies(&b);

// Calculate BDD `!a ∨ b`.
let equiv_imp = a.not().or(&b);

// Check that they are equivalent.
assert!(imp.iff(&equiv_imp).is_true());

or, with the shared implementation:

use ruddy::shared::BddManager;
use ruddy::VariableId;

// Create the manager.
let mut manager = BddManager::new();

// Create two variables v0 and v1.
let v0 = VariableId::new(0);
let v1 = VariableId::new(1);

// Make the BDDs representing `v0=true` and `v1=true`.
let a = manager.new_bdd_literal(v0, true);
let b = manager.new_bdd_literal(v1, true);

// Calculate BDD `a => b`.
let imp = manager.implies(&a, &b);

// Calculate BDD `!a ∨ b`.
let not_a = manager.not(&a);
let equiv_imp = manager.or(&not_a, &b);

// Check that they are equivalent.
assert_eq!(imp, equiv_imp);

More complex examples can be found in the examples folder.

Modules

boolean_operators

Defines binary boolean operators And, Or, Xor, and others, used in crate::split::Bdd::apply, crate::shared::BddManager::apply, and crate::split::Bdd::nested_apply, crate::shared::BddManager::nested_apply plus its variants.

shared

Provides the structures for working with shared binary decision diagrams, mainly BddManager and Bdd.

split

Provides the structures for working with split binary decision diagrams, mainly Bdd.

Structs

NodeId

A type for identifying nodes in BDDs.

VariableId

A type for identifying variables in BDDs.

Enums

DeserializeIdError

An error which can be returned when deserializing a variable or node identifier.

Traits

NodeIdAny

An internal trait implemented by types that can serve as BDD node identifiers. The core property of this trait is that a node ID must have one designated “undefined” value (similar to Option::None and equivalent to the maximal representable value), and two designated “terminal” values equivalent to 0 and 1. Every other node id must fall in the 1 < id < undefined interval.