• Top
    • Documentation
    • Books
    • Recursion-and-induction
    • Boolean-reasoning
      • Ipasir
      • Aignet
      • Aig
        • Aig-constructors
        • Aig-vars
        • Aig-sat
        • Bddify
        • Aig-substitution
        • Aig-other
          • Best-aig
            • Aig-label-nodes
            • Aig-list-list-best
            • Aig-collect-andnode-labels
            • Aig-list-best-aux1
            • Aig-collect-labels
            • Aig-list-best
            • Aig-list-list-label-nodes
            • Aig-list-label-nodes
            • Aig-list-list-best-aux
            • Aig-count-andnode-labels
            • Aig-list-best-aux
            • Aig-count-labels
          • Aig2c
          • Expr-to-aig
          • Aiger-write
          • Aig-random-sim
          • Aiger-read
          • Aig-print
          • Aig-cases
        • Aig-semantics
        • Aig-and-count
      • Satlink
      • Truth
      • Ubdds
      • Bdd
      • Faig
      • Bed
      • 4v
    • Projects
    • Debugging
    • Std
    • Proof-automation
    • Macro-libraries
    • ACL2
    • Interfacing-tools
    • Hardware-verification
    • Software-verification
    • Testing-utilities
    • Math
  • Aig-other

Best-aig

Algorithms for choosing "better" (smaller) AIGs.

Given two AIGs, A and B, we say that A is "better" than B if:

  • A has fewer unique AND nodes than B, or
  • A,B have the same number of unique AND nodes, but A has fewer total nodes than B.

We provide two main functions for choosing good AIGs:

  • aig-list-best chooses the best AIG from a non-empty list of AIGs.
  • aig-list-list-best is given a list of non-empty AIG Lists, say (L1 L2 ... Ln), and returns (B1 B2 ... Bn), where each Bi is the best AIG from the corresponding Li.

You could just implement aig-list-list-best as an ordinary "map" or projection of aig-list-best. But aig-list-list-best is written in a slightly smarter way than this, so that it can share the labels and memoization results across all of the AIGs in all of the lists.

Implementation

It is tricky to directly count "unique nodes" in a memoized way, but there is a very easy way to do it indirectly.

First, we assign a number to every unique AIG node in sight, which (assuming constant-time hashing) is linear in the sizes of the input AIGs. We call these numbers labels.

Next, we can write memoized functions to gather the sets of labels for all of the AND nodes within an AIG, and similarly for all of the nodes. We just use regular ordered sets to represent these sets. Importantly, these collection functions can be easily memoized.

Finally, to count the number of ANDs (or all nodes) in an AIG, we just collect the labels for its ANDs (or all nodes) and see how many labels were found.

BOZO it would probably be much better to use sbitsets to represent label sets. If we ever need to speed this up, that's probably the first thing to try.

Subtopics

Aig-label-nodes
Assign unique numbers (labels) to the nodes of an AIG.
Aig-list-list-best
Top-level function for choosing the best AIGs from a list of AIG lists.
Aig-collect-andnode-labels
Collect the labels for AND nodes in an AIG. (memoized)
Aig-list-best-aux1
Main loop for finding the best AIG.
Aig-collect-labels
Collect the labels of ALL nodes in an AIG. (memoized)
Aig-list-best
Top level function for choosing the best AIG out of a list.
Aig-list-list-label-nodes
Extends aig-label-nodes to an AIG list list.
Aig-list-label-nodes
Extends aig-label-nodes to an AIG list.
Aig-list-list-best-aux
Aig-count-andnode-labels
Aig-list-best-aux
Aig-count-labels