# 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.