This function checks whether the operands are SNaN or QNaN. If at least one of them is NaN or both of them are zeros, then it returns the second operand. It also handles infinities.
Return values: (mv flag sign exp implicit frac invalid).
Function:
(defun sse-max/min-special (kind1 sign1 exp1 implicit1 frac1 kind2 sign2 exp2 implicit2 frac2 operation) (declare (type (unsigned-byte 1) sign1) (type (unsigned-byte 1) implicit1) (type (unsigned-byte 1) sign2) (type (unsigned-byte 1) implicit2) (type (integer 0 36) operation)) (declare (xargs :guard (and (natp exp1) (natp frac1) (natp exp2) (natp frac2)))) (let ((__function__ 'sse-max/min-special)) (declare (ignorable __function__)) (cond ((or (eq kind1 'snan) (eq kind1 'qnan) (eq kind1 'indef) (eq kind2 'snan) (eq kind2 'qnan) (eq kind2 'indef)) (mv t sign2 exp2 implicit2 frac2 t)) ((and (eq kind1 'zero) (eq kind2 'zero)) (mv t sign2 exp2 implicit2 frac2 nil)) ((eq kind1 'inf) (if (or (and (int= operation 34) (int= sign1 0)) (and (int= operation 36) (int= sign1 1))) (mv t sign1 exp1 implicit1 frac1 nil) (mv t sign2 exp2 implicit2 frac2 nil))) ((eq kind2 'inf) (if (or (and (int= operation 34) (int= sign2 0)) (and (int= operation 36) (int= sign2 1))) (mv t sign2 exp2 implicit2 frac2 nil) (mv t sign1 exp1 implicit1 frac1 nil))) (t (mv nil 0 0 0 0 nil)))))
Theorem:
(defthm integerp-sse-max/min-special-1 (implies (and (integerp sign1) (integerp sign2)) (integerp (mv-nth 1 (sse-max/min-special kind1 sign1 exp1 implicit1 frac1 kind2 sign2 exp2 implicit2 frac2 operation)))) :rule-classes :type-prescription)
Theorem:
(defthm integerp-sse-max/min-special-2 (implies (and (integerp exp1) (integerp exp2)) (integerp (mv-nth 2 (sse-max/min-special kind1 sign1 exp1 implicit1 frac1 kind2 sign2 exp2 implicit2 frac2 operation)))) :rule-classes :type-prescription)
Theorem:
(defthm integerp-sse-max/min-special-3 (implies (and (integerp implicit1) (integerp implicit2)) (integerp (mv-nth 3 (sse-max/min-special kind1 sign1 exp1 implicit1 frac1 kind2 sign2 exp2 implicit2 frac2 operation)))) :rule-classes :type-prescription)
Theorem:
(defthm integerp-sse-max/min-special-4 (implies (and (integerp frac1) (integerp frac2)) (integerp (mv-nth 4 (sse-max/min-special kind1 sign1 exp1 implicit1 frac1 kind2 sign2 exp2 implicit2 frac2 operation)))) :rule-classes :type-prescription)