		Search-engine friendly clone of the ACL2 documentation.

Bitops

Trailing-1-count

Optimized trailing 0 count for integers.

Signature
(trailing-1-count x) → *
Arguments: x — Guard (integerp x).

To make this fast, be sure and include the "std/bitsets/bignum-extract-opt" book (reqires a ttag), which prevents this (at least on CCL64) from needing to create new bignums when run on bignums.

Definitions and Theorems

Function: trailing-1-count

(defun trailing-1-count (x)
  (declare (xargs :guard (integerp x)))
  (let ((__function__ 'trailing-1-count))
    (declare (ignorable __function__))
    (mbe :logic
         (if (or (eql x -1) (not (logbitp 0 x)))
             0
           (+ 1 (trailing-1-count (logcdr x))))
         :exec
         (if (eql -1 x)
             0
           (trailing-1-count-rec x 0)))))

Theorem: trailing-1-count-is-trailing-0-count-of-lognot

(defthm trailing-1-count-is-trailing-0-count-of-lognot
  (equal (trailing-1-count x)
         (trailing-0-count (lognot x))))