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