And-Inverter Graphs are a way to represent Boolean functions using only the operations and and not.
This AIG library, found in
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:
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
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
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.