Image created by stories
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.