[PATCH] D88087: [SCEV] Limited support for unsigned preds in isImpliedViaOperations

[Max Kazantsev via Phabricator via llvm-commits]

mkazantsev added a comment.

Let me elaborate a bit.

We are trying to prove `LHS >u RHS`, knowing that `FoundLHS >u FoundRHS`. We want to somehow reduce this to an equivalent `>s` proof.

You are correct that if we know that all `LHS`, `RHS`, `FoundLHS` and `FoundRHS` are non-negative, we can simply call `isImpliedViaOperations(>s, LHS, RHS, FoundLHS, FoundRHS)`.

However, we might not be able to prove `isKnownNonNegative(LHS)` or `isKnownNonNegative(RHS)`. Imagine the case when we have proved `isKnownNonNegative(FoundLHS)` and `isKnownNonNegative(FoundRHS)`, but cannot do so for neither `LHS` nor `RHS`. In this case (and this is what my patch is about), we should try to infer non-negativity of `LHS` and `RHS` from `FoundLHS > FoundRHS`. And the way to do it is to call `isImpliedViaOperations(>s, LHS, -1, FoundLHS, FoundRHS)` and `isImpliedViaOperations(>s, RHS, -1, FoundLHS, FoundRHS)`. What you proposed is just a subset of what can be proved with implication.

I can split this change into two pieces: first piece with trivially provable non-negativity of `LHS` and `RHS`, and the second case is when we cannot prove this trivially and should use implication. Does it make sense now?


CHANGES SINCE LAST ACTION
  https://reviews.llvm.org/D88087/new/

https://reviews.llvm.org/D88087