[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