		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)))))