		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