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§
Sourcefn exists<'a, I: IntoIterator<Item = &'a Self>>(&'a self, vars: I) -> Self
fn exists<'a, I: IntoIterator<Item = &'a Self>>(&'a self, vars: I) -> Self
Existential quantification over a set of variables vars
Sourcefn satisfiable(&self) -> bool
fn satisfiable(&self) -> bool
Check whether a satisfying assignment exists for the BDD.
Sourcefn implies(&self, rhs: &Self) -> Self
fn implies(&self, rhs: &Self) -> Self
Compute the implication of two BDDs, i.e., the bdd lhs => rhs.
Sourcefn equiv(&self, rhs: &Self) -> Self
fn equiv(&self, rhs: &Self) -> Self
Compute the equivalence of two BDDs, i.e., the bdd lhs <=> rhs.
Sourcefn swap<'a, I: IntoIterator<Item = &'a Self>>(&'a self, from: I, to: I) -> Self
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".