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