search

OCamlPro / alt-ergo

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

feat(BV): Add support for bv2nat/int2bv normal forms #1154

Open bclement-ocp opened 2 weeks ago

bclement-ocp commented 2 weeks ago

Currently, Alt-Ergo knows the value of [bv2nat] and [int2bv] on constants. We also perform some simplifications during semantic value creation; however, these simplifications are not integrated into the rest of the solver. For instance, we know that [bv2nat(x @ y)] is equal to [bv2nat(x) * 2^n + bv2nat(y)] (where [n] is the bit-width of [y]), but we don't know that [z] is equal to the same under the hypothesis that [z = x @ y].

This patch moves these simplifications to the [Bitv_rel] module, making them an integral part of the solving process. Since we can't compute [bv2nat] (or [int2bv]) of an arbitrary semantic value, we generate fresh variables to represent them when needed.

Note: this PR depends on #1144 and #1152. Only the last commit titled "feat(BV): Add support for bv2nat/int2bv normal forms" is included in this PR.

bclement-ocp commented 1 week ago

Fixes #824

(I don't know why it does not appear in the "Development" dropdown...)