		Search-engine friendly clone of the ACL2 documentation.

Bitops/parity

Parity32

Optimized version of (parity 32 x).

Signature
(parity32 x) → *

The basic idea is from Sean Anderson's bit twiddling hacks page, except that we don't use a lookup table at the end. See parity4 for details about why we don't do that.

Definitions and Theorems

Function: parity32$inline

(defun parity32$inline (x)
 (declare (type (unsigned-byte 32) x))
 (let ((__function__ 'parity32))
  (declare (ignorable __function__))
  (mbe :logic (parity 32 x)
       :exec
       (b* ((x (the (unsigned-byte 32)
                    (logxor x
                            (the (unsigned-byte 32) (ash x -16)))))
            (x (the (unsigned-byte 32)
                    (logxor x (the (unsigned-byte 32) (ash x -8)))))
            (x (the (unsigned-byte 32)
                    (logxor x (the (unsigned-byte 32) (ash x -4)))))
            (x (the (unsigned-byte 32)
                    (logxor x (the (unsigned-byte 32) (ash x -2)))))
            (x (the (unsigned-byte 32)
                    (logxor x
                            (the (unsigned-byte 32) (ash x -1))))))
         (the (unsigned-byte 1) (logand 1 x))))))