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