		Search-engine friendly clone of the ACL2 documentation.

Toposort

Extract-topological-loop

Extract the topological loop from failed applications of toposort-aux.

Signature
(extract-topological-loop seen stop acc full-seen) → final-acc
Arguments: seen — A copy of the seen alist that we're recurring through.
Guard (cons-listp seen).; stop — The node that we looped back to, so we know when to stop (and won't include nodes that we were exploring before getting to the looping node, i.e., the "handle" of a "lasso").; acc — Accumulator for nodes that really are in the loop.; full-seen — Fast copy of the full seen alist so we can tell if nodes were finished or not.
Returns: final-acc — List of all the nodes in the loop.

Definitions and Theorems

Function: extract-topological-loop

(defun extract-topological-loop (seen stop acc full-seen)
  (declare (xargs :guard (cons-listp seen)))
  (let ((__function__ 'extract-topological-loop))
    (declare (ignorable __function__))
    (cond ((atom seen)
           (prog2$ (er hard? 'extract-topological-loop
                       "Should never hit the end of seen!")
                   acc))
          ((eq (cdar seen) :started)
           (b* ((name (caar seen))
                (finishedp (eq (cdr (hons-get name full-seen))
                               :finished))
                (acc (if finishedp acc (cons name acc))))
             (if (hons-equal name stop)
                 acc
               (extract-topological-loop (cdr seen)
                                         stop acc full-seen))))
          (t (extract-topological-loop (cdr seen)
                                       stop acc full-seen)))))

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

(defthm true-listp-of-extract-topological-loop
 (implies
   (true-listp acc)
   (true-listp (extract-topological-loop seen stop acc full-seen))))

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

(defthm subsetp-equal-of-extract-topological-loop
  (subsetp-equal (extract-topological-loop seen stop acc full-seen)
                 (append (alist-keys seen) acc)))