If Y is nonzero we can simplify the ge/le > gt/lt
(X ^ Y_NonZero) u>= X > (X ^ Y_NonZero) u> X
(X ^ Y_NonZero) u<= X > (X ^ Y_NonZero) u< X
(X ^ Y_NonZero) s>= X > (X ^ Y_NonZero) s> X
(X ^ Y_NonZero) s<= X > (X ^ Y_NonZero) s< X
Differential D144608
[InstCombine] Add transforms for `(icmp {us}ge/le (xor X, Y), X)` goldstein.w.n on Feb 22 2023, 5:20 PM. Authored by
Details If Y is nonzero we can simplify the ge/le > gt/lt (X ^ Y_NonZero) u>= X > (X ^ Y_NonZero) u> X (X ^ Y_NonZero) u<= X > (X ^ Y_NonZero) u< X (X ^ Y_NonZero) s>= X > (X ^ Y_NonZero) s> X (X ^ Y_NonZero) s<= X > (X ^ Y_NonZero) s< X
Diff Detail
Event TimelineComment Actions This is adding a lot of code to a function that's already too big. A helper function will make it easier to read. This seems like 2 or 3 independent patches? I just looked at the first group of 4 Alive proofs, and those seem fine.
