		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)))