|
|
|---|
|
|
|
|---|
Fast implementation of
(fast-logrev-u8 x) → reverse-x
This function is based on the Reverse the bits in a byte with 7 operations (no 64-bit) algorithm, described on Sean Anderson's Bit Twiddling Hacks page.
I use this non-64-bit version, even though it takes more operations than some of the other algorithms, because it uses at most a 49-bit integer, which is a fixnum on CCL and probably most other 64-bit Lisps. In contrast, the 64-bit algorithms (probably) would require bignums.
Anyway, it's at least a pretty good improvement over logrev.
(let ((byte #b101010) (times 100000000)) ;; 12.18 seconds (time (loop for i fixnum from 1 to times do (logrev 8 byte))) ;; .32 seconds (time (loop for i fixnum from 1 to times do (fast-logrev-u8 byte))))
Function:
(defun acl2::fast-logrev-u8$inline (x) (declare (type (unsigned-byte 8) x)) (let ((__function__ 'fast-logrev-u8)) (declare (ignorable __function__)) (mbe :logic (logrev 8 x) :exec (b* (((the (unsigned-byte 32) t1) (logand (the (unsigned-byte 32) (* (the (unsigned-byte 16) x) (the (unsigned-byte 16) 2050))) (the (unsigned-byte 32) 139536))) ((the (unsigned-byte 32) t2) (logand (the (unsigned-byte 32) (* (the (unsigned-byte 16) x) (the (unsigned-byte 16) 32800))) (the (unsigned-byte 32) 558144))) ((the (unsigned-byte 32) t3) (logior (the (unsigned-byte 32) t1) (the (unsigned-byte 32) t2))) ((the (unsigned-byte 49) t4) (* (the (unsigned-byte 32) t3) (the (unsigned-byte 17) 65793))) ((the (unsigned-byte 33) t5) (ash t4 -16))) (the (unsigned-byte 8) (logand t5 255))))))