Std/bitsets
Optimized libraries for representing finite sets of natural numbers
using bit masks, featuring a strong connection to the std/osets library.
Introduction
The std/bitsets library offers two ways to represent sets of natural
numbers.
- bitsets—plain bitsets—each set is encoded as a
single bit-mask, i.e., using a single natural number. This representation is
particularly efficient for sets of very small numbers but cannot cope well with
large elements.
- sbitsets—sparse bitsets—each set is encoded as an
ordered list of offset/block pairs, each block being a bit-mask for
60 elements. This representation is more forgiving; it
can handle larger sets, perhaps with very large elements, and still achieves
bitset-like efficiencies in many cases.
Either representation provides a nice set-level abstraction that should
shield you from reasoning about the underlying bitwise arithmetic operations;
see reasoning.
Loading the Library
To load everything (except for optimizations that require trust tags):
(include-book "std/bitsets/top" :dir :system)
Alternately, for just the plain bitset library:
(include-book "std/bitsets/bitsets" :dir :system)
Or for just the sparse bitsets library:
(include-book "std/bitsets/sbitsets" :dir :system)
Optional Optimizations
You may be able to substantially speed up the bitset-members
operation for large sets, perhaps especially on CCL, by loading an optimized,
raw Lisp definition:
(include-book "std/bitsets/bitsets-opt" :dir :system)
See ttag-bitset-members and bignum-extract for details.
Subtopics
- Bitsets
- Bitsets library: uses bitmasks to represent finite sets of (small)
natural numbers.
- Sbitsets
- Sparse bitsets library: an alternative to bitsets for
representing finite sets of natural numbers.
- Reasoning
- How to reason about bitsets.
