Floor
Division returning an integer by truncating toward negative infinity
Example Forms:
ACL2 !>(floor 14 3)
4
ACL2 !>(floor -14 3)
-5
ACL2 !>(floor 14 -3)
-5
ACL2 !>(floor -14 -3)
4
ACL2 !>(floor -15 -3)
5
(Floor i j) returns the result of taking the quotient of i and
j and returning the greatest integer not exceeding that quotient. For
example, the quotient of -14 by 3 is -4 2/3, and the largest
integer not exceeding that rational number is -5.
The guard for (floor i j) requires that i and j are
rational (real, in ACL2(r)) numbers and j is non-zero.
Floor is a Common Lisp function. See any Common Lisp documentation
for more information. However, note that unlike Common Lisp, the ACL2
floor function returns only a single value, that is, the quotient of the
division, while the remainder is returned by mod.
Function: floor
(defun floor (i j)
(declare (xargs :guard (and (real/rationalp i)
(real/rationalp j)
(not (eql j 0)))))
(let* ((q (* i (/ j)))
(n (numerator q))
(d (denominator q)))
(cond ((= d 1) n)
((>= n 0)
(nonnegative-integer-quotient n d))
(t (+ (- (nonnegative-integer-quotient (- n) d))
-1)))))
