The main function is aig-binary-and. It implements something like the algorithm described in:

- Robert Brummayer and Armin Biere. Local Two-Level And Inverter Graph Minimization Without Blowup. Mathematical and Engineering Methods in Computer Science (MEMICS). 2006.

In particular, see Table 2 in that paper, which describes optimization rules that are ``locally size decreasing without affecting global sharing negatively.''

We try to implement these rules in aig-and-main, which returns:

(mv status arg1 arg2)

The status is either:

:fail if no rule applies, in which casearg1 andarg2 are just copies ofx andy and we need to construct a new AND node that joins them together;:subterm if a rewrite rule applies that reduces the AND ofx andy to either a constant or to a subterm ofx ory . This subterm is returned as botharg1 andarg2 . In this case, we assume there is no more rewriting to be done and just return the reduced subterm.:reduced if a rewrite rule applies that reduces the AND in some interesting way, where it is no longer a proper subterm ofx ory . In this case, it may be possible to further reducearg1 andarg2 , so we want to recursively rewrite them.

See also aig-and-dumb, which is much less sophisticated but may be easier to reason about in certain cases where you really care about the structure of the resulting AIGs.

A June 2015 experiment suggests that, for a particular 80-bit floating point addition problem, this fancier algorithm improves the size of AIGs produced by sv by about 3% when measured either by unique AND nodes or by unique conses.

**Macro: **

(defmacro aig-and (&rest args) (cons 'mbe (cons ':logic (cons (aig-and-macro-logic-part args) (cons ':exec (cons (aig-and-macro-exec-part args) 'nil))))))

- Aig-and-main
- And-Node, Main Optimizations, Non-Recursive.
- Aig-and-pass6a
- Level 3 Substitution Rules, Single Direction.
- Aig-and-pass5
- Level 2, Resolution Rule.
- Aig-and-pass3
- Level 2 Contradiction Rule 2 and all Level 4 Rules.
- Aig-and-pass4a
- Level 2, Subsumption Rules 1 and 2, Single Direction.
- Aig-and-pass6
- Level 3 Substitution Rules, Both Directions.
- Aig-and-pass2a
- Level 2 Contradiction Rule 1 and Idempotence Rule, Single Direction.
- Aig-and-pass2
- Level 2 Contradiction Rule 1 and Idempotence Rule, Both Directions.
- Aig-and-pass4
- Level 2, Subsumption Rules 1 and 2, Both Directions.
- Aig-and-dumb
`(aig-and-dumb x y)`is a simpler alternative to aig-and.- Aig-negation-p
`(aig-negation-p x y)`determines if the AIGsx andy are (syntactically) negations of one another.- Aig-and-pass1
- Level 1 simplifications.
- Aig-binary-and
`(aig-binary-and x y)`constructs an AIG representing(and x y) .- Aig-and-macro-exec-part
- Generates the :exec part for a aig-and MBE call.
- Aig-and-macro-logic-part
- Generates the :logic part for a aig-and MBE call.