		Search-engine friendly clone of the ACL2 documentation.

Best-aig

Aig-collect-labels

Collect the labels of ALL nodes in an AIG. (memoized)

Signature
(aig-collect-labels x map) → label-set
Arguments: x — A single AIG.; map — Mapping of AIG nodes to labels.
Returns: label-set — Ordered set of labels for all nodes in X.
Type (set::setp label-set).

Definitions and Theorems

Function: aig-collect-labels

(defun aig-collect-labels (x map)
  (declare (xargs :guard t))
  (let ((__function__ 'aig-collect-labels))
    (declare (ignorable __function__))
    (b* (((when (atom x)) nil)
         (x-label (cdr (hons-get x map)))
         (car-labels (aig-collect-labels (car x) map))
         (cdr-labels (aig-collect-labels (cdr x) map)))
      (set::insert x-label
                   (set::union car-labels cdr-labels)))))

Theorem: setp-of-aig-collect-labels

(defthm setp-of-aig-collect-labels
  (b* ((label-set (aig-collect-labels x map)))
    (set::setp label-set))
  :rule-classes :rewrite)

Function: aig-collect-labels-memoize-condition

(defun aig-collect-labels-memoize-condition (x map)
  (declare (ignorable x map)
           (xargs :guard 't))
  (and (consp x) (cdr x)))