		Search-engine friendly clone of the ACL2 documentation.

Logops-definitions

Logmaskp

(logmaskp i) recognizes positive bit-masks, i.e., numbers of the form 2^n - 1.

Signature
(logmaskp i) → bool

Note that this function explicitly checks (integerp i), which means it doesn't satisfy an int-equiv congruence. See also bitmaskp, which fixes its argument and may execute slightly faster.

Definitions and Theorems

Function: logmaskp

(defun logmaskp (i)
  (declare (xargs :guard t))
  (let ((__function__ 'logmaskp))
    (declare (ignorable __function__))
    (mbe :logic (and (integerp i)
                     (>= i 0)
                     (equal i (- (expt2 (integer-length i)) 1)))
         :exec (and (integerp i)
                    (eql i
                         (the unsigned-byte
                              (- (the unsigned-byte
                                      (ash 1 (integer-length i)))
                                 1)))))))

Subtopics

Ihs/logmaskp-lemmas: Lemmas about logmaskp from the logops-lemmas book.
Logmaskp*: Recursive definition of logmaskp.