		Search-engine friendly clone of the ACL2 documentation.

Best-aig

Aig-list-best-aux

Signature
(aig-list-best-aux x map) → best
Arguments: x — A non-empty list of AIGs.; map — Mapping of AIG nodes to labels.
Returns: best — Best AIG in X.

Definitions and Theorems

Function: aig-list-best-aux

(defun aig-list-best-aux (x map)
  (declare (xargs :guard t))
  (let ((__function__ 'aig-list-best-aux))
    (declare (ignorable __function__))
    (if (atom x)
        (raise "Expected at least one aig.")
      (aig-list-best-aux1 (cdr x)
                          (car x)
                          (aig-count-andnode-labels (car x) map)
                          map))))