Bvec
Internal representations of symbolic bit vectors.
GL's core symbolic arithmetic functions operate on lists of bfrs, which may be interpreted either as signed or unsigned symbolic
integers.
For unsigned bit vectors this is entirely straightforward. We use an
LSB-first encoding of the bits, so the car of a BFR list represents the
least significant bit of the natural number, a la logcar, whereas the
cdr of the BFR represents its more significant bits, a la logcdr.
For signed bit vectors, we use a similar encoding except that we interpret
the final bit of the number as the sign bit. So, when working on a signed bit
vector, we generally use scdr instead of just cdr.
Subtopics
- Scdr
- Like logcdr for signed bvecs.
- Bfr-list->s
- Signed interpretation of a BFR list under some environment.
- Bfr-eval-list
- Evaluate a list of BFRs, return the list of the (Boolean) results.
- Bfr-scons
- Like logcons for signed bvecs.
- Bfr-ucons
- Like logcons for unsigned bvecs.
- Bfr-list->u
- Unsigned interpretation of a BFR list under some environment.
- Bfr-sterm
- Promote a single BFR into a signed, one-bit bvec, i.e., the resulting
value under bfr-list->s is either 0 or -1, depending on the
environment.
- Bfr-snorm
- Pbfr-list-depends-on
- V2i
- Convert a (pure constant) signed bvec into an integer.
- N2v
- Convert a natural into a corresponding unsigned bvec (with constant bits).
- V2n
- Convert an unsigned bvec into the corresponding natural.
- S-endp
- Are we at the end of a signed bit vector?
- I2v
- Convert an integer into a corresponding signed bvec (with constant bits).
- First/rest/end
- Deconstruct a signed bit vector.
- Bool->sign
- Interpret a sign bit as an integer: true → -1, false → 0.
