# Struct boolean_expression::BDD
[−]
[src]

`pub struct BDD<T> where`

T: Clone + Debug + Eq + Ord + Hash, { /* fields omitted */ }

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.)

A BDD is built up from terminals (free variables) and constants, combined with the logical combinators AND, OR, and NOT. It may be evaluated with certain terminal assignments.

The major advantage of a BDD is that its logical operations are performed,
it will "self-simplify": i.e., taking the OR of `And(a, b)`

and `And(a, Not(b))`

will produce `a`

without any further simplification step. Furthermore,
the `BDDFunc`

representing this value is canonical: if two different
expressions are produced within the same BDD and they both result in
(simplify down to) `a`

, then the `BDDFunc`

values will be equal. The
tradeoff is that logical operations may be expensive: they are linear in
BDD size, but BDDs may have exponential size (relative to terminal count)
in the worst case.

## Methods

`impl<T> BDD<T> where`

T: Clone + Debug + Eq + Ord + Hash,

[src]

T: Clone + Debug + Eq + Ord + Hash,

`pub fn new() -> BDD<T>`

[src]

Produce a new, empty, BDD.

`pub fn terminal(&mut self, t: T) -> BDDFunc`

[src]

Produce a function within the BDD representing the terminal `t`

. If
this terminal has been used in the BDD before, the same `BDDFunc`

will be
returned.

`pub fn constant(&mut self, val: bool) -> BDDFunc`

[src]

Produce a function within the BDD representing the constant value `val`

.

`pub fn not(&mut self, n: BDDFunc) -> BDDFunc`

[src]

Produce a function within the BDD representing the logical complement
of the function `n`

.

`pub fn and(&mut self, a: BDDFunc, b: BDDFunc) -> BDDFunc`

[src]

Produce a function within the BDD representing the logical AND of the
functions `a`

and `b`

.

`pub fn or(&mut self, a: BDDFunc, b: BDDFunc) -> BDDFunc`

[src]

Produce a function within the BDD representing the logical OR of the
functions `a`

and `b`

.

`pub fn implies(&mut self, a: BDDFunc, b: BDDFunc) -> BDDFunc`

[src]

Produce a function within the BDD representing the logical implication `a`

-> `b`

.

`pub fn sat(&self, f: BDDFunc) -> bool`

[src]

Check whether the function `f`

within the BDD is satisfiable.

`pub fn restrict(&mut self, f: BDDFunc, t: T, val: bool) -> BDDFunc`

[src]

Return a new function based on `f`

but with the given label forced to the given value.

`pub fn from_expr(&mut self, e: &Expr<T>) -> BDDFunc`

[src]

Produce a function within the BDD representing the given expression
`e`

, which may contain ANDs, ORs, NOTs, terminals, and constants.

`pub fn evaluate(&self, f: BDDFunc, values: &HashMap<T, bool>) -> bool`

[src]

Evaluate the function `f`

in the BDD with the given terminal
assignments. Any terminals not specified in `values`

default to `false`

.

`pub fn sat_one(&self, f: BDDFunc) -> Option<HashMap<T, bool>>`

[src]

Compute an assignment for terminals which satisfies 'f'. If satisfiable, this function returns a HashMap with the assignments (true, false) for terminals unless a terminal's assignment does not matter for satisfiability. If 'f' is not satisfiable, returns None.

Example: for the boolean function "a or b", this function could return one of the following two HashMaps: {"a" -> true} or {"b" -> true}.

`pub fn to_expr(&self, f: BDDFunc) -> Expr<T>`

[src]

Convert the BDD to a minimized sum-of-products expression.

`pub fn to_dot(&self, f: BDDFunc) -> String`

[src]

Export BDD to `dot`

format (from the graphviz package) to enable visualization.

## Trait Implementations

`impl<T: Clone> Clone for BDD<T> where`

T: Clone + Debug + Eq + Ord + Hash,

[src]

T: Clone + Debug + Eq + Ord + Hash,

`fn clone(&self) -> BDD<T>`

[src]

Returns a copy of the value. Read more

`fn clone_from(&mut self, source: &Self)`

1.0.0[src]

Performs copy-assignment from `source`

. Read more

`impl<T: Debug> Debug for BDD<T> where`

T: Clone + Debug + Eq + Ord + Hash,

[src]

T: Clone + Debug + Eq + Ord + Hash,