4 ms·

No? SMT solvers underpin the majority of program synthesis research tools. When you get down to it, you're optimizing (searching) for some program that maximiz

No? SMT solvers underpin the majority of program synthesis research tools. When you get down to it, you're optimizing (searching) for some program that maximizes/minimizes some objective function with terms for error relative to specification/examples and size of synthesized program, while applying some form of cleverness to pruning the search space. This is absolutely within the wheelhouse of SMT solvers, and something that they are used for. SMT doesn't have to be used, but for implementation it enables iterating on the concept more quickly (see also, more broadly: prototyping in Prolog), and in other cases it's simply the most effective tool for the job. So, it tends to get a lot of play.

throwawaymaths 2y ago
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.
- dzaima 2y ago
  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...

throwawaymaths 2y ago

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.

dzaima 2y ago
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...