Struct ZddManager 

pub struct ZddManager { /* private fields */ }

Zero-suppressed Binary Decision Diagram (ZDD) manager. ZDDs use a different reduction rule optimized for sparse sets:

• Eliminate node if high == 0 (instead of low == high for BDDs)

ZDDs are particularly efficient for representing:

• Sparse sets and families of sets
• Combinatorial structures
• Paths in graphs

Implementations

impl ZddManager

pub fn new() -> Self

Creates a new ZDD manager.

pub fn empty(&self) -> NodeId

Returns the empty set.

pub fn base(&self) -> NodeId

Returns the base set (set containing only the empty set).

pub fn singleton(&mut self, var: VarId) -> NodeId

Creates a ZDD for a singleton set containing just one variable.

pub fn union(&mut self, left: NodeId, right: NodeId) -> NodeId

Computes the union of two ZDD sets.

pub fn intersection(&mut self, left: NodeId, right: NodeId) -> NodeId

Computes the intersection of two ZDD sets.

pub fn difference(&mut self, left: NodeId, right: NodeId) -> NodeId

Computes the set difference: left \ right

pub fn count(&self, node: NodeId) -> u64

Returns the number of sets in the family represented by this ZDD.

pub fn node_count(&self) -> usize

Returns the number of nodes in the manager.

pub fn clear_cache(&mut self)

Clears the operation cache.

Trait Implementations

impl Clone for ZddManager

fn clone(&self) -> ZddManager

Returns a duplicate of the value.

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

Performs copy-assignment from source.

impl Debug for ZddManager

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

Formats the value using the given formatter.

impl Default for ZddManager

fn default() -> Self

Returns the “default value” for a type.

impl Display for ZddManager

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

Formats the value using the given formatter.