		Search-engine friendly clone of the ACL2 documentation.

Bitops

Trailing-0-count

Optimized trailing 0 count for integers.

Signature
(trailing-0-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-0-count

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

Theorem: trailing-0-count-properties

(defthm trailing-0-count-properties
  (implies (not (zip x))
           (let ((count (trailing-0-count x)))
             (and (logbitp count x)
                  (equal (loghead count x) 0)
                  (implies (< (nfix idx) count)
                           (not (logbitp idx x)))))))

Theorem: logand-of-minus-in-terms-of-trailing-0-count

(defthm logand-of-minus-in-terms-of-trailing-0-count
  (implies (not (zip x))
           (equal (logand x (- x))
                  (ash 1 (trailing-0-count x)))))

Theorem: trailing-0-count-bound

(defthm trailing-0-count-bound
  (implies (posp x)
           (< (trailing-0-count x)
              (integer-length x)))
  :rule-classes ((:linear :trigger-terms ((trailing-0-count x)))))

Theorem: trailing-0-count-of-ifix-x

(defthm trailing-0-count-of-ifix-x
  (equal (trailing-0-count (ifix x))
         (trailing-0-count x)))

Theorem: trailing-0-count-int-equiv-congruence-on-x

(defthm trailing-0-count-int-equiv-congruence-on-x
  (implies (int-equiv x x-equiv)
           (equal (trailing-0-count x)
                  (trailing-0-count x-equiv)))
  :rule-classes :congruence)