		Search-engine friendly clone of the ACL2 documentation.

Toposort

Toposort-aux

Main depth-first topological sorting routine.

Signature
(toposort-aux queue seen graph) → (mv successp seen)
Arguments: queue — All the nodes we have left to explore. Initially this is just (alist-keys graph.; seen — Fast alist that binds nodes to their status (see below).; graph — Fast alist that binds nodes to the lists of their dependents. Remains constant as we recur.
Returns: successp — We return successfully only if we're able to explore all of the nodes in the queue without finding a loop.; seen — Final seen fast alist, from which we can extract the topological order or a loop.

The status of each node is either:

unbound, if we haven't started it yet, or bound to
:started if we are currently exploring its dependents, or
:finished if we are done exploring it.

On success, a topologically sorted list of nodes can be extracted from seen by looking at the :finished nodes using extract-topological-order. On failure, the loop we found can be extracted from seen by looking at the :started nodes with extract-topological-loop.

Definitions and Theorems

Function: toposort-aux

(defun toposort-aux (queue seen graph)
 (declare (xargs :guard t))
 (let ((__function__ 'toposort-aux))
  (declare (ignorable __function__))
  (b*
   (((when (atom queue)) (mv t seen))
    (orig-seen-al seen)
    (node (car queue))
    (status (hons-get node seen))
    ((when (eq (cdr status) :finished))
     (toposort-aux (cdr queue) seen graph))
    ((when status)
     (mv nil (hons-acons node :started seen)))
    (deps-look (hons-get node graph))
    ((unless deps-look)
     (er hard? 'toposort-aux
         "No binding for ~x0." node)
     (toposort-aux (cdr queue) seen graph))
    (seen (hons-acons node :started seen))
    (deps (cdr deps-look))
    ((mv deps-okp seen)
     (toposort-aux deps seen graph))
    ((unless deps-okp) (mv nil seen))
    (seen (hons-acons node :finished seen))
    ((unless (mbt (o< (toposort-measure (cdr queue)
                                        seen graph)
                      (toposort-measure queue orig-seen-al graph))))
     (mv nil seen)))
   (toposort-aux (cdr queue) seen graph))))

Theorem: cons-listp-of-toposort-aux

(defthm cons-listp-of-toposort-aux
  (implies (cons-listp seen)
           (cons-listp (mv-nth 1 (toposort-aux queue seen graph)))))

Theorem: subsetp-equal-of-alist-keys-of-toposort-aux

(defthm subsetp-equal-of-alist-keys-of-toposort-aux
  (implies
       (subsetp-equal (alist-keys seen)
                      (alist-keys graph))
       (subsetp-equal
            (alist-keys (mv-nth 1 (toposort-aux queue seen graph)))
            (alist-keys graph))))

Theorem: toposort-aux-consp-on-failure

(defthm toposort-aux-consp-on-failure
  (implies (not (mv-nth 0 (toposort-aux queue seen graph)))
           (consp (mv-nth 1 (toposort-aux queue seen graph)))))