		Search-engine friendly clone of the ACL2 documentation.

Fast-logext

Fast-logext-exec

Executable definition of fast-logext in the general case.

Signature
(fast-logext-exec b x) → *
Arguments: b — Guard (posp b).; x — Guard (integerp x).

Definitions and Theorems

Function: fast-logext-exec$inline

(defun fast-logext-exec$inline (b x)
  (declare (xargs :guard (and (posp b) (integerp x))))
  (let ((__function__ 'fast-logext-exec))
    (declare (ignorable __function__))
    (b* ((x1 (logand (1- (ash 1 b)) x))
         (m (ash 1 (- b 1))))
      (- (logxor x1 m) m))))

Theorem: fast-logext-exec-is-logext

(defthm fast-logext-exec-is-logext
  (implies (posp b)
           (equal (fast-logext-exec b x)
                  (logext b x))))