|
|
|---|
|
|
|
|---|
Optimized function for selecting a bit range from a big integer.
Suppose you have a large (perhaps millions of bits) bignum, and you
want to extract a small range (maybe only a few thousand bits) from somewhere
in the middle. Using regular ACL2 primitives like logand and ash, you don't
have any good options that don't require copying a much larger portion of the
number. You either have to truncate the big number to the end of the range you
want (which may yield a large bignum) and then shift it into place, or else
shift the lowest bit into place (which may yield a large bignum) and then
truncate it to the width you want. One option requires making a new bignum
that is
Fast-part-select is based on bitsets::bignum-extract, which extracts a 32-bit slice from a bignum. It has an optimized implementation on CCL that simply grabs the appropriate array element from within the bignum representation. Fast-part-select stitches together the required range from these 32-bit slices. It isn't particularly efficient if the width of the selection is large, but it is independent of the width of the input integer from which we're selecting and the bit offset at which we're selecting.
It's kind of a pity to have to use this; it would be nice if Lisps had
efficient implementations of the Common Lisp
Note: For good performance, it is important to use the raw Lisp definition of bignum-extract, loaded by including the book "std/bitsets/bignum-extract-opt".
See also fast-part-extend, which performs the same operation but returns the range sign-extended instead of zero-extended.
Function:
(defun fast-part-select$inline (x width low) (declare (type integer x) (type (integer 0 *) width) (type (integer 0 *) low)) (declare (xargs :guard (and (integerp x) (natp width) (natp low)))) (declare (xargs :split-types t)) (let ((__function__ 'fast-part-select)) (declare (ignorable __function__)) (mbe :logic (part-select-width-low x width low) :exec (b* ((width (lnfix width)) (low (lnfix low)) ((when (eql width 0)) 0) (low-slice (ash low -5)) (low-omit (logand 31 low)) (high (+ -1 low width)) (high-slice (ash high -5)) (high-omit (- 31 (logand 31 high))) (slices (+ 1 (- high-slice low-slice)))) (fast-psel x low-slice slices low-omit high-omit)))))