		Search-engine friendly clone of the ACL2 documentation.

4vec-operations

4vec-reduction-or

Reduction logical OR of a 4vec.

Signature
(4vec-reduction-or x) → or-x
Arguments: x — Guard (4vec-p x).
Returns: or-x — Type (3vec-p! or-x).

ORs together all of the bits in a 4vec. Following the boolean-convention, we return:

False (all 0s) if all of the (infinite) bits are 0, i.e., if X is 0,
True (all 1s) if there is any bit that is 1, or
All Xes otherwise.

When translating Verilog, the input vector may be either sign- or 0-extended without affecting the result.

Definitions and Theorems

Function: 4vec-reduction-or

(defun 4vec-reduction-or (x)
  (declare (xargs :guard (4vec-p x)))
  (let ((__function__ '4vec-reduction-or))
    (declare (ignorable __function__))
    (3vec-reduction-or (3vec-fix x))))

Theorem: 3vec-p!-of-4vec-reduction-or

(defthm 3vec-p!-of-4vec-reduction-or
  (b* ((or-x (4vec-reduction-or x)))
    (3vec-p! or-x))
  :rule-classes :rewrite)

Theorem: 4vec-reduction-or-recursive

(defthm 4vec-reduction-or-recursive
 (equal
  (4vec-reduction-or x)
  (b*
   (((4vec x))
    ((when (and (or (zip x.upper) (eql x.upper -1))
                (or (zip x.lower) (eql x.lower -1))))
     (3vec-fix x))
    (first (4vec-idx->4v 0 x))
    (or-rest
        (4vec-idx->4v 0
                      (4vec-reduction-or (4vec (logcdr x.upper)
                                               (logcdr x.lower))))))
   (4v->4vec-bit (acl2::4v-or first or-rest))))
 :rule-classes
 ((:definition :install-body nil
               :clique (4vec-reduction-or)
               :controller-alist ((4vec-reduction-or t)))))

Theorem: 4vec-reduction-or-of-3vec-fix-x

(defthm 4vec-reduction-or-of-3vec-fix-x
  (equal (4vec-reduction-or (3vec-fix x))
         (4vec-reduction-or x)))

Theorem: 4vec-reduction-or-3vec-equiv-congruence-on-x

(defthm 4vec-reduction-or-3vec-equiv-congruence-on-x
  (implies (3vec-equiv x x-equiv)
           (equal (4vec-reduction-or x)
                  (4vec-reduction-or x-equiv)))
  :rule-classes :congruence)