Struct biodivine_lib_bdd::BddNode

pub 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.

impl BddNode

pub fn is_terminal(&self) -> bool

Check whether this node is effectively terminal.

Warning: This does not mean the node is necessarily terminal, it might also just point to a terminal node, effectively gaining its value. However, this should not happen in minimized BDDs.

pub fn is_one(&self) -> bool

Check whether this node is effectively one.

pub fn is_zero(&self) -> bool

Check whether this node is effectively zero.

Trait Implementations

impl Clone for BddNode

fn clone(&self) -> BddNode

Returns a copy of the value.

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

Performs copy-assignment from source.

impl Debug for BddNode

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

Formats the value using the given formatter.

impl Hash for BddNode

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

Feeds this value into the given Hasher.

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

where H: Hasher, Self: Sized,

Feeds a slice of this type into the given Hasher.

impl PartialEq for BddNode

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

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

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

This method tests for !=. The default implementation is almost always sufficient, and should not be overridden without very good reason.

impl Copy for BddNode

impl Eq for BddNode

impl StructuralPartialEq for BddNode