Skip to content

Commit

Permalink
feat(BV): Do not store width in Bitlist (#1144)
Browse files Browse the repository at this point in the history
This patch rewrites the Bitlist module to represent infinite-width
bit-vectors rather than fixed-width bit-vectors, making it able to
represent unbounded integers. This improves the symmetry with the
interval domain (which also applies to unbounded integers) and is
intended to simplify the implementation of BV-to-int and int-to-BV
conversions.

In order to avoid having to use negative numbers in bitlists, the
internal representation is changed from a pair of (bits equal to [1],
bits equal to [0]) masks to a pair (bits equal to [1], unknown bits)
masks. This change should also be good for memory consumption, as we no
longer keep two copies of the value around when all bits are known.
  • Loading branch information
bclement-ocp authored Jul 8, 2024
1 parent 9c0bfa3 commit a7cf228
Show file tree
Hide file tree
Showing 4 changed files with 354 additions and 289 deletions.
Loading

0 comments on commit a7cf228

Please sign in to comment.