		Search-engine friendly clone of the ACL2 documentation.

Base-api

Aignet-init

(aignet-init max-outs max-regs max-ins max-nodes aignet) clears the aignet, setting the arrays to the given sizes.

Logically, just returns nil, i.e., the resulting aignet contains only the implicit constant-0 node.

In the execution, we reset the counters associated with the Aignet and also resize the stobj arrays to the indicated sizes.

Note: the max-nodes size indicates the number of logical nodes that the node array will be able to hold without resizing. That is, since each node takes two 32-bit array slots, we resize the physical node array to 2 * max-nodes elements, so that there are room for max-nodes nodes.

Function: aignet-init^

(defun aignet$a::aignet-init^
       (max-outs max-regs max-ins max-nodes aignet)
       (declare (type (unsigned-byte 29) max-outs)
                (type (unsigned-byte 29) max-regs)
                (type (unsigned-byte 29) max-ins)
                (type (unsigned-byte 29) max-nodes))
       (declare (xargs :guard (posp max-nodes)))
       (declare (ignore max-outs
                        max-regs max-ins max-nodes aignet))
       (let ((__function__ 'aignet$a::aignet-init^))
            (declare (ignorable __function__))
            nil))