https://www.cs.cornell.edu/~asampson/blog/minisynth.html Program Synthesis is Possible MAY 9, 2018 Program synthesis is not only a hip session title at programming languages conferences. It’s also a broadly applicable technique that people from many walks of computer-science life can use. But it can seem like magic: automatically generating programs from specifications sounds like it might require a PhD in formal methods. Wisconsin’s Aws Albarghouthi wrote a wonderful primer on synthesis last year that helps demystify the basic techniques with example code. Here, we’ll expand on Aws’s primer and build a tiny but complete-ish synthesis engine from scratch. You can follow along with my Python code or start from an empty buffer. Z3 is Amazing We won’t quite start from scratch—we’ll start with Z3 and its Python bindings. Z3 is a satisfiability modulo theories (SMT) solver, which is like a SAT solver with theories that let you express constraints involving integers, bit vectors, floating point numbers, and what have you. We’ll use Z3’s Python bindings. Let’s try it out:
import z3
To use Z3, we’ll write a logical formula over some variables and then solve them to get a model, which is a valuation of the variables that makes the formula true. Here’s one formula, for example:
formula = (z3.Int('x') / 7 == 6)
The z3.Int call introduces a Z3 variable. Running this line of Python doesn’t actually do any division or equality checking; instead, the Z3 library overloads Python’s / and == operators on its variables to produce a proposition. So formula here is a logical proposition of one free integer variable, x, that says that x / 7 = 6. Let’s solve formula. We’ll use a little function called solve to invoke Z3: def solve(phi): s = z3.Solver() s.add(phi) s.check() return s.model() Z3’s solver interface is much more powerful than what we’re doing here, but this is all we’ll need to get the model for a single problem:
print(solve(formula))
On my machine, I get: [x = 43] which is admittedly a little disappointing, but at least it’s true: using integer division, 43 \/ 7 = 6. Z3 also has a theory of bit vectors, as opposed to unbounded integers, which supports shifting and whatnot:
y = z3.BitVec('y', 8) print(solve(y << 3 == 40))
There are even logical quantifiers:
z = z3.Int('z') n = z3.Int('n') print(solve(z3.ForAll([z], z * n == z)))
Truly, Z3 is amazing. But we haven’t quite synthesized a program yet. Sketching In the Sketch spirit, we’ll start by synthesizing holes to make programs equivalent. Here’s the scenario: you have a slow version of a program you’re happy with; that’s your specification. You can sort of imagine how to write a faster version, but a few of the hard parts elude you. The synthesis engine’s job will be fill in those details so that the two programs are equivalent on every input. Take Aws’s little example: you have the “slow” expression x * 2, and you know that there’s a “faster” version to be had that can be written x << ?? for some value of ??. Let’s ask Z3 what to write there:
x = z3.BitVec('x', 8) slow_expr = x * 2 h = z3.BitVec('h', 8) # The hole, a.k.a. ?? fast_expr = x << h goal = z3.ForAll([x], slow_expr == fast_expr) print(solve(goal))
Nice! We get the model [h = 1], which tells us that the two programs produce the same result for every byte x when we left-shift by 1. That’s (a very simple case of) synthesis: we’ve generated a (subexpression of a) program that meets our specification. Without a proper programming language, however, it doesn’t feel much like generating programs. We’ll fix that next. ............. it's discouraging that the examples so far do not generate code other than variables. still seeming like the first julia library is more accessible. above python library is at https://github.com/sampsyo/minisynth