Commits on Jun 28, 2024

1. feat(BV, CP): Add propagators for bvshl and bvlshr …

   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 committed Jun 28, 2024
   Configuration menu

   • View commit details
   • Copy full SHA for 32a3e5f
   • Browse repository at this point

   Copy the full SHA

   32a3e5f View commit details

   Browse the repository at this point in the history