		Search-engine friendly clone of the ACL2 documentation.

Depgraph

Transdeps

Compute the transitive dependencies for a list of nodes.

Signature
(transdeps nodes graph) → deps
Arguments: nodes — The list of nodes to compute dependencies for.; graph — Alist that binds nodes to the lists of nodes they (directly) depend on. See below.
Returns: deps — The ordered set of nodes that nodes depend on. Always includes nodes themselves.
Type (true-listp deps).

We implement a general-purpose, transitive closure operation for dependency graph reachability. We determine all nodes in the graph that are reachable from the starting nodes.

After calling this function you may wish to use transdeps-free to clear out the relevant memo tables.

Definitions and Theorems

Function: transdeps

(defun transdeps (nodes graph)
  (declare (xargs :guard t))
  (let ((__function__ 'transdeps))
    (declare (ignorable __function__))
    (let ((orig (mergesort nodes)))
      (with-fast-alist graph
                       (transdeps-aux orig nil orig graph)))))

Theorem: true-listp-of-transdeps

(defthm true-listp-of-transdeps
  (b* ((deps (transdeps nodes graph)))
    (true-listp deps))
  :rule-classes :rewrite)

Theorem: setp-of-transdeps

(defthm setp-of-transdeps
  (b* ((deps (transdeps nodes graph)))
    (setp deps))
  :rule-classes :rewrite)

Theorem: transdeps-subset

(defthm transdeps-subset
  (subset (transdeps nodes graph)
          (union (mergesort nodes)
                 (transdeps-allnodes graph))))

Subtopics

Transdeps-aux: Main algorithm for collecting transitive dependencies.
Transdeps-direct-for-nodes: Get the set of direct dependencies for a set of nodes.
Transdeps-direct-for-node: Memoized. Get the set of dependencies for a single node.
Transdeps-allnodes: Overapproximation of all of the nodes in the graph.
Transdeps-free: Free memo tables associated with transdeps.