		Search-engine friendly clone of the ACL2 documentation.

Best-aig

Aig-list-list-best

Top-level function for choosing the best AIGs from a list of AIG lists.

Signature
(aig-list-list-best x) → best
Arguments: x — An AIG List List, say (L1 L2 ... Ln). These should each be non-empty.
Returns: best — An AIG List, say (B1 B2 ... Bn), where each Bi is the best AIG from the corresponding Li.

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-list-best

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