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

via llvm-commits llvm-commits at lists.llvm.org
Fri May 24 19:19:01 PDT 2024


AtariDreams 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`.

GCD being one means we will loop forever because every number that isn't zero has a common denominator of 1 with another

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


More information about the llvm-commits mailing list