Reduction logical XOR (i.e., parity) of a 4vec.
We compute the parity of
(4vec-parity #b0) == 0 (all 0s, false) (4vec-parity #b1) == -1 (all 1s, true) (4vec-parity #b11) == 0 (all 0s, false) (4vec-parity #b10) == -1 (all 1s, true)
Subtle. Since 4vecs are ``infinite width,'' reduction
operators are a bit unusual. For parity computations this is especially true
for negative number: if
Function:
(defun 4vec-parity (x) (declare (xargs :guard (4vec-p x))) (let ((__function__ '4vec-parity)) (declare (ignorable __function__)) (if (and (2vec-p x) (<= 0 (2vec->val x))) (b* ((x (2vec->val x))) (2vec (- (fast-parity (+ 1 (integer-length x)) x)))) (4vec-x))))
Theorem:
(defthm 3vec-p!-of-4vec-parity (b* ((parity (4vec-parity x))) (3vec-p! parity)) :rule-classes :rewrite)
Theorem:
(defthm 4vec-parity-of-2vecx-fix-x (equal (4vec-parity (2vecx-fix x)) (4vec-parity x)))
Theorem:
(defthm 4vec-parity-2vecx-equiv-congruence-on-x (implies (2vecx-equiv x x-equiv) (equal (4vec-parity x) (4vec-parity x-equiv))) :rule-classes :congruence)