		Search-engine friendly clone of the ACL2 documentation.

Boole$

Perform a bit-wise logical operation on 2 two's complement integers

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 the analogous Common Lisp function boole in the Common Lisp Hyperspec. 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.

Function: boole$

(defun boole$ (op i1 i2)
  (declare (type (integer 0 15) op)
           (type integer i1 i2))
  (cond ((eql op *boole-1*) i1)
        ((eql op *boole-2*) i2)
        ((eql op *boole-and*) (logand i1 i2))
        ((eql op *boole-andc1*)
         (logandc1 i1 i2))
        ((eql op *boole-andc2*)
         (logandc2 i1 i2))
        ((eql op *boole-c1*) (lognot i1))
        ((eql op *boole-c2*) (lognot i2))
        ((eql op *boole-clr*) 0)
        ((eql op *boole-eqv*) (logeqv i1 i2))
        ((eql op *boole-ior*) (logior i1 i2))
        ((eql op *boole-nand*) (lognand i1 i2))
        ((eql op *boole-nor*) (lognor i1 i2))
        ((eql op *boole-orc1*) (logorc1 i1 i2))
        ((eql op *boole-orc2*) (logorc2 i1 i2))
        ((eql op *boole-set*) 1)
        ((eql op *boole-xor*) (logxor i1 i2))
        (t 0)))