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

[Max Kazantsev via Phabricator via llvm-commits]

mkazantsev marked an inline comment as done.
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:
> mkazantsev wrote:
> > 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.
> Yes, you're right -- they're not equivalent.  I think I confused it with `Denum + 1 <= FoundRHS`.
> 
> On the other hand, can we write the condition as `(Denum - 1) <= FoundRHS`?  Again, we know that `Denum - 1` won't sign overflow, and computing `(Denum - 1)` may be faster than computing `FoundRHS + 1` because `Denum` is a constant.
Indeed, this makes sense. Will do.


https://reviews.llvm.org/D30887