For the pattern `(zext i1 X) + (sext i1 Y)`, the constant range is [-1, 1].

We can simplify the pattern by logical operations. Like:

(zext i1 X) + (sext i1 Y) == -1 --> ~X & Y (zext i1 X) + (sext i1 Y) == 0 --> ~(X ^ Y) (zext i1 X) + (sext i1 Y) == 1 --> X & ~Y

And other predicates can the combination of these results:

(zext i1 X) + (sext i1 Y)) != -1 --> X | ~Y (zext i1 X) + (sext i1 Y)) s> -1 --> X | ~Y (zext i1 X) + (sext i1 Y)) u< -1 --> X | ~Y (zext i1 X) + (sext i1 Y)) s> 0 --> X & ~Y (zext i1 X) + (sext i1 Y)) s< 0 --> ~X & Y (zext i1 X) + (sext i1 Y)) != 1 --> ~X | Y (zext i1 X) + (sext i1 Y)) s< 1 --> ~X | Y (zext i1 X) + (sext i1 Y)) u> 1 --> ~X & Y

All alive proofs:

https://alive2.llvm.org/ce/z/KmgDpF

https://alive2.llvm.org/ce/z/fLwWa9

https://alive2.llvm.org/ce/z/ZKQn2P