		Search-engine friendly clone of the ACL2 documentation.

Base-api

Aignet-set-nxst

(aignet-set-nxst f reg aignet) adds a next-state node to the aignet.

Logically this is just:

(cons (nxst-node (aignet-lit-fix f aignet)
                 (aignet-id-fix regid aignet))
      aignet)

The fixing here ensures that well-formedness of the network is preserved unconditionally.

In the execution we update the necessary arrays, counts, etc.

Function: aignet-set-nxst^

(defun
   aignet$a::aignet-set-nxst^
   (f reg aignet)
   (declare
        (xargs :guard (and (litp f)
                           (natp reg)
                           (aignet$a::aignet-well-formedp aignet))))
   (declare (xargs :guard (and (aignet$a::id-existsp (lit->var f)
                                                     aignet)
                               (< reg (aignet$a::num-regs aignet))
                               (< (aignet$a::num-nxsts aignet)
                                  536870911))))
   (let ((__function__ 'aignet$a::aignet-set-nxst^))
        (declare (ignorable __function__))
        (cons (nxst-node (aignet-lit-fix f aignet)
                         reg)
              (node-list-fix aignet))))