		Search-engine friendly clone of the ACL2 documentation.

Utilities

Aignet-record-levels

Records the level of each node in aignet-levels, where combinational inputs and constants have level 0 and a node has level n+1 if its children have maximum level n.

Signature
(aignet-record-levels aignet aignet-levels) → aignet-levels
Returns: aignet-levels — Type (< (fanin-count aignet) (len aignet-levels)).

Does not record a level value for combinational outputs. Look up the level of its fanin node instead.

Definitions and Theorems

Function: aignet-record-levels

(defun aignet-record-levels
       (aignet aignet-levels)
       (declare (xargs :stobjs (aignet aignet-levels)))
       (declare (xargs :guard t))
       (let ((__function__ 'aignet-record-levels))
            (declare (ignorable __function__))
            (b* ((aignet-levels (resize-u32 (num-fanins aignet)
                                            aignet-levels)))
                (aignet-record-levels-aux 0 aignet aignet-levels))))

Theorem: return-type-of-aignet-record-levels

(defthm
   return-type-of-aignet-record-levels
   (b* ((aignet-levels (aignet-record-levels aignet aignet-levels)))
       (< (fanin-count aignet)
          (len aignet-levels)))
   :rule-classes :linear)

Theorem: aignet-levels-correct-of-aignet-record-levels

(defthm aignet-levels-correct-of-aignet-record-levels
        (aignet-levels-correct-up-to
             (+ 1 (fanin-count aignet))
             aignet
             (aignet-record-levels aignet aignet-levels)))