		Search-engine friendly clone of the ACL2 documentation.

Depgraph

Dependency-chain-p

(dependency-chain-p nodes graph) determines if a list of nodes indeed follows a set of dependencies in graph.

Signature
(dependency-chain-p nodes graph) → depchain-p
Arguments: nodes — List of nodes to check.; graph — Alist that binds nodes to their dependents.

Say nodes is (n1 n2 ... nk). We check that n2 is a dependent of n1, n3 is a dependent of n2, and so forth. This is mainly used as a sanity check on any loops we claim to have found.

Definitions and Theorems

Function: dependency-chain-p

(defun dependency-chain-p (nodes graph)
  (declare (xargs :guard t))
  (let ((__function__ 'dependency-chain-p))
    (declare (ignorable __function__))
    (b* (((when (atom nodes)) t)
         ((when (atom (cdr nodes))) t)
         (node1 (first nodes))
         (node2 (second nodes))
         (deps1 (cdr (hons-get node1 graph))))
      (and (hons-member-equal node2 deps1)
           (dependency-chain-p (cdr nodes)
                               graph)))))