mirror of
https://github.com/llvm/llvm-project.git
synced 2025-04-24 15:26:24 +00:00
51a2f50ee7
my prove: we can simple `(n * s) ceildiv a ceildiv s` to `n ceildiv a` because `(n * s) ceildiv a ceildiv b` <=> `(n * s) ceildiv s ceildiv a` <=> `n ceildiv a` let's prove the `s floordiv a floor b` <=> `s floordiv b floor a` let `s = ka +m (m < a)` so `s floordiv a` <=> `s / a - m / a` similarly, it can be proven that: `s floordiv a floordiv b` <=> `s / (a * b) - m / (a * b) - n / (b) constrain (n < b)` <=> `s / (a * b) - (m + a*n) / (a*b)` because `a* b - (m + a*n)` <=> `a*b - a*n - m` > `a - m` > `0` so `s floordiv a floordiv b` <=> `[s / (a*b)]` <=> `s floordiv b floordiv a` but if `s floordiv b` mutiply a factor above didn't always hold true. Fixes https://github.com/llvm/llvm-project/issues/107508