• Top
  • Documentation
  • Books
  • Recursion-and-induction
  • Boolean-reasoning
  • Projects
  • Debugging
  • Std
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
  • Software-verification
  • Testing-utilities
  • Math
    • Arithmetic
    • Bit-vectors
      • Sparseint
      • Bitops
        • Bitops/merge
        • Bitops-compatibility
        • Bitops-books
        • Logbitp-reasoning
        • Bitops/signed-byte-p
        • Fast-part-select
        • Bitops/integer-length
        • Bitops/extra-defs
        • Install-bit
        • Trailing-0-count
        • Bitops/defaults
        • Logbitp-mismatch
        • Trailing-1-count
        • Bitops/rotate
        • Bitops/equal-by-logbitp
        • Bitops/ash-bounds
        • Bitops/fast-logrev
        • Limited-shifts
        • Bitops/part-select
        • Bitops/parity
        • Bitops/saturate
        • Bitops/part-install
        • Bitops/logbitp-bounds
        • Bitops/ihsext-basics
        • Bitops/fast-rotate
        • Bitops/fast-logext
        • Bitops/ihs-extensions
      • Bv
      • Ihs
      • Rtl
    • Algebra

• 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)