[Mlir-commits] [mlir] [mlir][affine] fix the issue of ceildiv-mul-ceildiv form expression n… (PR #111254)

[llvmlistbot at llvm.org]

lipracer wrote:

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.



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