		Search-engine friendly clone of the ACL2 documentation.

Aig-constructors

Aig-or-list

(aig-or-list x) ors together all of the AIGs in the list x.

Signature
(aig-or-list x) → aig

As a dumb attempt at optimization, we try to avoid consing if we see that there's a t 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-or-list

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

Theorem: aig-or-list-aux-removal

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

Subtopics

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