		Search-engine friendly clone of the ACL2 documentation.

Best-aig

Aig-label-nodes

Assign unique numbers (labels) to the nodes of an AIG.

Signature
(aig-label-nodes x free map) → (mv free map)
Arguments: x — A single AIG to traverse.; free — Smallest label that hasn't been assigned to any node, yet.
Guard (natp free).; map — Fast alist from AIG nodes to labels (which we're constructing).
Returns: free — Updated free index.
Type (natp free).; map — Updated map.

Definitions and Theorems

Function: aig-label-nodes

(defun aig-label-nodes (x free map)
  (declare (xargs :guard (natp free)))
  (let ((__function__ 'aig-label-nodes))
    (declare (ignorable __function__))
    (b* (((when (atom x)) (mv (lnfix free) map))
         ((when (hons-get x map))
          (mv (lnfix free) map))
         ((mv free map)
          (aig-label-nodes (car x) free map))
         ((mv free map)
          (aig-label-nodes (cdr x) free map))
         (map (hons-acons x free map))
         (free (+ 1 free)))
      (mv free map))))

Theorem: natp-of-aig-label-nodes.free

(defthm natp-of-aig-label-nodes.free
  (b* (((mv ?free common-lisp::?map)
        (aig-label-nodes x free map)))
    (natp free))
  :rule-classes :type-prescription)