search

OCamlPro / alt-ergo

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

feat(BV, CP): Propagators for addition and multiplication #1083

Closed bclement-ocp closed 2 months ago

bclement-ocp commented 5 months ago

This patch adds constraints to represent bit-vector addition and multiplication, with propagators in the interval domain and a simple propagator for multiplication that only considers the factors-of-two multiples in the bit-vector domain (this information cannot be captured by the interval domain due to imprecise handling of overflow).

No propagator for addition in the bit-vector domain is provided yet, although the plan is to add a full-adder propagator to provide a limited form of local bit-blasting, as suggested in

S. Bardin, P. Herrmann, and F. Perroud. “An Alternative to SAT-Based Approaches for Bit-Vectors”. In: TACAS. 2010.

Note: this requires and currently includes #1058 ; the commit titled "feat(BV, CP): Propagators for addition and multiplication" is new.

bclement-ocp commented 3 months ago

Rebased with the new Intervals module from #1108

Halbaroth commented 2 months ago

Can you rebase this PR please? I will review it today :)

bclement-ocp commented 2 months ago

I don't understand why GitHub was saying there were merge conflicts in a bunch of files there were none? I force pushed again and that seems to have solved it.