A dumb introduction to z3
Recently I have come across a nice article: Many Hard Leetcode Problems are Easy Constraint Problems, and I figured, I really should learn how to use these things! What else do I really have to do? I have had use for solvers (or as they are commonly called: theorem provers) In a previous article, but then I tried to prove the things with good old algorithms. I looked at z3 at the time, but found the whole concept a bit too opaque. Now however, it seemed a bit easier to get into. To be clear, as