		Search-engine friendly clone of the ACL2 documentation.

Signed-saturate

Signed-saturate16

Optimized implementation of 16-bit signed saturation.

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

Definitions and Theorems

Function: signed-saturate16$inline

(defun signed-saturate16$inline (x)
  (declare (xargs :guard (integerp x)))
  (let ((__function__ 'signed-saturate16))
    (declare (ignorable __function__))
    (mbe :logic (signed-saturate-fn 16 x)
         :exec (cond ((>= x 32767) 32767)
                     ((<= x -32768) 32768)
                     (t (the (unsigned-byte 16)
                             (logand (the (signed-byte 16) x)
                                     65535)))))))