		Search-engine friendly clone of the ACL2 documentation.

Best-aig

Aig-list-best-aux1

Main loop for finding the best AIG.

Signature
(aig-list-best-aux1 x best best-ands map) → new-best
Arguments: x — An AIG list.; best — Best AIG we've seen so far.; best-ands — How many unique AND nodes in our best AIG so far.
Guard (natp best-ands).; map — Mapping of AIG nodes to labels.
Returns: new-best — Best AIG in X, or best it's better than everything in X.

Definitions and Theorems

Function: aig-list-best-aux1

(defun aig-list-best-aux1 (x best best-ands map)
  (declare (xargs :guard (natp best-ands)))
  (let ((__function__ 'aig-list-best-aux1))
    (declare (ignorable __function__))
    (b* (((when (atom x)) best)
         (ands (aig-count-andnode-labels (car x) map))
         ((when (or (< ands best-ands)
                    (and (= best-ands ands)
                         (< (aig-count-labels (car x) map)
                            (aig-count-labels best map)))))
          (aig-list-best-aux1 (cdr x)
                              (car x)
                              ands map)))
      (aig-list-best-aux1 (cdr x)
                          best best-ands map))))