		Search-engine friendly clone of the ACL2 documentation.

Fast-logext

Fast-logext64

Optimized implementation of 64-bit sign-extension.

Signature
(fast-logext64 x) → *
Arguments: x — Guard (integerp x).

Definitions and Theorems

Function: fast-logext64$inline

(defun fast-logext64$inline (x)
 (declare (xargs :guard (integerp x)))
 (let ((__function__ 'fast-logext64))
   (declare (ignorable __function__))
   (mbe :logic (logext 64 x)
        :exec
        (if (and (<= x 1152921504606846975)
                 (<= -1152921504606846976 x))
            x
          (the (signed-byte 64)
               (- (the (unsigned-byte 64)
                       (logxor (the (unsigned-byte 64)
                                    (logand 18446744073709551615 x))
                               (the (unsigned-byte 64)
                                    9223372036854775808)))
                  9223372036854775808))))))