A hons-based And-Inverter Graph (AIG) library for representing and manipulating Boolean functions.

And-Inverter Graphs are a way to represent Boolean functions using only the
operations *and* and *not*.

This AIG library, found in **Hons-AIG library** to distinguish it from another AIG library, aignet. Very briefly:

- Hons-AIGs are simpler, easier to work with, and easier to reason about.
- aignet is faster.

We won't say anything more about Aignet here. A much more detailed comparison of the libraries is available in: Jared Davis and Sol Swords. Verified AIG Algorithms in ACL2. In ACL2 Workshop 2013. May, 2013. EPTCS 114. Pages 95-110.

We always construct AIGs with hons so that existing pieces of AIGs will be automatically reused. We represent AIGs as arbitrary cons trees, which we interpret as follows:

T represents the constant-true function.NIL represents the constant-false function.- Any other atom represents a Boolean variable (i.e., an input to the function.)
- A cons of the form
(A . NIL) represents the negation ofA . - Any other cons,
(A . B) , represents the conjunction ofA andB .

Note that every ACL2 object is a well-formed AIG under this definition.

This meaning of cons trees is given by the evaluation function aig-eval, which returns the (Boolean) value of an AIG under some particular assignment to its variables. This function naturally induces an equivalence relation, aig-equiv: two AIGs are semantically equivalent if they have the same evaluation under every possible variable assignment.

You might wonder why we would restrict ourselves to using only *and*
and *not*? On the surface, using a richer language like S-expressions
might seem more compact. For instance, with S-expressions we could represent

But another critical part of memory efficiency is structure sharing. That
is, suppose that we already need

Besides the aig-semantics functions like aig-eval and aig-equiv, the real core of the library includes:

- Basic, low-level aig-constructors for building
AIGs (
*and*,*or*, etc.). We prove these operations correct with respect to aig-eval. - Somewhat higher-level aig-substitution operations, like aig-restrict, aig-compose, and aig-partial-eval.
- Operations for collecting the variables from an AIG, such as aig-vars.

We provide some tools to "solve" AIGs. Historically we have heavily used the bddify algorithm, which constructs a BDD from an AIG. More recently, aig-sat provides a nice alternative using aignet and satlink to give the problem to a SAT solver.

Beyond this, the rest of the library is a hodgepodge of aig-other algorithms for working with AIGs.

Another option for representing Boolean functions would be to use

- cheaper to construct, e.g., if we want to
*or*together the functionsf andg , it only takes a few conses with AIGs, whereas with BDDs we need to walk throughf andg to construct a new structure (which might be quite large); but - more expensive to compare, e.g., with BDDs we can determine if
f andg are equal via pointer equality, whereas with AIGs this is a satisfiability problem.

This tradeoff is often worth it. For instance, it can often be more faster to construct an AIG and then bddify it than to just directly build the BDD. Why? With the whole AIG visible, the bddify algorithm can often "prune" branches of the AIG that turn out to be irrelevant, and hence avoid constructing large parts of the BDD that aren't really needed.

- Aig-constructors
- Low-level functions for constructing AIGs.
- Aig-vars
`(aig-vars x)`returns the variables of the AIGX .- Aig-sat
- Determine whether an AIG is satisfiable.
- Bddify
- An verified algorithm for converting aigs into ubdds.
- Aig-substitution
- AIG operations for carrying out substitutions, compositions, and partial evaluations.
- Aig-other
- Various hard-to-categorize algorithms for working with AIGs.
- Aig-semantics
- Functions related to the semantic meaning of AIGs, e.g., aig-eval and aig-equiv.
- Aig-and-count
- Counts how many ANDs are in an AIG.