[PATCH] D30887: [ScalarEvolution] Predicate implication from operations

[Max Kazantsev via Phabricator via llvm-commits]

mkazantsev added inline comments.


================
Comment at: lib/Analysis/ScalarEvolution.cpp:8586
+      // Try to prove the following rule:
+      // (Denum <= FoundRHS + 1) && (RHS <= 0) => (LHS > RHS).
+      auto *Next = getAddExpr(FoundRHSExt, getOne(Ty2));
----------------
sanjoy wrote:
> Any reason why you need to check `Denum <= FoundRHS + 1` instead of `Denum < FoundRHS`?  Since `FoundRHS < FoundLHS`, `FoundRHS + 1` can't sign overflow, so the above two should be equivalent with `Denum < FoundRHS` being (slightly) faster since we're not adding.
> 
> Can you also add one or two lines of comment as an informal proof on why this is correct?
> 
> Same for the second rule.
Imagine Denum = 3, FoundRHS = 2. Denum <= FoundRHS + 1 is true, but Denum < FoundRHS is false. These two are not equivalent.

For example given that FoundRHS = 2. The given fact FoundLHS > 2 means that FoundLHS is at least 3. Then we can prove that FoundLHS / (2 + 1) is at least one. If we used you rule, we could only prove that FoundLHS / 1 > 0, which is a weaker statement.

I will add a comment on that proof.


https://reviews.llvm.org/D30887