[PATCH] D88208: [SCEV] Prove implicaitons via AddRec start

[Max Kazantsev via Phabricator via llvm-commits]

mkazantsev added inline comments.


================
Comment at: llvm/lib/Analysis/ScalarEvolution.cpp:9892
+    const SCEV *FoundLHS, const SCEV *FoundRHS) {
+  // {X,+,1} < Y implies X < Y, and {X,+,-1} > Y implies X > Y.
+  // {X,+,C} != Y implies X != Y and {X,+,C} == Y implies X == Y if Y is a
----------------
reames wrote:
> If Y is loop invariant, this obviously follows.  And the more general form of (X,+,W) < Y ==> X < Y would also hold.
> 
> I'm struggling to convince myself this holds when Y is an arbitrary loop varying scev.  I haven't found a counter example yet.
> 
> Could I ask you to split this into two patches?  One for the invariant case since that's easy to reason about, and one for the varying Y case?  I both want to think about that separately and have an easy patch to revert if needed.
Do we need this for varying Y case?


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

https://reviews.llvm.org/D88208