		Search-engine friendly clone of the ACL2 documentation.

Implementation-environments

Schar-format->min

The ACL2 integer value of SCHAR_MIN [C17:5.2.4.2.1/1].

Signature
(schar-format->min schar-format uchar-format) → min
Arguments: schar-format — Guard (schar-formatp schar-format).; uchar-format — Guard (uchar-formatp uchar-format).
Returns: min — Type (integerp min).

Based on the discussion in schar-format, this is either - 2^{\mathtt{CHAR\_BIT}-1} (if the signed format is two's complement and the pattern with sign bit 1 and all value bits 0 is not a trap representation) or - 2^{\mathtt{CHAR\_BIT}-1} + 1 (if the signed format is ones' complement or sign-and-magnitude, or it is two's complement but the pattern with sign bit 1 and all value bits 0 is a trap representation).

Like schar-format->max, this function also depends on the unsigned char format. Unlike schar-format->max, this function also depends on the signed char format.

Definitions and Theorems

Function: schar-format->min

(defun schar-format->min (schar-format uchar-format)
 (declare (xargs :guard (and (schar-formatp schar-format)
                             (uchar-formatp uchar-format))))
 (let ((__function__ 'schar-format->min))
  (declare (ignorable __function__))
  (if
   (and
     (equal (signed-format-kind (schar-format->signed schar-format))
            :twos-complement)
     (not (schar-format->trap schar-format)))
   (- (expt 2
            (1- (uchar-format->size uchar-format))))
   (- (1- (expt 2
                (1- (uchar-format->size uchar-format))))))))

Theorem: integerp-of-schar-format->min

(defthm integerp-of-schar-format->min
  (b* ((min (schar-format->min schar-format uchar-format)))
    (integerp min))
  :rule-classes :rewrite)

Theorem: schar-format->min-type-prescription

(defthm schar-format->min-type-prescription
  (b* ((common-lisp::?min
            (schar-format->min schar-format uchar-format)))
    (and (integerp min) (< min 0)))
  :rule-classes :type-prescription)

Theorem: schar-format->min-upper-bound

(defthm schar-format->min-upper-bound
 (b* ((common-lisp::?min
           (schar-format->min schar-format uchar-format)))
   (<= min -127))
 :rule-classes
 ((:linear
   :trigger-terms ((schar-format->min schar-format uchar-format)))))

Theorem: schar-format->min-of-schar-format-fix-schar-format

(defthm schar-format->min-of-schar-format-fix-schar-format
  (equal (schar-format->min (schar-format-fix schar-format)
                            uchar-format)
         (schar-format->min schar-format uchar-format)))

Theorem: schar-format->min-schar-format-equiv-congruence-on-schar-format

(defthm
    schar-format->min-schar-format-equiv-congruence-on-schar-format
  (implies
       (schar-format-equiv schar-format schar-format-equiv)
       (equal (schar-format->min schar-format uchar-format)
              (schar-format->min schar-format-equiv uchar-format)))
  :rule-classes :congruence)

Theorem: schar-format->min-of-uchar-format-fix-uchar-format

(defthm schar-format->min-of-uchar-format-fix-uchar-format
  (equal (schar-format->min schar-format
                            (uchar-format-fix uchar-format))
         (schar-format->min schar-format uchar-format)))

Theorem: schar-format->min-uchar-format-equiv-congruence-on-uchar-format

(defthm
    schar-format->min-uchar-format-equiv-congruence-on-uchar-format
  (implies
       (uchar-format-equiv uchar-format uchar-format-equiv)
       (equal (schar-format->min schar-format uchar-format)
              (schar-format->min schar-format uchar-format-equiv)))
  :rule-classes :congruence)