		Search-engine friendly clone of the ACL2 documentation.

Bitops/fast-logrev

Fast-logrev-u16

Fast implementation of (logrev 16 x) for 16-bit unsigned values.

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

(let ((x     #xdead)
      (times 100000000))
  ;; 24.198 seconds
  (time (loop for i fixnum from 1 to times do (logrev 16 x)))
  ;; 1.214 seconds
  (time (loop for i fixnum from 1 to times do (fast-logrev-u16 x))))

Definitions and Theorems

Function: fast-logrev-u16

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