Rust and Z3 Team Up to Synthesize Loop-Free Programs

Synthesizing Loop-Free Programs with Rust and Z3 (2020)

Program synthesis automatically finds a program from a specification, but the search space is huge. This post explains counterexample-guided iterative synthesis of component-based, loop-free programs, based on Gulwani et al.'s paper. It walks through a Rust implementation using the Z3 solver, with examples like isolating the rightmost zero bit. The author hopes to help newcomers understand the topic and invites experts to diagnose performance issues where the synthesizer fails to match published results.