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 y

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/#0KytITM4uLi5PUqjMzTXRAZEGYNKYqwxZyhQsaAgmjVClzHQQek2BUqlFuSl6mUUgrrmOgkGFAQSYQ2ljKG0KpQ2htIkBKjCD0kYKNkY6ZjoGOiY6hjqmOsY65nZgq8wA#asm https://dzaima.github.io/paste/#0KytITM4uLi5PUqjMzTXRAZEGYNK...