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.