		Search-engine friendly clone of the ACL2 documentation.

Transdeps

Transdeps-aux

Main algorithm for collecting transitive dependencies.

Signature
(transdeps-aux curr prev orig graph) → deps
Arguments: curr — Nodes we're currently exploring.
Guard (setp curr).; prev — Nodes we've previously explored.
Guard (setp prev).; orig — Nodes that we were originally looking for.
Guard (setp orig).
Returns: deps — Type (setp deps).

We are trying to compute the set of all nodes that are necessary for curr and prev. At each step, we assume that all of prev's dependencies are already found within (curr U prev), so we are really only looking for "new" dependencies of the nodes in curr. If all of these new are already in curr U prev, we have reached a fixed point and we can stop. Otherwise, we need to explore these new dependencies, but we can expand prev with everything in curr so we know not to look there anymore.

The list of orig nodes is a termination hack of sorts. Without this, we would need to do something to ensure that the curr/prev lists don't contain nodes that aren't found anywhere in the graph. By also knowing what the original nodes were, we can include them in the measure.

Definitions and Theorems

Function: transdeps-aux

(defun transdeps-aux (curr prev orig graph)
 (declare (xargs :guard (and (setp curr)
                             (setp prev)
                             (setp orig))))
 (declare
  (xargs
     :guard (and (subset curr
                         (union orig (transdeps-allnodes graph)))
                 (subset prev
                         (union orig (transdeps-allnodes graph))))))
 (let ((__function__ 'transdeps-aux))
  (declare (ignorable __function__))
  (b*
   ((new (transdeps-direct-for-nodes curr graph))
    (curr+prev (union curr prev))
    ((unless (mbt (subset curr+prev
                          (union orig (transdeps-allnodes graph)))))
     curr+prev)
    ((when (subset new curr+prev))
     curr+prev))
   (transdeps-aux (difference new curr+prev)
                  curr+prev orig graph))))

Theorem: setp-of-transdeps-aux

(defthm setp-of-transdeps-aux
  (b* ((deps (transdeps-aux curr prev orig graph)))
    (setp deps))
  :rule-classes :rewrite)

Theorem: transdeps-aux-in

(defthm transdeps-aux-in
  (implies (and (in a (transdeps-aux curr prev orig graph))
                (subset curr
                        (union orig (transdeps-allnodes graph)))
                (subset prev
                        (union orig (transdeps-allnodes graph))))
           (in a
               (union orig (transdeps-allnodes graph)))))

Theorem: transdeps-aux-subset

(defthm transdeps-aux-subset
  (implies (and (subset curr
                        (union orig (transdeps-allnodes graph)))
                (subset prev
                        (union orig (transdeps-allnodes graph))))
           (subset (transdeps-aux curr prev orig graph)
                   (union orig (transdeps-allnodes graph)))))