		Search-engine friendly clone of the ACL2 documentation.

Invert

Invert-inner-loop

Add a parent dependency to each of its children.

Signature
(invert-inner-loop parent children acc) → acc
Arguments: parent — A node in the original graph.; children — List of nodes that parent depends on, in the original graph.; acc — New, inverted graph we are building. Fast alist.
Returns: acc — Extended by adding parent as a dependency of each child.

Definitions and Theorems

Function: invert-inner-loop

(defun invert-inner-loop (parent children acc)
  (declare (xargs :guard t))
  (let ((__function__ 'invert-inner-loop))
    (declare (ignorable __function__))
    (b* (((when (atom children)) acc)
         (child1 (car children))
         (curr-parents (cdr (hons-get child1 acc)))
         (new-parents (cons parent curr-parents))
         (acc (hons-acons child1 new-parents acc)))
      (invert-inner-loop parent (cdr children)
                         acc))))

Theorem: invert-inner-loop-correct

(defthm invert-inner-loop-correct
 (iff
    (member
         par
         (cdr (hons-assoc-equal
                   child
                   (invert-inner-loop parent children orig-alist))))
    (or (member par
                (cdr (hons-assoc-equal child orig-alist)))
        (and (equal par parent)
             (member child children)))))