Crate boolean_expression

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 Aliases

BDDFunc

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