		Search-engine friendly clone of the ACL2 documentation.

Base-api

Regnum->id

(regnum->id n aignet) gets the ID of the node with register number n.

Logically this is (fanin-count (lookup-stype n :reg aignet)).

In the execution this is a stobj array lookup in the registers array.

Function: regnum->id

(defun aignet$a::regnum->id (n aignet)
  (declare
       (xargs :guard (and (natp n)
                          (aignet$a::aignet-well-formedp aignet))))
  (declare (xargs :guard (< n (aignet$a::num-regs aignet))))
  (let ((__function__ 'aignet$a::regnum->id))
    (declare (ignorable __function__))
    (fanin-count (lookup-stype n (reg-stype) aignet))))