[llvm] [ConstraintElim] Drop invalid rows instead of failing the elimination (PR #76299)

Nikita Popov via llvm-commits llvm-commits at lists.llvm.org
Wed Jan 3 01:04:05 PST 2024


nikic wrote:

> > Why is it valid to simply drop these rows? Doesn't this mean we lose constraints?
> 
> `sat` means that the constraint system _**may**_ have a solution. Returning `sat` for an inconsistent system is allowed. So it is safe to drop constraints.

I see. I think this should be spelled out in the eliminateUsingFM() documentation. If I understand correctly, the current implementation does preserve satisfiability during elimination (in the sense of "iff") -- but it's a stronger property than we need, so we can relax it, as this patch does. Or is it already possible for the current eliminateUsingFM() implementation to turn an unsat system into a sat one?

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


More information about the llvm-commits mailing list