		Search-engine friendly clone of the ACL2 documentation.

Best-aig

Aig-list-best

Top level function for choosing the best AIG out of a list.

Signature
(aig-list-best x) → best
Arguments: x — An AIG List, which should be non-empty.
Returns: best — The best AIG in x.

This is easy to use: it handles all of the details of freeing the fast alists and memo tables it uses.

Definitions and Theorems

Function: aig-list-best

(defun aig-list-best (x)
  (declare (xargs :guard t))
  (let ((__function__ 'aig-list-best))
    (declare (ignorable __function__))
    (b* (((mv ?free map)
          (cwtime (aig-list-label-nodes x 0 nil)
                  :mintime 1/2))
         (ret (cwtime (aig-list-best-aux x map)
                      :mintime 1/2)))
      (fast-alist-free map)
      (clear-memoize-table 'aig-collect-andnode-labels)
      (clear-memoize-table 'aig-collect-labels)
      ret)))