[llvm] [InstCombine] Simplify fractions when there is no overflow (PR #92949)

via llvm-commits llvm-commits at lists.llvm.org
Fri May 24 10:06:21 PDT 2024


goldsteinn wrote:

> Anyway, in addition to the Alive2 proof, in the event I messed up there, here is how if a multiplication followed by a division does not have an unsigned wrap, a reduced fraction does:
> 
The alive2 proofs are way to complicated. I don't think they really serve the purpose of avoiding bugs, as even though they verify, its not clear they don't have bugs in them.

 I would suggest instead of implementing GCD, pass an additional argument and setup assumes s.t `GCD >= 1 && mulC % GCD == 0 && divC % GCD % 0`.

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


More information about the llvm-commits mailing list