		Search-engine friendly clone of the ACL2 documentation.

Aig-and-count

Counts how many ANDs are in an AIG.

Signature
(aig-and-count x) → count
Returns: count — Type (natp count).

Definitions and Theorems

Function: aig-and-count

(defun aig-and-count (x)
       (declare (xargs :guard t))
       (let ((__function__ 'aig-and-count))
            (declare (ignorable __function__))
            (cond ((aig-atom-p x) 0)
                  ((eq (cdr x) nil)
                   (aig-and-count (car x)))
                  (t (+ 1 (aig-and-count (car x))
                        (aig-and-count (cdr x)))))))

Theorem: natp-of-aig-and-count

(defthm natp-of-aig-and-count
        (b* ((count (aig-and-count x)))
            (natp count))
        :rule-classes :type-prescription)

Theorem: aig-and-count-when-atom

(defthm aig-and-count-when-atom
        (implies (aig-atom-p x)
                 (equal (aig-and-count x) 0)))

Theorem: aig-and-count-of-aig-not

(defthm aig-and-count-of-aig-not
        (equal (aig-and-count (aig-not x))
               (aig-and-count x)))