search

OCamlPro / alt-ergo

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

chore(BV, CP): Refactor propagation mechanism #1185

Closed bclement-ocp closed 3 weeks ago

bclement-ocp commented 1 month ago

This patch simplifies the propagation mechanism (currently used in the bit-vector relations only) in order to accomodate different types of propagators more easily.

In particular, there is now a single generic (and configurable) loop that runs the propagators instead of a spaghetti of different loops for each kind of propagators.

Note: This PR depends on and includes #1152 and #1154. Only the commit titled "chore(BV, CP): Refactor propagation mechanism" (and later commits) are part of this PR.

Halbaroth commented 3 weeks ago

Please rebase and we can merge :)