(gate-id->fanin1 id aignet) gets the 1st fanin literal of the AND
gate node whose ID is
Logically this is just
The fanin function ensures that the literal returned is a valid fanin, i.e. its ID is less than the ID of the gate node, and is not a combinational output node.
In the execution this is mostly just a stobj array lookup in the node array.
(defun gate-id->fanin1 (id aignet) (declare (xargs :stobjs (aignet))) (declare (xargs :guard (natp id))) (declare (xargs :guard (and (id-existsp id aignet) (eql (id->type id aignet) (gate-type))))) (let ((__function__ 'gate-id->fanin1)) (declare (ignorable __function__)) (mbe :logic (non-exec (fanin 1 (lookup-id id aignet))) :exec (snode->fanin^ (id->slot1 id aignet)))))