		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.