		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)))))