		Search-engine friendly clone of the ACL2 documentation.

Basic-floating-point-utilities

Fp-to-rat

Convert the bit-vector or integer representation used by hardware to rational for the cases of zero, denormal, and normal.

Signature
(fp-to-rat sign exp frac bias exp-width frac-width) → *
Arguments: sign — Guard (integerp sign).; exp — Guard (integerp exp).; frac — Guard (integerp frac).; bias — Guard (natp bias).; exp-width — Guard (posp exp-width).; frac-width — Guard (posp frac-width).

Definitions and Theorems

Function: fp-to-rat

(defun fp-to-rat (sign exp frac bias exp-width frac-width)
  (declare (xargs :guard (and (integerp sign)
                              (integerp exp)
                              (integerp frac)
                              (natp bias)
                              (posp exp-width)
                              (posp frac-width))))
  (let ((__function__ 'fp-to-rat))
    (declare (ignorable __function__))
    (cond ((and (eql exp 0) (eql frac 0)) 0)
          ((and (eql exp 0) (not (eql frac 0)))
           (let ((man (* frac (expt 2 (- frac-width)))))
             (* (if (eql sign 0) 1 -1)
                man (expt 2 (- 1 bias)))))
          ((and (< 0 exp)
                (<= exp (fp-max-finite-exp exp-width)))
           (let ((man (* (logior (ash 1 frac-width) frac)
                         (expt 2 (- frac-width)))))
             (* (if (eql sign 0) 1 -1)
                man (expt 2 (- exp bias)))))
          (t 0))))

Theorem: rationalp-fp-to-rat

(defthm rationalp-fp-to-rat
  (implies
       (integerp frac)
       (rationalp (fp-to-rat sign
                             exp frac bias exp-width frac-width)))
  :rule-classes :type-prescription)