		Search-engine friendly clone of the ACL2 documentation.

Bitops/parity

Fast-parity

Optimized alternative to parity.

Signature
(fast-parity n x) → p
Arguments: n — Guard (natp n).; x — Guard (integerp x).
Returns: p — Type (bitp p).

This is faster than parity because it computes up to 32 bits of parity at a time using parity32.

Definitions and Theorems

Function: fast-parity

(defun fast-parity (n x)
  (declare (xargs :guard (and (natp n) (integerp x))))
  (let ((__function__ 'fast-parity))
    (declare (ignorable __function__))
    (mbe :logic (parity n x)
         :exec
         (if (<= n 32)
             (parity32 (logand (logmask n) x))
           (logxor (parity32 (logand 4294967295 x))
                   (fast-parity (- n 32) (ash x -32)))))))

Theorem: bitp-of-fast-parity

(defthm acl2::bitp-of-fast-parity
  (b* ((p (fast-parity n x))) (bitp p))
  :rule-classes :type-prescription)