Struct biodivine_lib_bdd::BddNode
source · pub struct BddNode {
pub var: BddVariable,
pub low_link: BddPointer,
pub high_link: BddPointer,
}
Expand description
(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§
source§impl BddNode
impl BddNode
sourcepub fn mk_node(
var: BddVariable,
low_link: BddPointer,
high_link: BddPointer
) -> BddNode
pub fn mk_node( var: BddVariable, low_link: BddPointer, high_link: BddPointer ) -> BddNode
Make a new general node.
Assumptions:
low
andhigh
are pointers in the sameBdd
array.- Returned node will be added to the same
Bdd
wherelow
andhigh
are pointers.
Trait Implementations§
source§impl PartialEq for BddNode
impl PartialEq for BddNode
impl Copy for BddNode
impl Eq for BddNode
impl StructuralPartialEq for BddNode
Auto Trait Implementations§
impl Freeze for BddNode
impl RefUnwindSafe for BddNode
impl Send for BddNode
impl Sync for BddNode
impl Unpin for BddNode
impl UnwindSafe for BddNode
Blanket Implementations§
source§impl<T> BorrowMut<T> for Twhere
T: ?Sized,
impl<T> BorrowMut<T> for Twhere
T: ?Sized,
source§fn borrow_mut(&mut self) -> &mut T
fn borrow_mut(&mut self) -> &mut T
Mutably borrows from an owned value. Read more