		Search-engine friendly clone of the ACL2 documentation.

Toposort

Extract-topological-order

Extract the topological order from successful applications of toposort-aux.

Signature
(extract-topological-order seen acc) → nodelist
Arguments: seen — Guard (cons-listp seen).

Definitions and Theorems

Function: extract-topological-order

(defun extract-topological-order (seen acc)
  (declare (xargs :guard (cons-listp seen)))
  (let ((__function__ 'extract-topological-order))
    (declare (ignorable __function__))
    (cond ((atom seen) acc)
          ((eq (cdar seen) :finished)
           (extract-topological-order (cdr seen)
                                      (cons (caar seen) acc)))
          (t (extract-topological-order (cdr seen)
                                        acc)))))

Theorem: true-listp-of-extract-topological-order

(defthm true-listp-of-extract-topological-order
  (implies (true-listp acc)
           (true-listp (extract-topological-order seen acc))))

Theorem: subsetp-equal-of-extract-topological-order

(defthm subsetp-equal-of-extract-topological-order
  (subsetp-equal (extract-topological-order seen acc)
                 (append (alist-keys seen) acc)))

Now we prove a completeness theorem that shows extract-topological-order will get us at least everything that was in the queue.

Theorem: extract-topological-order-includes-queue

(defthm extract-topological-order-includes-queue
 (implies
      (and (mv-nth 0 (toposort-aux queue seen graph))
           (subsetp-equal queue (alist-keys graph)))
      (subsetp-equal queue
                     (extract-topological-order
                          (mv-nth 1 (toposort-aux queue seen graph))
                          nil))))

And a uniqueness theorem that shows the extracted elements are at least duplicate-free.

Theorem: no-duplicatesp-equal-of-extract-topological-order

(defthm no-duplicatesp-equal-of-extract-topological-order
  (implies
       (no-duplicatesp-equal (extract-topological-order seen nil))
       (no-duplicatesp-equal
            (extract-topological-order
                 (mv-nth 1 (toposort-aux queue seen graph))
                 nil))))