### BOOLE$

perform a bit-wise logical operation on 2 two's complement integers
Major Section: ACL2-BUILT-INS

When integers `x`

and `y`

are viewed in their two's complement
representation, `(boole$ op x y)`

returns the result of applying the
bit-wise logical operation specified by `op`

. The following table is
adapted from documentation for analogous Common Lisp function `boole`

in
the Common Lisp HyperSpec
(http://www.lisp.org/HyperSpec/Body/fun_boole.html#boole). Note that
the values of `op`

for `boole$`

are ACL2 constants, rather than
corresponding values of `op`

for the Common Lisp function `boole`

.

op result
----------- ---------
*boole-1* x
*boole-2* y
*boole-andc1* and complement of x with y
*boole-andc2* and x with complement of y
*boole-and* and
*boole-c1* complement of x
*boole-c2* complement of y
*boole-clr* the constant 0 (all zero bits)
*boole-eqv* equivalence (exclusive nor)
*boole-ior* inclusive or
*boole-nand* not-and
*boole-nor* not-or
*boole-orc1* or complement of x with y
*boole-orc2* or x with complement of y
*boole-set* the constant -1 (all one bits)
*boole-xor* exclusive or

The guard of `boole$`

specifies that `op`

is the value of one of the
constants above and that `x`

and `y`

are integers.

See any Common Lisp documentation for analogous information about
Common Lisp function `boole`

.

To see the ACL2 definition of this function, see pf.