		Search-engine friendly clone of the ACL2 documentation.

Depgraph

Topologically-ordered-p

(topologically-ordered-p nodes graph) determines if a list of nodes is topologically ordered with respect to a graph.

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

We check that, for every node a in the list of nodes, the dependents of a come before a.

This is a weak check in a couple of ways: we don't require that the nodes are unique, and we don't check that every node in the graph is among the nodes.

We can determine if the nodes are topologically sorted in linear time, assuming constant-time hashing.

Definitions and Theorems

Function: topologically-ordered-p

(defun topologically-ordered-p (nodes graph)
  (declare (xargs :guard t))
  (let ((__function__ 'topologically-ordered-p))
    (declare (ignorable __function__))
    (b* ((seen (len nodes))
         ((mv ans seen)
          (topologically-ordered-p-aux nodes graph seen)))
      (fast-alist-free seen)
      ans)))

Subtopics

Topologically-ordered-p-aux