computing 
, bicycles 
, hiphop 
, books 
, pen plotters 
, he/him
U tweetove putem weba ili aplikacija drugih proizvođača možete dodati podatke o lokaciji, kao što su grad ili točna lokacija. Povijest lokacija tweetova uvijek možete izbrisati. Saznajte više
blogged: Synthesizing Loop-Free Programs w/ Rust and Z3! Writing Programs That Write Other Programs!! https://fitzgeraldnick.com/2020/01/13/synthesizing-loop-free-programs.html …
This post introduces program synthesis, and explains counterexample-guided iterative synthesis of component-based programs, based on "Synthesis of Loop-Free Programs" by Gulwani et al. Finally, we walk through an implementation written in Rust, using the Z3 solver.
I hope that folks who are unfamiliar w/ program synthesis, just like I was not too long ago, find this enlightening. I've done my best to make it approachable by providing lots of examples, breaking all the formulas down, and explaining each bit:pic.twitter.com/GCdtdjuxkK
I also hope I can nerd snipe some folks who are already familiar with this stuff into helping me diagnose why my synthesizer can't find solve some of the harder Hacker's Delight benchmark problems. Am I missing well-known optimizations? See impl and results sections for details
Thanks for such a thought provoking read. My own excursions into code synthesis in Rust (finding a 32 instruction loop in 6502 to force a DMA heavy c64 graphics mode) have thus far just been implemented as a (tightly pruned) depth first search.
Your explanation of CEGIS is excellent; I suspect I have a use for it for another problem I've been meaning to wrote a solver for.
Pretty cool!
Thank you for that extensive writeup. Really enjoyed reading through it. Program synthesis is an interesting field.
Twitter je možda preopterećen ili ima kratkotrajnih poteškoća u radu. Pokušajte ponovno ili potražite dodatne informacije u odjeljku Status Twittera.
