@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.
-
I’m curious how
@oe1cxw created RISC-V instruction decoders using z3 descriptions of bit manipulation intrinsics. Seems to require “column generation” as the number of instructions is not known a priori. V.clever. This example uses conditional holes: https://www.cs.cornell.edu/~asampson/blog/minisynth.html …
I'm usually not using z3 but yices2 and boolector. They are many many times faster for the kind of problems I'm looking at. I've never built a risc-v insn decoder for program synthesis. Usually that's one abstraction level up, see for example http://svn.clifford.at/handicraft/2018/xbitpermsyn/ ….
-
-
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
- Show replies
New conversation -
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.