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

[Sanjoy Das via Phabricator via llvm-commits]

sanjoy added inline comments.


================
Comment at: lib/Analysis/ScalarEvolution.cpp:8565
+
+      auto *Denum = getSCEV(LR);
+      assert(isa<SCEVConstant>(Denum) && "Denumerator must be a constant!");
----------------
It might be better to do `auto *Denum = cast<SCEVConstant>(getSCEV(LR))`.


================
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));
----------------
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.


https://reviews.llvm.org/D30887