		Search-engine friendly clone of the ACL2 documentation.

Floating-point-comparison-specifications

Sse-cmp-special

Signature
(sse-cmp-special kind1 sign1 kind2 sign2 exp-width frac-width operation) → (mv * * *)
Arguments: exp-width — Guard (posp exp-width).; frac-width — Guard (posp frac-width).

This function checks whether operands are NaN and then returns the corresponding results. It also handles the infinities.

Return values: (mv flag integer-result invalid)

Definitions and Theorems

Function: sse-cmp-special

(defun sse-cmp-special (kind1 sign1 kind2
                              sign2 exp-width frac-width operation)
 (declare (type (unsigned-byte 1) sign1)
          (type (unsigned-byte 1) sign2)
          (type (integer 0 38) operation))
 (declare (xargs :guard (and (posp exp-width)
                             (posp frac-width))))
 (let ((__function__ 'sse-cmp-special))
  (declare (ignorable __function__))
  (let ((invalid (or (eq kind1 'snan)
                     (eq kind2 'snan)
                     (and (or (eq kind1 'qnan)
                              (eq kind1 'indef)
                              (eq kind2 'qnan)
                              (eq kind2 'indef))
                          (or (int= operation 1)
                              (int= operation 2)
                              (int= operation 5)
                              (int= operation 6)
                              (int= operation 8))))))
   (cond
    ((or (eq kind1 'snan)
         (eq kind1 'qnan)
         (eq kind1 'indef)
         (eq kind2 'snan)
         (eq kind2 'qnan)
         (eq kind2 'indef))
     (cond ((or (int= operation 3)
                (int= operation 4)
                (int= operation 5)
                (int= operation 6))
            (mv t
                (1- (ash 1 (+ 1 exp-width frac-width)))
                invalid))
           ((or (int= operation 8)
                (int= operation 9))
            (mv t 7 invalid))
           (t (mv t 0 invalid))))
    ((or (eq kind1 'inf) (eq kind2 'inf))
     (b*
      ((rat1 (if (eq kind1 'inf)
                 (if (int= sign1 0) 1 -1)
               0))
       (rat2 (if (eq kind2 'inf)
                 (if (int= sign2 0) 1 -1)
               0))
       (cmp-result (case operation
                     (0 (= rat1 rat2))
                     (1 (< rat1 rat2))
                     (2 (<= rat1 rat2))
                     (3 nil)
                     (4 (not (= rat1 rat2)))
                     (5 (not (< rat1 rat2)))
                     (6 (not (<= rat1 rat2)))
                     (7 t)
                     (otherwise nil)))
       (result
            (if (or (int= operation 8)
                    (int= operation 9))
                (cond ((> rat1 rat2) 0)
                      ((< rat1 rat2) 1)
                      (t 4))
              (if cmp-result (1- (ash 1 (+ 1 exp-width frac-width)))
                0))))
      (mv t result invalid)))
    (t (mv nil 0 invalid))))))

Theorem: integerp-sse-cmp-special-1

(defthm integerp-sse-cmp-special-1
 (integerp
    (mv-nth 1
            (sse-cmp-special kind1 sign1 kind2
                             sign2 exp-width frac-width operation)))
 :rule-classes :type-prescription)