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…