		Search-engine friendly clone of the ACL2 documentation.

Bitops/parity

Parity4

Optimized version of (parity 4 x).

Signature
(parity4 x) → p
Returns: p — Type (bitp p).

The basic idea is from Sean Anderson's bit twiddling hacks page. The number #x6996 acts as a lookup table for the parity of the numbers between 0 and 15, so we can simply index into it to get the answer.

It seems that using ash and logand is slightly faster than logbit in ccl. Could perhaps be faster still if we found a way to get CCL to optimize away the ash function call.

Definitions and Theorems

Function: parity4$inline

(defun parity4$inline (x)
 (declare (type (unsigned-byte 4) x))
 (let ((__function__ 'parity4))
  (declare (ignorable __function__))
  (mbe
   :logic (parity 4 x)
   :exec
   (the bit
        (logand 1
                (the (unsigned-byte 32)
                     (ash (the (unsigned-byte 32) 27030)
                          (the (integer -16 0)
                               (- (the (unsigned-byte 4) x))))))))))

Theorem: bitp-of-parity4

(defthm bitp-of-parity4
  (b* ((p (parity4$inline x))) (bitp p))
  :rule-classes :type-prescription)