		Search-engine friendly clone of the ACL2 documentation.

Logand

Bitwise logical `and' of zero or more integers

When integers are viewed in their two's complement representation, logand returns their bitwise logical `and'. In ACL2 logand is a macro that expands into calls of the binary function binary-logand, except that (logand) expands to -1 and (logand x) expands to (the integer x).

The guard for binary-logand requires its arguments to be integers. Logand is defined in Common Lisp. See any Common Lisp documentation for more information.

Macro: logand

(defmacro logand (&rest args)
          (cond ((null args) -1)
                ((null (cdr args))
                 (cons 'the
                       (cons 'integer (cons (car args) 'nil))))
                (t (xxxjoin 'binary-logand args))))

Function: binary-logand

(defun binary-logand (i j)
       (declare (xargs :guard (and (integerp i) (integerp j))))
       (cond ((zip i) 0)
             ((zip j) 0)
             ((eql i -1) j)
             ((eql j -1) i)
             (t (let ((x (* 2 (logand (floor i 2) (floor j 2)))))
                     (+ x
                        (cond ((evenp i) 0)
                              ((evenp j) 0)
                              (t 1)))))))

Subtopics

Ihs/logand-lemmas: Lemmas about logand from the logops-lemmas book.
Logand-defaults: Behavior of logand on bad inputs.
Logand*: Recursive definition of logand.