		Search-engine friendly clone of the ACL2 documentation.

Base-api

Aignet-add-out

(aignet-add-out f aignet) adds a primary output node to the aignet.

Logically this is just:

(cons (po-node (aignet-lit-fix f aignet))
      aignet)

The aignet-lit-fix ensures that well-formedness of the network is preserved unconditionally.

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

Function: aignet-add-out^

(defun
   aignet$a::aignet-add-out^ (f aignet)
   (declare
        (xargs :guard (and (litp f)
                           (aignet$a::aignet-well-formedp aignet))))
   (declare (xargs :guard (and (aignet$a::id-existsp (lit->var f)
                                                     aignet)
                               (< (aignet$a::num-outs aignet)
                                  536870910))))
   (let ((__function__ 'aignet$a::aignet-add-out^))
        (declare (ignorable __function__))
        (cons (po-node (aignet-lit-fix f aignet))
              (node-list-fix aignet))))