Bitwise logical `and' of two ints, complementing the second
When integers are viewed in their two's complement representation,
logandc2 returns the bitwise logical `and' of the first with the bitwise
logical `not' of the second.
The guard for logandc2 requires its arguments to be integers.
Logandc2 is defined in Common Lisp. See any Common Lisp documentation
for more information.
(defun logandc2 (i j)
(declare (xargs :guard (and (integerp i) (integerp j))))
(logand i (lognot j)))