Depgraph
A small library for working with dependency graphs.
This is just a small collection of basic graph algorithms for
working with dependency graphs.
Graph Representation
We represent dependency graphs as simple ACL2::alists that bind nodes
to the lists of nodes they (directly) depend on. For instance, a graph
like
A -----> B ---> C
| |
| |
v |
D <---+
Could be represented as:
((A . (B)) ; A only depends on B
(B . (C D)) ; B depends on C and D
(C . (D)) ; C only depends on D
(D . NIL)) ; D depends on nothing
Our algorithms treat graph as an alist, i.e., any "shadowed"
entries are ignored.
There are no restrictions on the kinds of nodes that a graph can contain.
However, our algorithms are generally based on ACL2::fast-alists, so for
good performance:
- It is helpful for the nodes to be ACL2::normed objects. (This isn't
strictly necessary; the nodes will be normed as needed.)
- It is helpful for graph to be a fast alist. (This isn't strictly
necessary; the graph will be made fast if needed.)
Subtopics
- Toposort
- General-purpose, depth-first topological sort for dependency graphs.
- Transdeps
- Compute the transitive dependencies for a list of nodes.
- Invert
- Invert a dependency graph.
- Mergesort-alist-values
- Sort all of the values bound in an alist.
- Alist-values-are-sets-p
- Recognizer for alists whose every value is an ordered set.
- Topologically-ordered-p
- (topologically-ordered-p nodes graph) determines if a list of nodes is
topologically ordered with respect to a graph.
- Dependency-chain-p
- (dependency-chain-p nodes graph) determines if a list of nodes indeed
follows a set of dependencies in graph.
