This patch consolidates the representation for bit-vector constraints in order to separate the operator (e.g. Band) from its arguments. While this has some initial overhead in terms of code to be written, it allows sharing boilerplate code (such code for as substitution and argument folding) across multiple operators, making it easier to add new propagators (e.g. arithmetic bit-wise operators) in the future.
This patch consolidates the representation for bit-vector constraints in order to separate the operator (e.g.
Band) from its arguments. While this has some initial overhead in terms of code to be written, it allows sharing boilerplate code (such code for as substitution and argument folding) across multiple operators, making it easier to add new propagators (e.g. arithmetic bit-wise operators) in the future.Note: This depends on (and includes) https://github.com/OCamlPro/alt-ergo/pull/1044, https://github.com/OCamlPro/alt-ergo/pull/1054, https://github.com/OCamlPro/alt-ergo/pull/1055, and #1056 ; only the last commit titled "feat(BV): Generic constraint representation" is new.