		Search-engine friendly clone of the ACL2 documentation.

Network

Reference guide for basic functions for working with the AIG network, i.e., a list of nodes.

Lookup-id: Core function for looking up an AIG node in the logical AIG network by its ID.
Lookup-stype: Core function for looking up an input, output, or register in the logical AIG network by its IO number.
Aignet-extension-p: (aignet-extension-p new old) determines if the aignet new is the result of building some new nodes onto another aignet old.
Aignet-nodes-ok: Basic well-formedness constraints for the AIG network.
Aignet-outputs-aux
Aignet-nxsts-aux
Fanin: (fanin which aignet) gets the specified fanin from the first node of the input network and fixes it to be a valid fanin literal of the rest of the network.
Aignet-outputs
Lookup-reg->nxst: Look up the next-state node that corresponds to particular register node.
Aignet-lit-fix: (aignet-lit-fix x aignet) fixes the literal x to be a valid literal for this AIG network.
Aignet-fanins
Stype-count: (stype-count type x) counts the number of nodes whose sequential-type is type in the node list x.
Aignet-nxsts
Aignet-idp: Check whether a node ID is in bounds for this network.
Aignet-norm
Aignet-norm-p
Aignet-id-fix: Fix an ID so that it is valid for the aignet.
Fanin-count: Number of fanin nodes in the list of nodes
Proper-node-listp: (proper-node-listp x) recognizes lists where every element satisfies proper-node-p.
Fanin-node-p
Node-list: A list of node-p objects.
Aignet-litp: Abbreviation for (aignet-idp (lit->var x) aignet).