Trait HasLevel

pub unsafe trait HasLevel {
    // Required methods
    fn level(&self) -> LevelNo;
    unsafe fn set_level(&self, level: LevelNo);
}

Trait for nodes that have a level

Quasi-reduced BDDs, for instance, do not need the level information stored in their nodes, so there is no need to implement this trait.

Implementors should also implement InnerNode. If Self is Sync, then the level number should be implemented using AtomicLevelNo. In particular, concurrent calls to Self::level() and Self::set_level() must not lead to data races.

Safety

1. A node in a LevelView with level number L has level number L (i.e. self.level() returns L).
2. InnerNode::check_level() with a check c must return c(self.level()). Similarly, InnerNode::assert_level_matches() must panic if the level does not match.

These conditions are crucial to enable concurrent level swaps as part of reordering (see the oxidd-reorder crate): The algorithm iterates over the nodes at the upper level and needs to know whether a node is part of the level directly below it. The procedure only has access to nodes at these two levels, hence it must rely on the level information for SAFETY.

Note that invariant 1 may be broken by HasLevel::set_level() and LevelView::swap(); the caller of these functions is responsible to re-establish the invariant.

Required Methods

fn level(&self) -> LevelNo

Get the node’s level

unsafe fn set_level(&self, level: LevelNo)

Set the node’s level

Safety

This method may break SAFETY invariant 1 of the HasLevel trait: A node in a LevelView with level number L has level number L (i.e. self.level() returns L). The caller is responsible to re-establish the invariant. (Make sure that the calling code is exception-safe!)

Implementors