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