Trait Manager

pub unsafe trait Manager: Sized {
    type Edge: Edge<Tag = Self::EdgeTag>;
    type EdgeTag: Tag;
    type InnerNode: InnerNode<Self::Edge>;
    type Terminal: Eq + Hash;
    type TerminalRef<'a>: Borrow<Self::Terminal> + Copy
       where Self: 'a;
    type Rules: DiagramRules<Self::Edge, Self::InnerNode, Self::Terminal>;
    type TerminalIterator<'a>: Iterator<Item = Self::Edge>
       where Self: 'a;
    type NodeSet: NodeSet<Self::Edge>;
    type LevelView<'a>: LevelView<Self::Edge, Self::InnerNode>
       where Self: 'a;
    type LevelIterator<'a>: DoubleEndedIterator<Item = Self::LevelView<'a>> + ExactSizeIterator
       where Self: 'a;

    // Required methods
    fn get_node(&self, edge: &Self::Edge) -> Node<'_, Self>;
    fn clone_edge(&self, edge: &Self::Edge) -> Self::Edge;
    fn drop_edge(&self, edge: Self::Edge);
    fn num_inner_nodes(&self) -> usize;
    fn num_levels(&self) -> LevelNo;
    fn add_level(
        &mut self,
        f: impl FnOnce(LevelNo) -> Self::InnerNode,
    ) -> AllocResult<Self::Edge>;
    fn level(&self, no: LevelNo) -> Self::LevelView<'_>;
    fn levels(&self) -> Self::LevelIterator<'_>;
    fn get_terminal(&self, terminal: Self::Terminal) -> AllocResult<Self::Edge>;
    fn num_terminals(&self) -> usize;
    fn terminals(&self) -> Self::TerminalIterator<'_>;
    fn gc(&self) -> usize;
    fn reorder<T>(&mut self, f: impl FnOnce(&mut Self) -> T) -> T;
    fn gc_count(&self) -> u64;
    fn reorder_count(&self) -> u64;

    // Provided method
    fn approx_num_inner_nodes(&self) -> usize { ... }
}

Manager for nodes in a decision diagram

In the basic formulation, a decision diagram is a directed acyclic graph where all inner nodes are associated with a level, and each level in turn is associated with a variable. A decision diagram can represent functions Dⁿ → T, where n is the number of variables. Every inner node has |D| outgoing edges, pointing to child nodes. The semantics of an inner node depends on the value of its associated variable. If the variable has value d ∈ D, then the node’s semantics is the semantics of the child referenced by the edge corresponding to d. Every terminal node is associated with a value t ∈ T, and the node’s semantics is just that value t. Some kinds of decision diagrams deviate from this formulation in one way or the other, but still fit into the framework.

The manager’s responsibility is to store nodes and provide edges to identify them. Internally, it has a unique table to ensure uniqueness of nodes (typically, there should be no two nodes with the same children at the same level). The manager supports some kind of garbage collection: If there are no more edges pointing to a node, the node does not necessarily have to be deleted immediately. It may well be that the node revives. But from time to time it may make sense to remove all currently dead nodes. The manager also supports a levelized view on the diagram (via LevelViews).

Note that we are way more concerned about levels than about variables here. This is because variables can easily be handled externally. For many kinds of diagrams, we can just use the function representation of a variable and get the mapping between variables and levels “for free”. This is especially nice as there are reordering operations which change the mapping between levels and variables but implicitly update the function representations accordingly.

Safety

The implementation must ensure that every inner node only refers to nodes stored in this manager.

Every level view is associated with a manager and a level number. Manager::level() must always return the level view associated to this manager with the given level number.

If Manager::InnerNode implements HasLevel, then the implementation must ensure that HasLevel::level() returns level number L for all nodes at the level view for L. Specifically this means that Manager::add_level() must check the newly created node. The invariant may only be broken by unsafe code (e.g. via HasLevel::set_level() and LevelView::swap()) and must be re-established when leaving the unsafe scope (be aware of panics!).

Required Associated Types

type Edge: Edge<Tag = Self::EdgeTag>

Type of edge

type EdgeTag: Tag

Type of edge tags

type InnerNode: InnerNode<Self::Edge>

Type of inner nodes

type Terminal: Eq + Hash

Type of terminals

type TerminalRef<'a>: Borrow<Self::Terminal> + Copy where Self: 'a

References to Self::Terminals

Should either be a &'a Self::Terminal or just Self::Terminal. The latter is useful for “static terminal managers” which don’t actually store terminal nodes but can map between edges and terminal nodes on the fly. In this case, it would be hard to hand out node references.

type Rules: DiagramRules<Self::Edge, Self::InnerNode, Self::Terminal>

Diagram rules, see DiagramRules for more details

type TerminalIterator<'a>: Iterator<Item = Self::Edge> where Self: 'a

Iterator over all terminals

The actual items are edges pointing to terminals since this allows us to get a NodeID.

type NodeSet: NodeSet<Self::Edge>

Node set type, possibly more efficient than a HashSet<NodeID>

type LevelView<'a>: LevelView<Self::Edge, Self::InnerNode> where Self: 'a

A view on a single level of the unique table.

type LevelIterator<'a>: DoubleEndedIterator<Item = Self::LevelView<'a>> + ExactSizeIterator where Self: 'a

Iterator over levels

Required Methods

fn get_node(&self, edge: &Self::Edge) -> Node<'_, Self>

Get a reference to the node to which edge points

fn clone_edge(&self, edge: &Self::Edge) -> Self::Edge

Clone edge

fn drop_edge(&self, edge: Self::Edge)

Drop edge

fn num_inner_nodes(&self) -> usize

Get the count of inner nodes

fn num_levels(&self) -> LevelNo

Get the number of levels

fn add_level( &mut self, f: impl FnOnce(LevelNo) -> Self::InnerNode, ) -> AllocResult<Self::Edge>

Add a level with the given node to the unique table.

To avoid unnecessary (un-)locking, this function takes a closure f that creates a first node for the new level.

Returns an edge for the newly created node.

Panics if the new node’s level does not match the provided level.

fn level(&self, no: LevelNo) -> Self::LevelView<'_>

Get the level given by no

Implementations may or may not acquire a lock here.

Panics if no >= self.num_levels().

fn levels(&self) -> Self::LevelIterator<'_>

Iterate over the levels from top to bottom

fn get_terminal(&self, terminal: Self::Terminal) -> AllocResult<Self::Edge>

Get an edge for the given terminal

Locking behavior: May acquire a lock for the internal terminal unique table. In particular, this means that calling this function while holding a terminal iterator (Manager::terminals()) may cause a deadlock.

fn num_terminals(&self) -> usize

Get the number of terminals

Should agree with the length of the iterator returned by Manager::terminals().

Locking behavior: May acquire a lock for the internal terminal unique table. In particular, this means that calling this function while holding a terminal iterator (Manager::terminals()) may cause a deadlock.

fn terminals(&self) -> Self::TerminalIterator<'_>

Iterator over all terminals

Locking behavior: May acquire a lock for the internal terminal unique table.

fn gc(&self) -> usize

Perform garbage collection

This method looks for nodes that are neither referenced by a Function nor another node and removes them. The method works from top to bottom, so if a node is only referenced by nodes that can be removed, this node will be removed as well.

Returns the number of nodes removed.

fn reorder<T>(&mut self, f: impl FnOnce(&mut Self) -> T) -> T

Prepare and postprocess a reordering operation. The reordering itself is performed in f.

Returns the value returned by f.

fn gc_count(&self) -> u64

Get the count of garbage collections

This counter should monotonically increase to ensure that caches are invalidated accordingly.

fn reorder_count(&self) -> u64

Get the count of reordering operations

This counter should monotonically increase to ensure that caches are invalidated accordingly.

Provided Methods

fn approx_num_inner_nodes(&self) -> usize

Get an approximate count of inner nodes

For concurrent implementations, it may be much less costly to determine an approximation of the inner node count than an accurate count (Self::num_inner_nodes()).

Dyn Compatibility

This trait is not dyn compatible.

In older versions of Rust, dyn compatibility was called "object safety", so this trait is not object safe.

Implementors