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.

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

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 cache (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.