Enum BDD 

pub enum BDD {
    CuDD(CuddDD),
    OxiDD(OxiDD),
}

Common representation of a binary decision diagram (BDD)

This enum defines a variant for each library that can be used. Note that combining BDDs of different libraries and managers will generally result in panics.

Currently, the supported BDD libraries are:

• CUDD
• OxiDD

Variants

CuDD(CuddDD)

A CUDD BDD

OxiDD(OxiDD)

An OxiDD BDD

Trait Implementations

impl Bdd for BDD

fn not(&self) -> Self

Negation of a BDD.

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

Conjunction of two BDDs.

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

Disjunction of two BDDs.

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

Existential quantification over a set of variables vars

fn satisfiable(&self) -> bool

Check whether a satisfying assignment exists for the BDD.

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

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

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

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

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

Swap variables according to the permutation.

impl BitAnd for &BDD

type Output = BDD

The resulting type after applying the & operator.

fn bitand(self, rhs: Self) -> BDD

Performs the & operation.

impl BitAnd for BDD

type Output = BDD

The resulting type after applying the & operator.

fn bitand(self, rhs: Self) -> BDD

Performs the & operation.

impl BitAndAssign for BDD

fn bitand_assign(&mut self, rhs: Self)

Performs the &= operation.

impl BitOr for &BDD

type Output = BDD

The resulting type after applying the | operator.

fn bitor(self, rhs: Self) -> BDD

Performs the | operation.

impl BitOr for BDD

type Output = BDD

The resulting type after applying the | operator.

fn bitor(self, rhs: Self) -> BDD

Performs the | operation.

impl BitOrAssign for BDD

fn bitor_assign(&mut self, rhs: Self)

Performs the |= operation.

impl Clone for BDD

fn clone(&self) -> BDD

Returns a duplicate of the value.

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

Performs copy-assignment from source.

impl Debug for BDD

fn fmt(&self, f: &mut Formatter<'_>) -> Result

Formats the value using the given formatter.

impl Not for &BDD

type Output = BDD

The resulting type after applying the ! operator.

fn not(self) -> BDD

Performs the unary ! operation.

impl Not for BDD

type Output = BDD

The resulting type after applying the ! operator.

fn not(self) -> BDD

Performs the unary ! operation.

impl PartialEq for BDD

fn eq(&self, other: &BDD) -> bool

Tests for self and other values to be equal, and is used by ==.

fn ne(&self, other: &Rhs) -> bool

Tests for !=. The default implementation is almost always sufficient, and should not be overridden without very good reason.

impl StructuralPartialEq for BDD