• Top
    • Documentation
    • Books
    • Boolean-reasoning
    • Projects
    • Debugging
    • Std
    • Proof-automation
    • Macro-libraries
    • ACL2
    • Interfacing-tools
    • Hardware-verification
    • Software-verification
    • Math
      • 100-theorems
      • Arithmetic
      • Bit-vectors
        • Sparseint
          • Sparseint-impl
          • Sparseint-p
          • Sparseint-binary-bittest
          • Sparseint-concatenate
          • Sparseint-binary-bitop
          • Sparseint-bitite
          • Sparseint-fix
          • Sparseint$-binary-minus
          • Sparseint-trailing-1-count-from
          • Sparseint-trailing-0-count-from
          • Sparseint-equal
          • Sparseint-test-bitorc2
          • Sparseint-test-bitorc1
          • Sparseint-test-bitnand
          • Sparseint-test-bitandc2
          • Sparseint-test-bitandc1
          • Sparseint-test-bitand
          • Sparseint-rightshift
          • Sparseint-bitcount-from
          • Sparseint-test-bitxor
          • Sparseint-test-bitor
          • Sparseint-test-bitnor
          • Sparseint-test-biteqv
          • Sparseint-compare
          • Sparseint-binary-minus
          • Sparseint-sign-ext
          • Sparseint-plus
          • Sparseint-bitandc2
          • Sparseint-bitandc1
          • Sparseint-bitand
          • Sparseint$-leaf-bitlimit
          • Sparseint-bitxor
          • Sparseint-bitorc2
          • Sparseint-bitorc1
          • Sparseint-bitor
          • Sparseint-bitnor
          • Sparseint-bitnand
          • Sparseint-biteqv
          • Sparseint-ash
          • Sparseint-<
          • Sparseint-bit
          • Sparseint-trailing-1-count
          • Sparseint-trailing-0-count
          • Sparseint-unary-minus
          • Sparseint-length
          • Sparseint-bitnot
          • Sparseint-bitcount
          • Int-to-sparseint
          • Sparseint-val
        • Bitops
        • Bv
        • Ihs
        • Rtl
      • Algebra
    • Testing-utilities
  • Bit-vectors

Sparseint

Alternative implementation of bignums based on balanced binary trees

In some applications it's convenient to operate on long bitvectors. Most Lisp implementations use immutable, array-based bignum representations. This means that when you create a new bitvector, it must allocate new memory to hold it even if a large chunk of that vector is simply a copy of some existing one.

Sparseints are an alternative bignum representation that tries to avoid this problem. They use a binary tree representation to allow structure sharing between vectors. To support efficient operations, they are built using an AVL-style balancing discipline which guarantees that the longest path from the root to a leaf is at most twice the length of the shortest such path. This balancing discipline means that concatenations, which could easily be implemented as constant-time operations, are instead (log n) time, but that right-shifts, which would otherwise be linear time, are also (log n) time.

High-level interface

The sparseint type is recognized by sparseint-p and fixed by sparseint-fix. It is FTY discipline compliant.

To make a sparseint from an integer, use (int-to-sparseint x). Often this will just return x. Every integer is a sparseint, but int-to-sparseint will break down larger integers into tree structures.

To get the integer value of a sparseint, use (sparseint-val x). Make sure you have enough memory to hold the integer value that this produces!

The rest of the operations on sparseints are listed here. As a syntactic convention, let x, y, and z be sparseints, and use xv, yv, and zv to signify (sparseint-val x), etc.

  • (sparseint-concatenate width x y), where width is a natural number, creates a new sparseint whose value is (logapp width xv yv). This can be used for left shifts, i.e., (sparseint-concatenate shift-amt 0 y).
  • (sparseint-rightshift shift x), where shift is a natural number, creates a new sparseint whose value is (ash xv (- shift)).
  • (sparseint-ash x shift), where shift is an integer, creates a new sparseint whose value is (ash xv shift).
  • (sparseint-sign-ext n x), where n is a positive number, creates a new sparseint whose value is (logext n xv).
  • (sparseint-bit n x), where n is a natural number, returns the bit (logbit n xv).
  • (sparseint-bitnot x) creates a new sparseint whose value is (lognot xv).
  • Of each of the following pairs of functions, the first computes a new sparseint whose value is (bitop xv yv), and the second returns (not (equal 0 (bitop xv yv))):
    • (sparseint-bitand x y), (sparseint-test-bitand x y)
    • sparseint-bitor, sparseint-test-bitor
    • sparseint-bitxor, sparseint-test-bitxor
    • sparseint-biteqv, sparseint-test-biteqv
    • sparseint-bitnand, sparseint-test-bitnand
    • sparseint-bitnor, sparseint-test-bitnor
    • sparseint-bitandc1, sparseint-test-bitandc1
    • sparseint-bitandc2, sparseint-test-bitandc2
    • sparseint-bitorc1, sparseint-test-bitorc1
    • sparseint-bitorc2, sparseint-test-bitorc2.
    These are all implemented using a pair of generic functions (sparseint-binary-bitop op x y) and (sparseint-binary-bittest op x y), where op is a 4-bit unsigned integer interpreted as a truth table describing the logical operation. That is, bit n of the result will be (logbit (+ (logbit n xv) (* 2 (logbit n yv))) op), so #b0100 signifies ANDc1, #b0110 signifies XOR, etc.
  • (sparseint-bitite x y z) returns a sparseint whose value is the bitwise if-then-else of xv, yv, zv.
  • (sparseint-equal x y) returns (equal xv yv).
  • (sparseint-compare x y) returns (compare xv yv), where compare returns 0 when its inputs are equal, -1 when the first is less than the second, and 1 when the first is greater than the second.
  • (sparseint-< x y) returns (< xv yv).
  • (sparseint-length x) returns (integer-length xv).
  • (sparseint-plus x y) returns a new sparseint whose value is (+ xv yv).
  • (sparseint-unary-minus x) returns a new sparseint whose value is (- xv).
  • (sparseint-binary-minus x y) returns a new sparseint whose value is (- xv yv).
  • (sparseint-trailing-0-count x) returns (trailing-0-count xv) and (sparseint-trailing-0-count-from x n) returns (trailing-0-count-from xv n). Similarly for (sparseint-trailing-1-count x) and (sparseint-trailing-1-count-from x n).
  • (sparseint-bitcount x) returns (logcount xv) and (sparseint-bitcount-from n x) returns (logcount (logtail n xv)).

Subtopics

Sparseint-impl
Umbrella topic for functions used in implementation of sparseint operations.
Sparseint-p
Recognizer for well-formed sparseints
Sparseint-binary-bittest
Test whether a binary bitwise operation (represented as a 4-bit truth table) on two sparseints yields a nonzero value.
Sparseint-concatenate
Form the concatenation (logapp) of two sparseints
Sparseint-binary-bitop
Apply a binary bitwise operation (represented as a 4-bit truth table) to two sparseints.
Sparseint-bitite
Compute the bitwise if-then-else of the three sparseint inputs.
Sparseint-fix
Fixing function for sparseints
Sparseint$-binary-minus
Subtract one sparseint from another.
Sparseint-trailing-1-count-from
Count the consecutive 1s of a sparseint starting at the given offset.
Sparseint-trailing-0-count-from
Count the consecutive 0s of a sparseint starting at the given offset.
Sparseint-equal
Check equality of the integer values of two sparseints
Sparseint-test-bitorc2
Check whether the logorc2 of two sparseints produces a nonzero value.
Sparseint-test-bitorc1
Check whether the logorc1 of two sparseints produces a nonzero value.
Sparseint-test-bitnand
Check whether the lognand of two sparseints produces a nonzero value.
Sparseint-test-bitandc2
Check whether the logandc2 of two sparseints produces a nonzero value.
Sparseint-test-bitandc1
Check whether the logandc1 of two sparseints produces a nonzero value.
Sparseint-test-bitand
Check whether the logand of two sparseints produces a nonzero value.
Sparseint-rightshift
Right-shift a sparseint by some shift amount
Sparseint-bitcount-from
Count the 1 bits in a sparseint if positive, 0 bits if negative, starting from offset.
Sparseint-test-bitxor
Check whether the logxor of two sparseints produces a nonzero value.
Sparseint-test-bitor
Check whether the logior of two sparseints produces a nonzero value.
Sparseint-test-bitnor
Check whether the lognor of two sparseints produces a nonzero value.
Sparseint-test-biteqv
Check whether the logeqv of two sparseints produces a nonzero value.
Sparseint-compare
Compare the values of two sparseints and return -1, 0, or 1.
Sparseint-binary-minus
Subtract two sparseints.
Sparseint-sign-ext
Sign-extend the given sparseint at the given (positive) position
Sparseint-plus
Add two sparseints.
Sparseint-bitandc2
Compute the logandc2 of two sparseints.
Sparseint-bitandc1
Compute the logandc1 of two sparseints.
Sparseint-bitand
Compute the logand of two sparseints.
Sparseint$-leaf-bitlimit
Limit on the size (in bits) of sparseint leaves.
Sparseint-bitxor
Compute the logxor of two sparseints.
Sparseint-bitorc2
Compute the logorc2 of two sparseints.
Sparseint-bitorc1
Compute the logorc1 of two sparseints.
Sparseint-bitor
Compute the logior of two sparseints.
Sparseint-bitnor
Compute the lognor of two sparseints.
Sparseint-bitnand
Compute the lognand of two sparseints.
Sparseint-biteqv
Compute the logeqv of two sparseints.
Sparseint-ash
Shift a sparseint by some amount, positive or negative
Sparseint-<
Check whether the value of x is less than the value of y.
Sparseint-bit
Extract the bit at the given index from a sparseint
Sparseint-trailing-1-count
Count the trailing consecutive 1s of a sparseint.
Sparseint-trailing-0-count
Count the trailing consecutive 0s of a sparseint.
Sparseint-unary-minus
Negate a sparseint.
Sparseint-length
Compute the integer-length of a sparseint. Returns an integer, not a sparseint.
Sparseint-bitnot
Bitwise negation of a sparseint
Sparseint-bitcount
Count the 1 bits in a sparseint if positive, 0 bits if negative.
Int-to-sparseint
Convert an integer into a sparseint.
Sparseint-val
Get the integer value of a sparseint