synth-loop-free-prog
Implementing Synthesis of Loop-free Programs by Gulwani et al in Rust, using the Z3 solver.
I explain the paper and walk through this implementation in my blog post Synthesizing Loop-Free Programs with Rust and Z3.
Example
use synth_loop_free_prog::*;
let mut builder = ProgramBuilder::new();
// ...build an unoptimized program...
let spec_program = builder.finish();
// Define a library of components that the synthesized program can use.
let library = Library {
components: vec![
component::add(),
component::sub(),
component::xor(),
component::shl(),
// etc...
],
};
let config = z3::Config::new();
let context = z3::Context::new(&config);
// Synthesize an optimized program!
let optimized_program = Synthesizer::new(&context, &library, &spec_program)
// One hour timeout.
.set_timeout(60 * 60 * 1000)
// Synthesize optimally small programs.
.should_synthesize_minimal_programs(true)
// Start synthesis!
.synthesize()?;
println!("Synthesized program:\n\n{}", optimized_program);Build
First, ensure that you have Z3 installed on your system:
# Something like this, depending on your OS.
$ sudo apt install libz3-devThen run
$ cargo buildTesting
$ cargo testRunning the Example Benchmarks
Run the all 25 benchmark programs from the paper (originally taken from Hacker's Delight) like this:
$ cargo run --example brahmaYou can also run only the ones that finish pretty quickly like this:
$ cargo run --example brahma -- --only-fastYou can see a full listing of the available options with:
$ cargo run --example brahma -- --helpLogging
Logging requires incoking cargo with --features log when building, running,
or testing.
At the debug log level, information about the progress of synthesis, the bit
width we're synthesizing at, and the example inputs is logged:
$ export RUST_LOG=synth_loop_free_prog=debugAt the trace level, every SMT query is additionally logged:
$ export RUST_LOG=synth_loop_free_prog=trace