		Search-engine friendly clone of the ACL2 documentation.

Logeqv

Bitwise logical equivalence of zero or more integers

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

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

Macro: logeqv

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

Function: binary-logeqv

(defun binary-logeqv (i j)
  (declare (xargs :guard (and (integerp i) (integerp j))))
  (logand (logorc1 i j) (logorc1 j i)))