(aignet-update-node-level id levels aignet) → new-levels
Function:
(defun aignet-update-node-level (id levels aignet) (declare (xargs :stobjs (levels aignet))) (declare (xargs :guard (natp id))) (declare (xargs :guard (< id (num-fanins aignet)))) (let ((__function__ 'aignet-update-node-level)) (declare (ignorable __function__)) (b* ((id (lnfix id)) (levels (if (< (u32-length levels) (num-fanins aignet)) (resize-u32 (max 16 (* 2 (num-fanins aignet))) levels) levels)) ((unless (eql (id->type id aignet) (gate-type))) (set-u32 id 0 levels)) (flev0 (get-u32 (lit-id (gate-id->fanin0 id aignet)) levels)) (flev1 (get-u32 (lit-id (gate-id->fanin1 id aignet)) levels))) (set-u32 id (+ 1 (max flev0 flev1)) levels))))
Theorem:
(defthm aignet-update-node-level-length-increases (b* ((?new-levels (aignet-update-node-level id levels aignet))) (<= (len levels) (len new-levels))) :rule-classes :linear)
Theorem:
(defthm aignet-update-node-level-length-lower-bound (b* ((?new-levels (aignet-update-node-level id levels aignet))) (< (fanin-count aignet) (len new-levels))) :rule-classes :linear)
Theorem:
(defthm aignet-update-node-level-of-nfix-id (equal (aignet-update-node-level (nfix id) levels aignet) (aignet-update-node-level id levels aignet)))
Theorem:
(defthm aignet-update-node-level-nat-equiv-congruence-on-id (implies (nat-equiv id id-equiv) (equal (aignet-update-node-level id levels aignet) (aignet-update-node-level id-equiv levels aignet))) :rule-classes :congruence)