# boolean_expression expression manipulation / BDD library

This crate provides for the manipulation and evaluation of Boolean expressions and Binary Decision Diagrams (BDDs), and the construction of BDDs from Boolean expressions. It can also simplify Boolean expressions via either a set of rules such as DeMorgan's Law (see `Expr::simplify_via_laws()`), or via a roundtrip through a `BDD` and a cubelist-based term reduction (see `Expr::simplify_via_bdd()`). The latter is more powerful, but also more expensive.

The main pieces of interest are:

• `Expr`, an AST enum for expression simple `AND` / `OR` / `NOT`-based expressions.
• `BDD`, a Binary Decision Diagram implementation.
• `CubeList`, a low-level datatype with support for cubelist manipulation (used when converting `BDD` functions to expressions).

## Structs

 BDD A `BDD` is a Binary Decision Diagram, an efficient way to represent a Boolean function in a canonical way. (It is actually a "Reduced Ordered Binary Decision Diagram", which gives it its canonicity assuming terminals are ordered consistently.) Cube A `Cube` is one (multidimensional) cube in the variable space: i.e., a particular set of variable assignments, where each variable is assigned either true, false, or "don't care". CubeList A `CubeList` is a sum (OR'd list) of cubes. It represents a Boolean expression in sum-of-products form, by construction. PersistedBDD A `PersistedBDD` is a wrapper around a `BDD` that provides a means to write BDD labels and nodes out to a `BDDOutput`. It tracks how much of the BDD has already been writen out, and writes out new nodes and labels as required when its `persist()` or `persist_all()` method is called.

## Enums

 CubeMergeResult The result of attempting to merge two cubes. CubeVar A variable assignment in a cube. Expr An `Expr` is a simple Boolean logic expression. It may contain terminals (i.e., free variables), constants, and the following fundamental operations: AND, OR, NOT.

## Constants

 BDD_ONE A special terminal `BDDFunc` which is constant `true` (one). BDD_ZERO A special terminal `BDDFunc` which is constant `false` (zero).

## Traits

 BDDOutput The `BDDOutput` trait provides an interface to inform a listener about new BDD nodes that are created. It allows the user to persist a BDD to a stream (e.g., a log or trace file) as a long-running process executes. A `BDDOutput` instance may be provided to all BDD operations.

## Type Definitions

 BDDFunc A `BDDFunc` is a function index within a particular `BDD`. It must only be used with the `BDD` instance which produced it.