		Search-engine friendly clone of the ACL2 documentation.

Round

Division returning an integer by rounding off

Example Forms:
ACL2 !>(round 14 3)
5
ACL2 !>(round -14 3)
-5
ACL2 !>(round 14 -3)
-5
ACL2 !>(round -14 -3)
5
ACL2 !>(round 13 3)
4
ACL2 !>(round -13 3)
-4
ACL2 !>(round 13 -3)
-4
ACL2 !>(round -13 -3)
4
ACL2 !>(round -15 -3)
5
ACL2 !>(round 15 -2)
-8

(Round i j) is the result of taking the quotient of i and j and rounding off to the nearest integer. When the quotient is exactly halfway between consecutive integers, it rounds to the even one.

The guard for (round i j) requires that i and j are rational (real, in ACL2(r)) numbers and j is non-zero.

Round is a Common Lisp function. See any Common Lisp documentation for more information. However, note that unlike Common Lisp, the ACL2 round function returns only a single value,

Function: round

(defun
     round (i j)
     (declare (xargs :guard (and (real/rationalp i)
                                 (real/rationalp j)
                                 (not (eql j 0)))))
     (let ((q (* i (/ j))))
          (cond ((integerp q) q)
                ((>= q 0)
                 (let* ((fl (floor q 1)) (remainder (- q fl)))
                       (cond ((> remainder 1/2) (+ fl 1))
                             ((< remainder 1/2) fl)
                             (t (cond ((integerp (* fl (/ 2))) fl)
                                      (t (+ fl 1)))))))
                (t (let* ((cl (ceiling q 1))
                          (remainder (- q cl)))
                         (cond ((< (- 1/2) remainder) cl)
                               ((> (- 1/2) remainder) (+ cl -1))
                               (t (cond ((integerp (* cl (/ 2))) cl)
                                        (t (+ cl -1))))))))))