Struct BddManager 

pub struct BddManager { /* private fields */ }

A Binary Decision Diagram manager. Maintains a unique table to ensure node sharing and canonical representation.

Implementations

impl BddManager

pub fn new() -> Self

Creates a new BDD manager.

pub fn constant_false(&self) -> NodeId

Returns the FALSE constant.

pub fn constant_true(&self) -> NodeId

Returns the TRUE constant.

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

Creates a BDD for a single variable.

pub fn not(&mut self, node: NodeId) -> NodeId

Negates a BDD node.

Runs on an explicit work-stack with a computed table (not_cache), rather than the tree recursion this replaces. Two defects are fixed:

• The recursion had no computed table, so every shared node was re-expanded. not on a 40-variable parity BDD — O(n) nodes, 2ⁿ tree unfoldings — never returned.
• Recursion depth was the BDD height, i.e. the variable count, with no guard. The return type is NodeId, so a depth cap could only have produced a silently wrong diagram.

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

Computes the AND of two BDD nodes.

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

Computes the OR of two BDD nodes.

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

Computes the XOR of two BDD nodes.

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

Computes the implication: left => right (equivalent to !left | right)

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

Computes the equivalence: left <=> right

pub fn ite( &mut self, cond: NodeId, then_node: NodeId, else_node: NodeId, ) -> NodeId

If-then-else operation: if cond then then_node else else_node.

Runs on an explicit work-stack with the standard ITE computed table keyed on the (cond, then, else) triple. The recursion this replaces had neither: with triple fan-out and no memo, shared cofactors of the hash-consed diagram were re-expanded exponentially, and the depth was the (unguarded) variable count. NodeId has no error channel, so a depth cap could only have returned a silently wrong diagram.

pub fn eval(&self, node: NodeId, assignment: &FxHashMap<VarId, bool>) -> bool

Evaluates a BDD with a given variable assignment.

pub fn sat_count(&self, node: NodeId, num_vars: u32) -> u64

Counts the number of satisfying assignments for a BDD.

pub fn node_count(&self) -> usize

Returns the number of nodes in the manager.

pub fn clear_cache(&mut self)

Clears the operation caches (useful for memory management).

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.

impl Display for BddManager

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

Formats the value using the given formatter.