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).
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.
|
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.
|
BDD_ONE | A special terminal BDDFunc which is constant true (one).
|
BDD_ZERO | A special terminal BDDFunc which is constant false (zero).
|
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.
|
BDDFunc | A BDDFunc is a function index within a particular BDD . It must only
be used with the BDD instance which produced it.
|