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.
