Check whether the operand is NaN or infinity. If so, return the integer indefinite.
Function:
(defun sse-cvt-fp-to-int-special (kind nbytes) (declare (xargs :guard (natp nbytes))) (let ((__function__ 'sse-cvt-fp-to-int-special)) (declare (ignorable __function__)) (let ((invalid (or (eq kind 'snan) (eq kind 'qnan) (eq kind 'indef) (eq kind 'inf)))) (if invalid (mv t (ash 1 (1- (ash nbytes 3))) invalid) (mv nil 0 invalid)))))
Theorem:
(defthm integerp-of-sse-cvt-fp-to-int-special.r (implies (and (natp nbytes)) (b* (((mv ?flg acl2::?r ?invalid) (sse-cvt-fp-to-int-special kind nbytes))) (integerp r))) :rule-classes :type-prescription)