Returns rounded sign, exponent, and fraction in case of overflow.
Function:
(defun fp-round-overflow-generic (rc sign exp-width frac-width) (declare (xargs :guard (and (integerp rc) (integerp sign) (posp exp-width) (posp frac-width)))) (let ((__function__ 'fp-round-overflow-generic)) (declare (ignorable __function__)) (rc-cases :rn (mv sign (fp-inf-exp exp-width) (fp-inf-frac)) :rd (if (eql 0 sign) (mv sign (fp-max-finite-exp exp-width) (fp-max-frac frac-width)) (mv sign (fp-inf-exp exp-width) (fp-inf-frac))) :ru (if (eql 0 sign) (mv sign (fp-inf-exp exp-width) (fp-inf-frac)) (mv sign (fp-max-finite-exp exp-width) (fp-max-frac frac-width))) :rz (mv sign (fp-max-finite-exp exp-width) (fp-max-frac frac-width)) :other (mv 0 0 0))))
Theorem:
(defthm integerp-fp-round-overflow-generic-0 (implies (integerp sign) (integerp (mv-nth 0 (fp-round-overflow-generic rc sign exp-width frac-width)))) :rule-classes :type-prescription)
Theorem:
(defthm integerp-fp-round-overflow-generic-1 (integerp (mv-nth 1 (fp-round-overflow-generic rc sign exp-width frac-width))) :rule-classes :type-prescription)
Theorem:
(defthm integerp-fp-round-overflow-generic-2 (integerp (mv-nth 2 (fp-round-overflow-generic rc sign exp-width frac-width))) :rule-classes :type-prescription)