Skip to main content

Bdd

Trait Bdd 

Source
pub trait Bdd:
    Sized
    + Debug
    + PartialEq
    + Clone {
    // Required methods
    fn not(&self) -> Self;
    fn and(&self, rhs: &Self) -> Self;
    fn or(&self, rhs: &Self) -> Self;
    fn exists<'a, I: IntoIterator<Item = &'a Self>>(&'a self, vars: I) -> Self;
    fn satisfiable(&self) -> bool;
    fn implies(&self, rhs: &Self) -> Self;
    fn equiv(&self, rhs: &Self) -> Self;
    fn swap<'a, I: IntoIterator<Item = &'a Self>>(
        &'a self,
        from: I,
        to: I,
    ) -> Self;
}
Expand description

The BDD trait defines the interface for a binary decision diagram.

Required Methods§

Source

fn not(&self) -> Self

Negation of a BDD.

Source

fn and(&self, rhs: &Self) -> Self

Conjunction of two BDDs.

Source

fn or(&self, rhs: &Self) -> Self

Disjunction of two BDDs.

Source

fn exists<'a, I: IntoIterator<Item = &'a Self>>(&'a self, vars: I) -> Self

Existential quantification over a set of variables vars

Source

fn satisfiable(&self) -> bool

Check whether a satisfying assignment exists for the BDD.

Source

fn implies(&self, rhs: &Self) -> Self

Compute the implication of two BDDs, i.e., the bdd lhs => rhs.

Source

fn equiv(&self, rhs: &Self) -> Self

Compute the equivalence of two BDDs, i.e., the bdd lhs <=> rhs.

Source

fn swap<'a, I: IntoIterator<Item = &'a Self>>(&'a self, from: I, to: I) -> Self

Swap variables according to the permutation.

Dyn Compatibility§

This trait is not dyn compatible.

In older versions of Rust, dyn compatibility was called "object safety".

Implementors§