(ci-id->ionum id aignet) gets the input or register number of the node whose ID is
Logically this is just
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.
(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)))))