feat(BV): Do not store width in Bitlist

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.