Re:C Is Not Suited to SIMD
by throwawaymaths on Tuesday January 28, 2025 @11:45AM
(#42854475)
If SMT solvers were all you needed, then for example, LLVM wouldn't need a polyhedral optimizer. And a polyhedral optimizer is a subset of the sorts of things you will need for doing the sort of things you're asking to do automatically.
[ Parent
| on HN ]
SMT solvers might not be feasible for large-scale things, but they can certainly be used to find a sequence of a couple instructions doing a specific thing if you give enough computational resources, and that's what OP was talking about. (whether it'll complete in a reasonable time (i.e. less than like an hour) for something with more than like 4 instructions is a separate question; but 4 instructions is enough for some fancy stuff).
Like, just playing around not particularly seriously, I've gotten SMT to spit out [1] for narrowing & packing four int32x8 vectors into one int8x32 vector, assuming no wrapping necessary (4 minutes via Bitwuzla), among other things; nothing one couldn't figure out by doing a bit of thinking, but it does work! And could conceivably get more feasible for larger tasks over time.
[1]: https://dzaima.github.io/paste/#0KytITM4uLi5PUqjMzTXRAZEGYNK...