This patch adds propagators on the bitlist domain for addition and
subtraction. These propagators are able to compute low bits
independently of high bits; in particular, we now know that the sum of
two even (or two odd) numbers is even.
If there is a bit pattern that prevents carry propagation (e.g. two [0]s
for addition), we are also able to compute the following bits precisely.
Note that we do not currently decompose addition/subtraction according
to these propagators -- for instance, we do not know that
(bvadd (concat x #b0) (concat y #b0)) is (concat (bvadd x y) #b0).
This patch adds propagators on the bitlist domain for addition and subtraction. These propagators are able to compute low bits independently of high bits; in particular, we now know that the sum of two even (or two odd) numbers is even.
If there is a bit pattern that prevents carry propagation (e.g. two [0]s for addition), we are also able to compute the following bits precisely.
Note that we do not currently decompose addition/subtraction according to these propagators -- for instance, we do not know that
(bvadd (concat x #b0) (concat y #b0))is(concat (bvadd x y) #b0).Note: depends on https://github.com/OCamlPro/alt-ergo/pull/1058, https://github.com/OCamlPro/alt-ergo/pull/1083, https://github.com/OCamlPro/alt-ergo/pull/1084, https://github.com/OCamlPro/alt-ergo/pull/1085, and #1144. Only the latest commit with title "feat(CP): Add bitlist propagators for add/sub" is included in this PR.