Crate biodivine_lib_bdd 

Biodivine/LibBDD

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, but is also generally more idiomatic in Rust.

At the moment, we support many standard operations on BDDs:

• Any binary logical operation (and, or, iff, …), and of course negation.
• Evaluation of Boolean expressions parsed from a string.
• A bdd! macro for a more idiomatic specification of operation chains.
• Simplified methods for CNF/DNF formula construction.
• Binary and text serialization/deserialization.
• Valuation/path iterators and other Bdd introspection methods (random_valuation, most_fixed_clause, …).
• Export of Bdd back into a Boolean expression.
• “Relational” operations: projection (existential quantification), selection (restriction) and unique subset picking (see tutorials for more info).
• A “variable flip” operation fused with custom logical binary operators.
• Export to .dot graphs.

More detailed description of all features can be found in our tutorial module, and of course in the API documentation.

use biodivine_lib_bdd::*;

let mut builder = BddVariableSetBuilder::new();
let [a, b, c] = builder.make(&["a", "b", "c"]);
let variables: BddVariableSet = builder.build();

// String expressions:
let x = variables.eval_expression_string("(a <=> !b) | c ^ a");
// Macro:
let y = bdd!(variables, (a <=> (!b)) | (c ^ a));
// Logical operators:
let z = variables.mk_literal(a, true)
    .iff(&variables.mk_literal(b, false))
    .or(&variables.mk_literal(c, true).xor(&variables.mk_literal(a, true)));

assert!(!x.is_false());
assert_eq!(6.0, x.cardinality());
assert_eq!(x, y);
assert_eq!(y, z);
assert_eq!(z, x);

for valuation in x.sat_valuations() {
    assert!(x.eval_in(&valuation));
}

Modules

boolean_expression

Boolean expressions are simple structures that represent boolean formulas explicitly.

op_function

Contains simple functions that can be used with apply and fused_flip_apply to implement basic logical operations.

random_sampling

tutorial

This is a documentation-only module with several submodules 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.

BddNode

(internal) Representation of individual vertices of the Bdd directed acyclic graph.

BddPartialValuation

Describes assignment of some arbitrary number of Bdd variables.

BddPathIterator

An iterator which goes through all paths in the Bdd, representing them as clauses using BddPartialValuation.

BddPointer

A type-safe index into the Bdd node array representation.

BddSatisfyingValuations

An iterator over all satisfying valuations of a specific BDD.

BddValuation

Exactly describes one assignment of boolean values to variables of a Bdd.

BddValuationIteratorDeprecated

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.

OwnedBddPathIterator

Same as BddPathIterator, but owns the underlying Bdd and thus does not require a lifetime.

OwnedBddSatisfyingValuations

Same as BddSatisfyingValuations, but owns the underlying Bdd and thus does not require a lifetime.

ValuationsOfClauseIterator

An iterator which goes through all valuations that satisfy a specific conjunctive clause.

Traits

IntoBdd

A trait which allows quick conversion of a type into a Bdd, assuming an appropriate BddVariablesSet is provided.