		Search-engine friendly clone of the ACL2 documentation.

Aig-constructors

Aig-and-list

(aig-and-list x) ands together all of the AIGs in the list x.

Signature
(aig-and-list x) → aig

As a dumb attempt at optimization, we try to avoid consing if we see that there's a nil anywhere in the list. This won't win very often, but it is quite cheap and it can win big when it does win by avoiding a lot of AIG construction.

Definitions and Theorems

Function: aig-and-list

(defun aig-and-list (x)
  (declare (xargs :guard t))
  (let ((__function__ 'aig-and-list))
    (declare (ignorable __function__))
    (mbe :logic
         (if (atom x)
             t
           (aig-and (car x)
                    (aig-and-list (cdr x))))
         :exec (cond ((atom x) t)
                     ((member-eql-without-truelistp nil x)
                      nil)
                     (t (aig-and-list-aux x))))))

Theorem: aig-and-list-aux-removal

(defthm aig-and-list-aux-removal
  (equal (aig-and-list-aux x)
         (aig-and-list x)))

Subtopics

Member-eql-without-truelistp
Aig-and-list-aux