Struct boolean_expression::BDD

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, 

pub fn new() -> BDD<T>

Produce a new, empty, BDD.

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

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

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

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

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

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

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

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

Produce a function within the BDD representing the logical implication a -> b.

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

Check whether the function f within the BDD is satisfiable.

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

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

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

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

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>

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

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

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, 

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

Returns a copy of the value.

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

Performs copy-assignment from source.

impl<T: Debug> Debug for BDD<T> where
    T: Clone + Debug + Eq + Ord + Hash, 

fn fmt(&self, __arg_0: &mut Formatter) -> Result

Formats the value using the given formatter.