Struct biodivine_lib_bdd::BddNode

pub(crate) struct BddNode {
    pub var: BddVariable,
    pub low_link: BddPointer,
    pub high_link: BddPointer,
}

(internal) Representation of individual vertices of the Bdd directed acyclic graph.

A BddNode can be a terminal, in which case it is either 0 or 1, or a decision node, in which case it contains a variable $v_i$ which it conditions upon and two pointers (low and high) to other nodes in the same Bdd:

graph LR
    id1($v_i$)
    id2($v_j$)
    id3($v_k$)
    id1 -->|low| id2
    id1 -->|high| id3

Internally, we represent terminal nodes using the same structure, giving them cyclic pointers. Instead of variable id, we use the number of variables in the original BddVariableSet. This is consistent with the fact that we first condition on smallest variable ids. It can be also used for consistency checks inside the library.

Fields

var: BddVariable

low_link: BddPointer

high_link: BddPointer

Implementations

impl BddNode

pub fn mk_zero(num_vars: u16) -> BddNode

Make a new terminal zero node.

pub fn mk_one(num_vars: u16) -> BddNode

Make a new terminal one node.

pub fn mk_node(
    var: BddVariable,
    low_link: BddPointer,
    high_link: BddPointer
) -> BddNode

Make a new general node.

Assumptions:

• low and high are pointers in the same Bdd array.
• Returned node will be added to the same Bdd where low and high are pointers.

Trait Implementations

impl Clone for BddNode

pub fn clone(&self) -> BddNode

Returns a copy of the value.

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

Performs copy-assignment from source.

impl Copy for BddNode

impl Debug for BddNode

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

Formats the value using the given formatter.

impl Eq for BddNode

impl Hash for BddNode

pub fn hash<__H: Hasher>(&self, state: &mut __H)

Feeds this value into the given Hasher.

pub fn hash_slice<H>(data: &[Self], state: &mut H) where
    H: Hasher, 

Feeds a slice of this type into the given Hasher.

impl PartialEq<BddNode> for BddNode

pub fn eq(&self, other: &BddNode) -> bool

This method tests for self and other values to be equal, and is used by ==.

pub fn ne(&self, other: &BddNode) -> bool

This method tests for !=.

impl StructuralEq for BddNode

impl StructuralPartialEq for BddNode