		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) → new-aignet-levels
Returns: new-aignet-levels — Type (< (fanin-count aignet) (len new-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*
   ((new-aignet-levels (aignet-record-levels aignet aignet-levels)))
   (< (fanin-count aignet)
      (len new-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)))

Theorem: len-of-aignet-record-levels

(defthm len-of-aignet-record-levels
 (b*
  ((?new-aignet-levels (aignet-record-levels aignet aignet-levels)))
  (equal (len new-aignet-levels)
         (num-fanins aignet))))