[−][src]Struct boolean_expression::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.)
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.
Implementations
impl<T> BDD<T> where
T: Clone + Debug + Eq + Hash,
[src]
T: Clone + Debug + Eq + 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 ite(&mut self, i: BDDFunc, t: BDDFunc, e: BDDFunc) -> BDDFunc
[src]
Produce a function within the BDD representing the logical if-then-else
of the functions i
, t
, and e
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 xor(&mut self, a: BDDFunc, b: BDDFunc) -> BDDFunc
[src]
Produce a function within the BDD representing the logical XOR 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.
pub fn max_sat(&mut self, funcs: &[BDDFunc]) -> BDDFunc
[src]
Produce a function that is true when the maximal number of given input functions are true.
pub fn labels(&self) -> Vec<T>
[src]
Return a vector of all labels in the BDD.
Trait Implementations
impl<T: Clone> Clone for BDD<T> where
T: Clone + Debug + Eq + Hash,
[src]
T: Clone + Debug + Eq + Hash,
impl<T: Debug> Debug for BDD<T> where
T: Clone + Debug + Eq + Hash,
[src]
T: Clone + Debug + Eq + Hash,
Auto Trait Implementations
impl<T> RefUnwindSafe for BDD<T> where
T: RefUnwindSafe,
T: RefUnwindSafe,
impl<T> Send for BDD<T> where
T: Send,
T: Send,
impl<T> Sync for BDD<T> where
T: Sync,
T: Sync,
impl<T> Unpin for BDD<T> where
T: Unpin,
T: Unpin,
impl<T> UnwindSafe for BDD<T> where
T: UnwindSafe,
T: UnwindSafe,
Blanket Implementations
impl<T> Any for T where
T: 'static + ?Sized,
[src]
T: 'static + ?Sized,
impl<T> Borrow<T> for T where
T: ?Sized,
[src]
T: ?Sized,
impl<T> BorrowMut<T> for T where
T: ?Sized,
[src]
T: ?Sized,
fn borrow_mut(&mut self) -> &mut T
[src]
impl<T> From<T> for T
[src]
impl<T, U> Into<U> for T where
U: From<T>,
[src]
U: From<T>,
impl<T> ToOwned for T where
T: Clone,
[src]
T: Clone,
type Owned = T
The resulting type after obtaining ownership.
fn to_owned(&self) -> T
[src]
fn clone_into(&self, target: &mut T)
[src]
impl<T, U> TryFrom<U> for T where
U: Into<T>,
[src]
U: Into<T>,
type Error = Infallible
The type returned in the event of a conversion error.
fn try_from(value: U) -> Result<T, <T as TryFrom<U>>::Error>
[src]
impl<T, U> TryInto<U> for T where
U: TryFrom<T>,
[src]
U: TryFrom<T>,