As part of writing Logic for Programmers I produced a lot of “chaff”, code samples and sections I wrote up and then threw away. Sometimes I found a better example for the same topic, sometimes I threw the topic away entirely. It felt bad to let everything all rot on my hard drive, so I’m sharing a bunch of chaff for a tool called “Z3”, which has all sorts of uses in software research.
First an explanation of what this tool actually is, and then some scripts in order of increasing interestingness. All examples will use the Python bindings ( pip install z3-solver ).
What is Z3?
Z3 is an SMT solver.
Okay, what is SMT?
An SMT (“Satisfiability Modulo Theories”) solver is a constraint solver that understands math and basic programming concepts. You give it some variables, some equations with those variables, and it tries to find you a model , or set of assignments that satisfy all those equations.
Imagine you’re 12 years old and taking Algebra I for the first time, and see this problem:
4x + 2y == 14 2x - y == 1 solve for x & y
You’re supposed to learn how to do solve this as a system of equations, but if you want to cheat yourself out of an education you can have Z3 solve this for you.
# pip install z3-solver import z3 s = z3 . Solver() x, y = z3 . Ints( 'x y' ) s . add( 4 * x + 2 * y == 14 ) s . add( 2 * x - y == 1 ) result = s . check() print(result) if result == z3 . sat: print(s . model())
... continue reading