		Search-engine friendly clone of the ACL2 documentation.

Signed-saturate

Signed-saturate64

Optimized implementation of 64-bit signed saturation.

Signature
(signed-saturate64 x) → *
Arguments: x — Guard (integerp x).

Definitions and Theorems

Function: signed-saturate64$inline

(defun signed-saturate64$inline (x)
  (declare (xargs :guard (integerp x)))
  (let ((__function__ 'signed-saturate64))
    (declare (ignorable __function__))
    (mbe :logic (signed-saturate-fn 64 x)
         :exec (cond ((>= x 9223372036854775807)
                      9223372036854775807)
                     ((<= x -9223372036854775808)
                      9223372036854775808)
                     (t (the (unsigned-byte 64)
                             (logand (the (signed-byte 64) x)
                                     18446744073709551615)))))))