• Top
    • Documentation
    • Books
    • Boolean-reasoning
      • Ipasir
      • Aignet
        • Base-api
        • Aignet-construction
        • Representation
          • Aignet-impl
          • Node
          • Network
            • Lookup-id
            • Lookup-stype
            • Aignet-extension-p
            • Aignet-nodes-ok
            • Aignet-outputs-aux
            • Aignet-nxsts-aux
            • Fanin
            • Aignet-outputs
            • Lookup-reg->nxst
            • Aignet-lit-fix
            • Aignet-fanins
            • Stype-count
            • Aignet-nxsts
            • Aignet-idp
            • Aignet-norm
            • Aignet-norm-p
            • Aignet-id-fix
            • Fanin-count
            • Proper-node-listp
            • Fanin-node-p
            • Node-list
            • Aignet-litp
          • Combinational-type
          • Typecode
          • Stypep
        • Aignet-copy-init
        • Aignet-simplify-with-tracking
        • Aignet-simplify-marked-with-tracking
        • Aignet-cnf
        • Aignet-simplify-marked
        • Aignet-complete-copy
        • Aignet-transforms
        • Aignet-eval
        • Semantics
        • Aignet-read-aiger
        • Aignet-write-aiger
        • Aignet-abc-interface
        • Utilities
      • Aig
      • Satlink
      • Truth
      • Ubdds
      • Bdd
      • Faig
      • Bed
      • 4v
    • Projects
    • Debugging
    • Std
    • Proof-automation
    • Macro-libraries
    • ACL2
    • Interfacing-tools
    • Hardware-verification
    • Software-verification
    • Math
    • Testing-utilities
  • Representation

Network

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

Subtopics

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