		Search-engine friendly clone of the ACL2 documentation.

Integer-length

Number of bits in two's complement integer representation

For non-negative integers, (integer-length i) is the minimum number of bits needed to represent the integer. Any integer can be represented as a signed two's complement field with a minimum of (+ (integer-length i) 1) bits.

The guard for integer-length requires its argument to be an integer. Integer-length is defined in Common Lisp. See any Common Lisp documentation for more information.

Function: integer-length

(defun integer-length (i)
  (declare (xargs :guard (integerp i)))
  (if (zip i)
      0
    (if (= i -1)
        0
      (+ 1 (integer-length (floor i 2))))))

Subtopics

Bitops/integer-length: Basic theorems about integer-length.
Ihs/integer-length-lemmas: Lemmas about integer-length from the logops-lemmas book.
Integer-length*: Recursive definition of integer-length.
Integer-length-default: Behavior of integer-length on bad inputs.