		Search-engine friendly clone of the ACL2 documentation.

Base-api

Regnum->nxst

(regnum->nxst reg aignet) gets the next-state literal for register number reg.

Logically this is just (lookup-reg->nxst reg aignet))

In the execution this gets the register ID number from the register array and then extracts the next-state literal from the node array.

Function: regnum->nxst

(defun
   regnum->nxst (reg aignet)
   (declare (xargs :stobjs (aignet)))
   (declare (xargs :guard (natp reg)))
   (declare (xargs :guard (< reg (num-regs aignet))))
   (let ((__function__ 'regnum->nxst))
        (declare (ignorable __function__))
        (mbe :logic (non-exec (lookup-reg->nxst reg aignet))
             :exec (snode->fanin^ (id->slot0 (regnum->id reg aignet)
                                             aignet)))))