Expand description
§Overview
A library to create and manipulate so called list decision diagrams, abbreviated as LDDs. List decision diagrams are data structures that can efficiently represent sets of vectors containing natural numbers [Dijk18].
An LDD is inductively defined as follows. First of all, constants ‘true’ and ‘false’ are two distinct LDDs. Given LDDs x and y, then node(value, x, y) is an LDD; where value is a natural number. As such, we observe that node(5, true, node(4, true, false)) is an LDD and in general we obtain a tree-like data structure.
Next, we should explain how LDDs represent a set of vectors. Given an LDD n then [n] is inductively defined as:
[false] = ∅
[true] = { <> }
[node(value, down, right)] = { value x | x in [down] } ∪ [right]\Note that since ‘true’ and ‘false’ are not very insightful and clash with Rust keywords we use ‘empty vector’ and ‘empty set’ for the constants ‘true’ and ‘false’ respectively.
§Citations
[Dijk18] — Tom van Dijk, Jaco van de Pol. Sylvan: multi-core framework for decision diagrams. International Journal on Software Tools for Technology Transfer. 19(6):675-696, 2017.
§Safety
This crate contains no unsafe code.
§Minimum Supported Rust Version
We do not maintain an official minimum supported rust version (MSRV), and it may be upgraded at any time when necessary.
§License
All MERC crates are licensed under the BSL-1.0 license. See the LICENSE file in the repository root for more information.
Modules§
Structs§
- Binary
LddReader - Binary
LddWriter - \brief Writes ldds in a streamable binary format to an output stream.
- Cache
- Implements an associative mapping between key value pairs, but has a limit on the maximum amount of elements stored. The cache requires that default values of K are never used in calls to get and insert, because these are used to indicate empty cache entries.
- Data
- This is the user facing data of a Node.
- DataRef
- This is the user facing data of a Node as references.
- Ldd
- Every Ldd points to its root node in the Storage instance for maximal sharing. These Ldd instances can only be created from the storage.
- LddDisplay
- Helper struct for displaying LDDs.
- LddDot
- Helper struct for displaying LDDs in DOT format.
- LddRef
- The LddRef is a reference to an existing Ldd instance. This can be used to avoid explicit protections that are performed when creating an Ldd instance.
- Node
- This is the LDD node(value, down, right) with some additional meta data.
- Operation
Cache - The operation cache can significantly speed up operations by caching intermediate results. This is necessary since the maximal sharing means that the same inputs can be encountered many times while evaluating the operation.
- Storage
- The storage that implements the maximal sharing behaviour. Meaning that identical nodes (same value, down and right) have a unique index in the node table. Therefore guaranteeing that Ldds n and m are identical iff their indices in the node table match.
- Sylvan
Reader - A reader for LDDs in the Sylvan .ldd format.
Enums§
- Binary
Operator - Any operator from LDD x LDD -> LDD.
- Ternary
Operator - Any operator from LDD x LDD x LDD -> LDD.
- Unary
Function - Any function from LDD -> usize.
Functions§
- append
- Appends the given value to every vector in the set represented by the given ldd.
- cache_
binary_ op - Implements an operation cache for a binary LDD operator.
- cache_
comm_ binary_ op - Implements an operation cache for a commutative binary LDD operator, i.e., an operator f such that f(a,b) = f(b,a) for all LDD a and b.
- cache_
terniary_ op - Implements an operation cache for a terniary LDD operator.
- cache_
unary_ function - Implements an operation cache for a unary LDD operator.
- compute_
meta - Computes a meta LDD from the given read and write projections that is suitable for relational_product.
- compute_
proj - Computes a meta LDD that is suitable for the project function from the given projection indices.
- element_
of - Returns true iff the set contains the vector.
- from_
iter - Returns an LDD containing all elements of the given iterator over vectors.
- height
- Returns the height of the LDD tree.
- len
- Returns the number of elements in the set.
- merge
- Interleave the vectors of two equal height ldds.
- minus
- Returns the largest subset of ‘a’ that does not contains elements of ‘b’, i.e., set difference.
- print_
differences - Prints the differences in contained vectors between two LDDs.
- print_
left - Prints vectors included in left, but not in right. Returns true iff the difference is non-empty.
- project
- Computes the set of vectors projected onto the given indices, where proj is equal to compute_proj([i_0, …, i_k]).
- project_
vector - Returns project(vector, proj), see project. Requires proj to be sorted.
- random_
sorted_ vector - Returns a sorted vector of the given length with unique u64 values (from 0..max_value).
- random_
vector - Returns a vector of the given length with random u64 values (from 0..max_value).
- random_
vector_ set - Returns a set of ‘amount’ vectors where every vector has the given length.
- read_
u32 - Returns a single u32 read from the given stream.
- read_
u64 - Returns a single u64 read from the given stream.
- relational_
product - Computes the set of vectors reachable in one step from the given set as defined by the sparse relation rel. Requires that meta = compute_meta(read_proj, write_proj).
- singleton
- Returns an LDD containing only the given vector, i.e., { vector }.
- union
- Returns the union of the given LDDs, i.e., a ∪ b.