2 ms·

So just use a SAT solver to check for checking whether pattern matching is exhaustive. Any decent one will have much better performance than the current approac

by not2b 5y ago

So just use a SAT solver to check for checking whether pattern matching is exhaustive. Any decent one will have much better performance than the current approach in the Rust compiler for complex cases. The interesting thing about SAT is that although the worst case is exponential (as far as we know until someone proves P = NP), even huge real-life problems (from circuits, program analysis etc) tend to have structure that makes them quickly solvable with a SAT solver. And if not, have a time budget and report "too complex to solve" if exceeded.

thaunatos 5y ago
It's worth noting that the author of the arcicle doesn't think it's worth integrating a SAT solver: > Does this mean that rustc should integrate an industrial-strength SAT solver? As hilarious as that would be, I'm advocating no such thing. This will only be a performance issue on pathological examples crafted by bored nerds, and I don't think precious engineering time should be spent on that. Besides, generalizing a SAT algorithm to handle the full expressive power of Rust's patterns might be, to borrow some language from mathematicians, non-trivial.