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.
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...
The author is suggesting array languages as the solution, which are a separate category from functional languages.
I count ~8 different implementations [1], which demonstrates considerable commitment :) Personally, I prefer to write once with portable intrinsics.
https://github.com/simdutf/simdutf/tree/1d5b5cd2b60850954df5...
Portable instructions and “scalable” length-agnostic vectors are usually fine for straightforward mathy (type-1[2]) SIMD code. But real SIMD trickery, the one that starts as soon as you take your variable byte shuffle out of the stable, is rarely so kind.
[1] https://branchfree.org/2019/04/01/fitting-my-head-through-th...
[2] https://branchfree.org/2024/06/09/a-draft-taxonomy-of-simd-u...
The 2x128 is handled by adopting AVX2 semantics for our InterleaveLower/Upper op, and when we want the extra fixup, there is also InterleaveWholeLower. I agree AVX-512 is awesome, it's my favorite target. Some of its useful ops (compress[store]) are fine to emulate. What idioms did you have in mind that don't translate? Spot on about PMOVMSKB, that's a pain point. We provide several ops to replace it with more relaxed semantics that are easier to emulate on other platforms, for example AllTrue, CountTrue, AllFalse. (I think DanilaK's NEON VSHRN trick is faster than the one from your first link?)