Truncate
Division returning an integer by truncating toward 0
Example Forms:
ACL2 !>(truncate 14 3)
4
ACL2 !>(truncate -14 3)
-4
ACL2 !>(truncate 14 -3)
-4
ACL2 !>(truncate -14 -3)
4
ACL2 !>(truncate -15 -3)
5
ACL2 !>(truncate 10/4 3/4)
3
(Truncate i j) is the result of taking the quotient of i and
j and dropping the fraction. For example, the quotient of -14 by
3 is -4 2/3, so dropping the fraction 2/3, we obtain a result
for (truncate -14 3) of -4.
The guard for (truncate i j) requires that i and j
are rational (real, in ACL2(r)) numbers and j is non-zero.
Truncate is a Common Lisp function. However, note that unlike Common
Lisp, the ACL2 truncate function returns only a single value, Also see
nonnegative-integer-quotient, which is appropriate for integers and may
simplify reasoning, unless a suitable arithmetic library is loaded, but be
less efficient for evaluation on concrete objects.
Function: truncate
(defun truncate (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))))))
