		Search-engine friendly clone of the ACL2 documentation.

Base-api

Gate-id->fanin0

(gate-id->fanin0 id aignet) gets the 0th fanin literal of the AND gate node whose ID is id.

Logically this is just

(fanin 0 (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->fanin0

(defun gate-id->fanin0 (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->fanin0))
    (declare (ignorable __function__))
    (mbe :logic (non-exec (fanin 0 (lookup-id id aignet)))
         :exec (snode->fanin^ (id->slot0 id aignet)))))