		Search-engine friendly clone of the ACL2 documentation.

Base-api

Gate-id->fanin1

(gate-id->fanin1 id aignet) gets the 1st fanin literal of the AND gate node whose ID is id.

Logically this is just

(fanin 1 (lookup-id id aignet))

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.

Function: gate-id->fanin1

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