This patch exposes constraint simplification as an explicit primitive, instead of performing simplification implicitly during substitutions.
This is preparatory work to represent constraints in a more generic way, allowing to limit boilerplate when adding new constraints (e.g. for arithmetic operations on bit-vectors), which is easier to do if substitution and simplification are separate operations.
Note that constraint simplification (both the existing implementation and the new one in this patch) can currently only occur based on the underlying semantic values; the domains are not available at the time simplification is performed. Allowing to perform simplification based on domains is left to a future patch.
This patch exposes constraint simplification as an explicit primitive, instead of performing simplification implicitly during substitutions.
This is preparatory work to represent constraints in a more generic way, allowing to limit boilerplate when adding new constraints (e.g. for arithmetic operations on bit-vectors), which is easier to do if substitution and simplification are separate operations.
Note that constraint simplification (both the existing implementation and the new one in this patch) can currently only occur based on the underlying semantic values; the domains are not available at the time simplification is performed. Allowing to perform simplification based on domains is left to a future patch.
Note: This depends on (and includes) https://github.com/OCamlPro/alt-ergo/pull/1044, https://github.com/OCamlPro/alt-ergo/pull/1054, and #1055; only the last commit titled "feat(BV,CP): Explicit constraint simplification" is new.