Struct BDDManager 

pub struct BDDManager {
    pub unique_table: HashMap<BDDNode, usize>,
    pub nodes: Vec<BDDNode>,
    pub apply_cache: HashMap<(u8, usize, usize), usize>,
}

A BDD manager: maintains a unique table and an apply cache.

Fields

unique_table: HashMap<BDDNode, usize>

Unique table: node → id.

nodes: Vec<BDDNode>

All allocated nodes (in order).

apply_cache: HashMap<(u8, usize, usize), usize>

Apply cache: (op, id1, id2) → id.

Implementations

impl BDDManager

pub fn new() -> Self

Create a new BDD manager.

pub fn false_node(&self) -> usize

Return the id of the constant-false BDD.

pub fn true_node(&self) -> usize

Return the id of the constant-true BDD.

pub fn var(&mut self, var: usize) -> usize

Create a variable node for var.

pub fn bdd_and(&mut self, a: usize, b: usize) -> usize

Compute the conjunction of two BDD nodes.

pub fn bdd_or(&mut self, a: usize, b: usize) -> usize

Compute the disjunction of two BDD nodes.

pub fn bdd_quantify_exists(&mut self, a: usize, var: usize) -> usize

Existentially quantify variable var out of BDD a.

Trait Implementations

impl Clone for BDDManager

fn clone(&self) -> BDDManager

Returns a duplicate of the value.

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

Performs copy-assignment from source.

impl Debug for BDDManager

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

Formats the value using the given formatter.

impl Default for BDDManager

fn default() -> Self

Returns the “default value” for a type.