@johnregehr Are there good papers with details on the SMT formulation of CEGIS for superoptimization aside from Gulwani et al and the Souper paper itself (and source)?
The whole thing seems alarmingly.. magical. I feel like an ape poking the monolith with a stick when I use Z3.
-
This Tweet is unavailable.
-
This Tweet is unavailable.
-
Yes. This only looks at programs with three sequential instructions, each one of them can be rori, grevi, or gzip (gzip is the old name for shfli/unshfli). This program produces a permutation that has the imm bits in the right order but interleaved with other bits. -> bext
I'd love to be able to also generate things like that bext and the final shifts with a solver, but solving for the 2nd parameter of bext is a pretty hard smt problem, in part because I am not aware of any efficient smt encoding for the bext operation.
