[llvm] [InstSimplify] Simplify nonzero comparisons involving X urem Y via X u>= Y (PR #216072)

[Hadong Lee via llvm-commits]

================
@@ -3292,6 +3292,14 @@ static Value *simplifyICmpWithBinOpOnLHS(CmpPredicate Pred, BinaryOperator *LBO,
     }
   }
 
+  // (X - (X urem Y)) u>= 1 iff X u>= Y.
+  Value *X, *Divisor;
+  if (MaxRecurse && Pred == ICmpInst::ICMP_UGE && match(RHS, m_One()) &&
----------------
ChrisLee02 wrote:

Thanks for the guidance and detailed explanation of the existing simplification path!
I've updated the patch to match X and X urem Y in `isKnownNonEqual` and use `isImpliedByDomCondition`.

I've also updated the PR description and the Alive2 proof, and expanded the test coverage. Could you please take another look?

https://github.com/llvm/llvm-project/pull/216072