		Search-engine friendly clone of the ACL2 documentation.

Depgraph

Toposort

General-purpose, depth-first topological sort for dependency graphs.

Signature
(toposort graph) → (mv successp result)
Arguments: graph — Alist that binds nodes to the lists of nodes they (directly) depend on. See below.
Returns: successp — True when the graph is loop-free and hence can be topologically sorted, or nil when there is a loop.
Type (booleanp successp).; result — On success: a list of nodes in topological order, guaranteed equivalent to (alist-keys graph) and in dependency order. On failure: a list of nodes that have a dependency loop.
Type (true-listp result).

We implement a depth-first topological sort of the graph. If the graph is loop-free, this produces (mv t nodes), where nodes are set equivalent to (alist-keys graph) and are in dependency order. Otherwise the graph has loops; we will find some loop and return (mv nil loop), where loop is a list of nodes such as (a b c a), where a depends on b, which depends on c, which depends on a.

The graph is as described in depgraph, but note:

graph is expected to be complete, i.e., every node that is ever listed as a dependent should be bound in graph; we will cause a hard error if this is not the case.
graph should (typically) not contain nodes that depend on themselves; any such nodes form trivial self-loops and will cause topological ordering to fail.

Usage Notes

In rare cases you may actually be able to directly use this to sort some structures in a dependency order. But most of the time, we imagine that you will need to:

Extract a dependency graph in the expected "toposort format",
Run toposort to get a topological ordering (or find a loop), and finally
Reorder your data according to the ordering that has been produced.

It might sometimes be more efficient to write custom topological sorts for various data structures. But that's a lot of work. We think that the translation steps are usually cheap enough that in most cases, the above strategy is the easiest way to topologically sort your data.

Definitions and Theorems

Function: toposort

(defun toposort (graph)
  (declare (xargs :guard t))
  (let ((__function__ 'toposort))
    (declare (ignorable __function__))
    (b* (((with-fast graph))
         (keys (alist-keys graph))
         ((mv successp seen)
          (toposort-aux keys (len keys) graph))
         ((unless successp)
          (b* ((loop (extract-topological-loop (cdr seen)
                                               (caar seen)
                                               (list (caar seen))
                                               seen)))
            (fast-alist-free seen)
            (or (dependency-chain-p loop graph)
                (er hard? 'toposort
                    "failed to produce a valid dependency chain!"))
            (or (hons-equal (car loop)
                            (car (last loop)))
                (er hard? 'toposort
                    "failed to produce a loop!"))
            (mv nil loop)))
         (nodes (extract-topological-order seen nil)))
      (fast-alist-free seen)
      (or (topologically-ordered-p nodes graph)
          (er hard? 'toposort
              "failed to produce a topological ordering!"))
      (mv t nodes))))

Theorem: booleanp-of-toposort.successp

(defthm booleanp-of-toposort.successp
  (b* (((mv ?successp ?result)
        (toposort graph)))
    (booleanp successp))
  :rule-classes :type-prescription)

Theorem: true-listp-of-toposort.result

(defthm true-listp-of-toposort.result
  (b* (((mv ?successp ?result)
        (toposort graph)))
    (true-listp result))
  :rule-classes :type-prescription)

We always know, regardless of success, that the nodes we return in our ordering or in our loop must be members of the graph:

Theorem: subsetp-equal-of-toposort

(defthm subsetp-equal-of-toposort
  (subsetp-equal (mv-nth 1 (toposort graph))
                 (alist-keys graph)))

On success, we know something even better, namely that our ordering contains all of the nodes of the graph:

Theorem: toposort-set-equiv

(defthm toposort-set-equiv
  (implies (mv-nth 0 (toposort graph))
           (set-equiv (mv-nth 1 (toposort graph))
                      (alist-keys graph))))

And incidentally, on success, our ordering contains no duplicates:

Theorem: no-duplicatesp-equal-of-toposort

(defthm no-duplicatesp-equal-of-toposort
  (implies (mv-nth 0 (toposort graph))
           (no-duplicatesp-equal (mv-nth 1 (toposort graph)))))

Subtopics

Toposort-aux: Main depth-first topological sorting routine.
Extract-topological-loop: Extract the topological loop from failed applications of toposort-aux.
Extract-topological-order: Extract the topological order from successful applications of toposort-aux.