Member-only story
Programming in Z3 by learning to think like a compiler
Programming in logic can help you produce better optimized, more secure, bug-free code … if only you knew how to do it.
It took me about two years to write my first program in Z3. I had done some tutorials, wrote code to solve other people’s example puzzles, but I couldn’t really figure out how to cross over from very abstract “toy” use cases to applications that had actual relevance.
Z3 is a Satisfiability modulo theories (SMT) solver, a cousin to the satisfiability (SAT) solvers I’ve written about before. Whereas SAT solvers require encoding everything in to a set of True/False statements, SMT solvers allow for greater expressiveness. In plain SAT you can represent addition by representing numbers in binary and performing logic operations to produce the correct sum. After all, that’s the way the CPU processes everything. If this concept is completely foreign to you, I recommend looking at NAND to Tetris as a great way of exploring how logic gates get built up into complex processors.
In SMT, however, you can just write 2+2 as 2+2, because SMT builds in those abstractions (called “theories”) … basically: just as a programming language like python will let you write things in neat, English looking phrases because it understands how to convert those phrases into the machine code old school programmers had to contend with, SMT solvers let people write neater models because it understands how to convert 2+2 into logic.
There are two main ways theories work in SMT. The first is essentially just compiling to the SAT equivalent and executing it as one large SAT. The second approach encapsulates those non-Boolean specific sections of the model into a SAT problem inside the SAT to be handled separately. The benefit of the second approach is greater efficiency around questions like: x + y = y + x
All of that is super cool and completely useless if you can’t figure out how to represent your problem in logic + arithmetic. And much of what programmers do doesn’t look like logic + arithmetic … at least not at first glance.
Think Like a Compiler
I learn a lot from attempting to learn other things and this was one of those situations. I had given up trying to understand how to…
