Struct boolean_expression::BDD [−][src]
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]
impl<T> BDD<T> where
T: Clone + Debug + Eq + Ord + Hash,
pub fn new() -> BDD<T>
[src]
pub fn new() -> BDD<T>
Produce a new, empty, BDD.
pub fn terminal(&mut self, t: T) -> BDDFunc
[src]
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
[src]
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
[src]
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
[src]
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
[src]
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
[src]
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
[src]
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
[src]
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
[src]
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
[src]
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>>
[src]
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>
[src]
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
[src]
pub fn to_dot(&self, f: BDDFunc) -> String
Export BDD to dot
format (from the graphviz package) to enable visualization.
pub fn max_sat(&mut self, funcs: &[BDDFunc]) -> BDDFunc
[src]
pub fn max_sat(&mut self, funcs: &[BDDFunc]) -> BDDFunc
Produce a function that is true when the maximal number of given input functions are true.
pub fn labels(&self) -> Vec<T>
[src]
pub fn labels(&self) -> Vec<T>
Return a vector of all labels in the BDD.
Trait Implementations
impl<T: Clone> Clone for BDD<T> where
T: Clone + Debug + Eq + Ord + Hash,
[src]
impl<T: Clone> Clone for BDD<T> where
T: Clone + Debug + Eq + Ord + Hash,
fn clone(&self) -> BDD<T>
[src]
fn clone(&self) -> BDD<T>
Returns a copy of the value. Read more
fn clone_from(&mut self, source: &Self)
1.0.0[src]
fn clone_from(&mut self, source: &Self)
Performs copy-assignment from source
. Read more
impl<T: Debug> Debug for BDD<T> where
T: Clone + Debug + Eq + Ord + Hash,
[src]
impl<T: Debug> Debug for BDD<T> where
T: Clone + Debug + Eq + Ord + Hash,