Crate boolean_expression [−] [src]

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.)
BDDLoader	A `BDDLoader` provides a way to inject BDD nodes directly, as they were previously dumped by a `PersistedBDD` to a `BDDOutput`. The user should create a `BDDLoader` instance wrapped around a `BDD` and call `inject_label` and `inject_node` as appropriate to inject labels and nodes.
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.