		Search-engine friendly clone of the ACL2 documentation.

Implementation-environments

Schar-format->max

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

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

Based on the discussion in schar-format, this is always 2^{\mathtt{CHAR\_BIT}-1} - 1.

This depends on CHAR_BIT, so this function also takes the unsigned char format as input. In fact, this function only depends on CHAR_BIT, but we include the signed char format as input for uniformity.

Definitions and Theorems

Function: schar-format->max

(defun schar-format->max (schar-format uchar-format)
  (declare (xargs :guard (and (schar-formatp schar-format)
                              (uchar-formatp uchar-format))))
  (declare (ignore schar-format))
  (let ((__function__ 'schar-format->max))
    (declare (ignorable __function__))
    (1- (expt 2
              (1- (uchar-format->size uchar-format))))))

Theorem: posp-of-schar-format->max

(defthm posp-of-schar-format->max
  (b* ((max (schar-format->max schar-format uchar-format)))
    (posp max))
  :rule-classes :rewrite)

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

(defthm schar-format->max-type-prescription
  (b* ((common-lisp::?max
            (schar-format->max schar-format uchar-format)))
    (and (posp max) (> max 1)))
  :rule-classes :type-prescription)

Theorem: schar-format->max-lower-bound

(defthm schar-format->max-lower-bound
  (b* ((common-lisp::?max
            (schar-format->max schar-format uchar-format)))
    (>= max 127))
  :rule-classes :linear)

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

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

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

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

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

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

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

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