		Search-engine friendly clone of the ACL2 documentation.

Base-api

Ci-id->ionum

(ci-id->ionum id aignet) gets the input or register number of the node whose ID is id.

Logically this is just

(stype-count (stype (car (lookup-id id aignet)))
             (cdr (lookup-id id aignet)))

However, its guard requires that it may only be called on the ID of a PI or register node. This is because the aignet data structure only stores this information for PIs and registers.

In the execution this is mostly a stobj array lookup in the node array.

Function: ci-id->ionum

(defun ci-id->ionum (id aignet)
 (declare (xargs :stobjs (aignet)))
 (declare (xargs :guard (natp id)))
 (declare (xargs :guard (and (id-existsp id aignet)
                             (eql (id->type id aignet) (in-type)))))
 (let ((__function__ 'ci-id->ionum))
   (declare (ignorable __function__))
   (mbe :logic (non-exec (b* ((suff (lookup-id id aignet)))
                           (stype-count (stype (car suff))
                                        (cdr suff))))
        :exec (snode->ionum^ (id->slot1 id aignet)))))