		Search-engine friendly clone of the ACL2 documentation.

Depgraph

Invert

Invert a dependency graph.

Signature
(invert graph) → inverted-graph
Arguments: graph — Alist that binds nodes to the list of nodes they (directly) depend on.
Returns: inverted-graph — Fast alist that binds nodes to the list of nodes that (directly) depend on them.

See the discussion of graph representation in depgraph. This basically changes the directions of arrows in the graph. For instance, if our original graph was:

A ----->  B ---> C        ((A . (B))
          |      |         (B . (C D))
          |      |         (C . (D))
          v      |         (D . NIL))
          D <----+

Then inverting the graph just changes the directions of all the arrows, e.g., we would have:

A <-----  B <--- C        ((A . NIL)
          ^      ^         (B . (A))
          |      |         (C . (B))
          |      |         (D . (C B)))
          D -----+

We are careful to ensure that every node is bound in the resulting graph, e.g., we'll have a binding for A even though it is a leaf node.

Definitions and Theorems

Function: invert

(defun invert (graph)
 (declare (xargs :guard t))
 (let ((__function__ 'invert))
   (declare (ignorable __function__))
   (b* ((nodes (alist-keys graph))
        (acc (make-fast-alist (pairlis$ nodes nil)))
        (acc (with-fast-alist graph
                              (invert-outer-loop nodes graph acc))))
     (fast-alist-clean acc))))

Theorem: invert-correct

(defthm invert-correct
  (iff (member parent
               (cdr (hons-assoc-equal child (invert graph))))
       (member child
               (cdr (hons-assoc-equal parent graph)))))

Subtopics

Invert-outer-loop: Add all parent dependencies to all children.
Invert-inner-loop: Add a parent dependency to each of its children.