		Search-engine friendly clone of the ACL2 documentation.

Base-api

Id->phase

(id->phase id aignet) computes the value of the node under the all-0 simulation.

In the logic, we have to compute the value by recursively walking over the node array. However, in the execution we keep these values pre-computed so this is mostly just a stobj array lookup in the node array.

Function: id->phase

(defun id->phase (id aignet)
       (declare (xargs :stobjs (aignet)))
       (declare (xargs :guard (natp id)))
       (declare (xargs :guard (id-existsp id aignet)))
       (let ((__function__ 'id->phase))
            (declare (ignorable __function__))
            (mbe :logic (non-exec (id-phase id aignet))
                 :exec (snode->phase^ (id->slot1 id aignet)))))