Logxor
Bitwise logical exclusive or of zero or more integers
When integers are viewed in their two's complement representation,
logxor returns their bitwise logical exclusive or. In ACL2 logxor
is a macro that expands into calls of the binary function binary-logxor,
except that (logxor) expands to 0 and (logxor x) expands to
(the integer x).
The guard for binary-logxor requires its arguments to be
integers. Logxor is defined in Common Lisp. See any Common Lisp
documentation for more information.
Macro: logxor
(defmacro logxor (&rest args)
(cond ((null args) 0)
((null (cdr args))
(cons 'the
(cons 'integer (cons (car args) 'nil))))
(t (xxxjoin 'binary-logxor args))))
Function: binary-logxor
(defun binary-logxor (i j)
(declare (xargs :guard (and (integerp i) (integerp j))))
(lognot (logeqv i j)))
Subtopics
- Ihs/logxor-lemmas
- Lemmas about logxor from the logops-lemmas book.
- Logxor-defaults
- Behavior of logxor on bad inputs.
- Logxor*
- Recursive definition of logxor.
