[all-commits] [llvm/llvm-project] 51a2f5: [mlir][affine] fix the issue of ceildiv-mul-ceildi...

[long.chen via All-commits]

  Branch: refs/heads/main
  Home:   https://github.com/llvm/llvm-project
  Commit: 51a2f50ee76a52d4a542822bfda9c4c17904b72f
      https://github.com/llvm/llvm-project/commit/51a2f50ee76a52d4a542822bfda9c4c17904b72f
  Author: long.chen <lipracer at gmail.com>
  Date:   2024-10-12 (Sat, 12 Oct 2024)

  Changed paths:
    M mlir/lib/IR/AffineExpr.cpp
    M mlir/test/Dialect/Affine/simplify-structures.mlir

  Log Message:
  -----------
  [mlir][affine] fix the issue of ceildiv-mul-ceildiv form expression not satisfying commutative (#111254)

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



To unsubscribe from these emails, change your notification settings at https://github.com/llvm/llvm-project/settings/notifications