@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.
-
Ok interesting. Thanks for sharing your program. I was puzzling over how one would express this in z3 (synthesizing RISC-V immediate decode programs) and thought the problem space was large. I see you add 3 instructions (syn.addcommand(...)) in make_riscv_b.py.
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.
Thanks. Twitter will use this to make your timeline better. UndoUndo
-
Loading seems to be taking a while.
Twitter may be over capacity or experiencing a momentary hiccup. Try again or visit Twitter Status for more information.