This patch adds interval and bitlist propagators for the bvshl (left
shift) and bvlshr (logical right shift) in the intervals and bitlist
domains for bit-vectors.
The interval propagator for left shift needs to be written specially in
order to properly deal with overflow, but the propagator for bvlshr is
written using a generic propagator for (bi)-monotone functions.
The bitlist propagator for bvshl is required because it needs to
propagate information regarding low bits that are not tracked by
intervals. However, I am not sure that the bitlist propagator for bvlshr
is actually needed since it might be subsumed by the interval propagator
for bvlshr (and consistency constraints) entirely, and we might want to
remove it.
bclement-ocp
commented
3 months ago
This patch adds interval and bitlist propagators for the bvshl (left shift) and bvlshr (logical right shift) in the intervals and bitlist domains for bit-vectors.
The interval propagator for left shift needs to be written specially in order to properly deal with overflow, but the propagator for bvlshr is written using a generic propagator for (bi)-monotone functions.
The bitlist propagator for bvshl is required because it needs to propagate information regarding low bits that are not tracked by intervals. However, I am not sure that the bitlist propagator for bvlshr is actually needed since it might be subsumed by the interval propagator for bvlshr (and consistency constraints) entirely, and we might want to remove it.
Note: this requires and currently includes https://github.com/OCamlPro/alt-ergo/pull/1058, https://github.com/OCamlPro/alt-ergo/pull/1083 and #1084 ; the commit titled " feat(BV, CP): Add propagators for bvshl and bvlshr" is new.