		Search-engine friendly clone of the ACL2 documentation.

Bitops/fast-logrev

Fast-logrev-u32

Faster implementation of (logrev 32 x) for 32-bit unsigned values.

Signature
(fast-logrev-u32 x) → reverse-x

We could probably do better using the Reverse an N-bit quantity in parallel in 5 * lg(N) operations algorithm, but this is at least pretty fast.

(let ((x     #xdeadbeef)
      (times 50000000))
  ;; 23.864 seconds
  (time (loop for i fixnum from 1 to times do (logrev 32 x)))
  ;; 1.296 seconds
  (time (loop for i fixnum from 1 to times do (fast-logrev-u32 x))))

Definitions and Theorems

Function: fast-logrev-u32

(defun fast-logrev-u32 (x)
  (declare (type (unsigned-byte 32) x))
  (let ((__function__ 'fast-logrev-u32))
    (declare (ignorable __function__))
    (mbe :logic (logrev 32 x)
         :exec
         (b* (((the (unsigned-byte 16) low)
               (logand x 65535))
              ((the (unsigned-byte 16) high)
               (ash x -16))
              ((the (unsigned-byte 16) rlow)
               (fast-logrev-u16 low))
              ((the (unsigned-byte 16) rhigh)
               (fast-logrev-u16 high)))
           (the (unsigned-byte 32)
                (logior (the (unsigned-byte 32) (ash rlow 16))
                        rhigh))))))