		Search-engine friendly clone of the ACL2 documentation.

Logops-definitions

Logsat

Signed saturation. (logsat size i) coerces i to a size-bit signed integer by saturation.

Signature
(logsat size i) → int
Arguments: size — Guard (and (integerp size) (< 0 size)).; i — Guard (integerp i).
Returns: int — Type (integerp int).

If i can be represented as a size-bit signed integer, then i is returned unchanged. Otherwise, (logsat size i) returns the size-bit signed integer closest to i. For positive i, this will be 2^{size-1} - 1. For negative i, this will be -(2^{size-1}.

This function returns a (possibly negative) integer. For consistency with signed-byte-p, size must be strictly greater than 0. In contrast, the related bitops::bitops/saturate functions always return size-bit natural numbers.

Definitions and Theorems

Function: logsat

(defun logsat (size i)
       (declare (type unsigned-byte size))
       (declare (xargs :guard (and (and (integerp size) (< 0 size))
                                   (integerp i))))
       (declare (xargs :split-types t))
       (let ((__function__ 'logsat))
            (declare (ignorable __function__))
            (let* ((i (mbe :logic (ifix i) :exec i))
                   (val (expt2 (the unsigned-byte (1- size))))
                   (maxval (the unsigned-byte
                                (1- (the unsigned-byte val))))
                   (minval (- val)))
                  (declare (type unsigned-byte val maxval)
                           (type integer i minval))
                  (if (>= i maxval)
                      maxval (if (<= i minval) minval i)))))

Theorem: logsat-type

(defthm logsat-type
        (b* ((int (logsat size i)))
            (integerp int))
        :rule-classes :type-prescription)

Subtopics

Logsat-basics