https://gcc.gnu.org/bugzilla/show_bug.cgi?id=118994
--- Comment #6 from Hongtao Liu <liuhongt at gcc dot gnu.org> --- (In reply to John Platts from comment #5) > GCC also fails to optimize (a | b) - ((a ^ b) >> 1) down to a single SSE2 > PAVGB/PAVGW, NEON/SVE2 SRHADD/URHADD, AltiVec > vavgsb/vavgsh/vavgsw/vavgub/vavguh/vavguw instruction where supported on the > target, but Clang will optimize (a | b) - ((a ^ b) >> 1) down to > PAVGB/PAVGW/SRHADD/URHADD where available on the target according to a > snippet over at https://godbolt.org/z/Yz8fEW46f. I asked grok3 if ((a | b) - ((a ^ b) >> 1) always equals to (a + b + 1) >> 1, and get positive answer. I verified the reasoning process and it seems to be fine. Theoretical Analysis To generalize, we expressed the first expression using identities: a | b = a + b - a & b (where & is bitwise AND), derived from set theory and verified numerically. a + b = a ^ b + 2*(a & b), reflecting binary addition without carry. Let c = a + b, d = a & b. Then: First expression: c - d - ((c - 2*d) >> 1) Second expression: (c + 1) >> 1 We analyzed two cases based on a ^ b's parity: a ^ b is even: Then c - 2d is even, implying c is even (since 2d is even, c must be even for difference to be even). The first expression simplifies to c/2, and the second is floor((c + 1)/2) = c/2 (when c is even, as floor((even + 1)/2) = even/2). a ^ b is odd: Then c - 2d is odd, implying c is odd. The first expression becomes c - d - floor((c - 2d)/2), simplifying to (c + 1)/2, and the second is floor((c + 1)/2) = (c + 1)/2 (since c is odd, c + 1 is even, division is exact). In both cases, the expressions are equal, confirming the equality for non-negative integers. For negative integers, as long as it's arithmetic shift, The equation still holds.
