Libraries for reasoning about bit vectors.
- Alternative implementation of bignums based on balanced binary trees
- Bitops is a library originally developed at Centaur Technology
for reasoning about bit-vector arithmetic. It grew out of an extension
to the venerable ACL2::ihs library, and is now fairly comprehensive.
- The BV library for reasoning about bit-vectors
- The Integer Hardware Specification (IHS) library is a collection of
arithmetic books, mainly geared toward bit-vector arithmetic.
- A library of register-transfer logic and computer arithmetic