search

OCamlPro / alt-ergo

OCamlPro public development repository for Alt-Ergo
https://alt-ergo.ocamlpro.com/
Other
131 stars 33 forks source link

feat(BV): Do not store width in Bitlist #1144

Closed bclement-ocp closed 2 months ago

bclement-ocp commented 3 months ago

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.

Note: depends on #1108, #1058, #1083, #1084, and #1085. Only the latest commit with title "feat(BV): Do not store width in Bitlist" is included in this PR.

bclement-ocp commented 3 months ago

This is +0-0 on QF_BV and slightly faster.