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

[Philip Reames via Phabricator via llvm-commits]

reames requested changes to this revision.
reames added inline comments.
This revision now requires changes to proceed.


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


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

https://reviews.llvm.org/D88208