		Search-engine friendly clone of the ACL2 documentation.

Basic-floating-point-utilities

Make-special-bp

Signature
(make-special-bp kind nan-frac-bits sign exp-width frac-width) → (mv * * * *)
Arguments: nan-frac-bits — Guard (integerp nan-frac-bits).; sign — Guard (integerp sign).; exp-width — Guard (posp exp-width).; frac-width — Guard (posp frac-width).

Definitions and Theorems

Function: make-special-bp

(defun make-special-bp
       (kind nan-frac-bits sign exp-width frac-width)
  (declare (xargs :guard (and (integerp nan-frac-bits)
                              (integerp sign)
                              (posp exp-width)
                              (posp frac-width))))
  (let ((__function__ 'make-special-bp))
    (declare (ignorable __function__))
    (case kind
      (indef (mv 1 (1- (ash 1 exp-width))
                 1 (ash 1 (1- frac-width))))
      (qnan (mv sign (1- (ash 1 exp-width))
                1
                (+ (ash 1 (1- frac-width))
                   nan-frac-bits)))
      (snan (mv sign (1- (ash 1 exp-width))
                1 nan-frac-bits))
      (inf (mv sign (1- (ash 1 exp-width)) 1 0))
      (zero (mv sign 0 0 0))
      (denormal (mv 0 0 0 1))
      (otherwise (mv 0 1 1 0)))))

Theorem: integerp-make-special-bp-0

(defthm integerp-make-special-bp-0
 (implies
    (integerp sign)
    (integerp (mv-nth 0
                      (make-special-bp kind nan-frac-bits
                                       sign exp-width frac-width))))
 :rule-classes :type-prescription)

Theorem: integerp-make-special-bp-1

(defthm integerp-make-special-bp-1
  (integerp (mv-nth 1
                    (make-special-bp kind nan-frac-bits
                                     sign exp-width frac-width)))
  :rule-classes :type-prescription)

Theorem: integerp-make-special-bp-2

(defthm integerp-make-special-bp-2
  (integerp (mv-nth 2
                    (make-special-bp kind nan-frac-bits
                                     sign exp-width frac-width)))
  :rule-classes :type-prescription)

Theorem: integerp-make-special-bp-3

(defthm integerp-make-special-bp-3
 (implies
    (integerp nan-frac-bits)
    (integerp (mv-nth 3
                      (make-special-bp kind nan-frac-bits
                                       sign exp-width frac-width))))
 :rule-classes :type-prescription)