These notes are available at [tjcsec.club/pres](https://tjcsec.club/pres)! # Math is hard Math that is completed by hand is often prone to errors, and sometimes problems will be far too difficult to solve on paper. This is where [z3](https://github.com/Z3Prover/z3) comes in! z3 is a program developed by Microsoft which allows you to solve equations with integer answers. While the backend is written in C++, there are several bindings available, and the most convenient of these is the Python one, which I will cover here. ## Installation z3 can be installed via `pip install z3-solver`. **IMPORTANT NOTE:** The package found by using `pip install z3` is **NOT** the same thing, and will not help you solve equations. Be careful to install the right one! ## Usage The library is available to be imported using `import z3`. Variables can be declared using the syntax `some_var = z3.Int("name")`, with `Int` replaced with `Real`, `Bool`, etc. if necessary. Then, simple expressions can be solved by passing multiple constraints to `z3.solve`: ```python from z3 import * x = Int("x") y = Int("y") solve(x > 2, y < 10, x + 2*y == 7) ``` However, this can quickly become unwieldy when we have too many constraints. For larger problems, a `z3.Solver` object is usually better: ```python from z3 import * x, y, z = Ints('x y z') # shorthand for Int('x'), Int('y')... s = Solver() s.add(x+y==9) s.add(x-2==z) print(s.check()) # "sat" if there is a solution, "unsat" if none print(s.model()) # prints the actual answer ``` z3 can also do basic simplification of expressions through `z3.simplify`: ```python from z3 import * a = Bool("a") print(simplify(And(a, True))) ``` Some rev challenges will involve unsigned integer types with a fixed number of bits. These types wrap around after overflowing, so a normal `z3.Int` won't work. In this case, a `z3.BitVec` is better. This type will operate exactly the same as a C `int`, `long`, etc. if you choose the same number of bits. One key distinction is that a `z3.BitVec` uses signed operations by default, so if the challenge uses an unsigned number, you need to use the unsigned version. `a > b` turns into `UGT(a, b)`, where `UGT` stands for *U*nsigned *G*reater *T*han, and the same thing applies for `<`, `<=`, `>=`, `/`, `%` and `>>`. See [here](https://microsoft.github.io/z3guide/programming/Z3%20Python%20-%20Readonly/Introduction/#machine-arithmetic) for more information. ### Limitations z3 only works on polynomial expressions, so if you ask it to solve something like `2**x==4`, it will throw an error. Also, on numbers larger than 32 bits, it may take too long to solve non-trivial expressions to be useful. ### More information - [official z3 python docs](https://microsoft.github.io/z3guide/programming/Z3%20Python%20-%20Readonly/Introduction/) - [github page](https://github.com/Z3Prover/z3) Go work on today's challenges at [ctf.tjcsec.club](https://ctf.tjcsec.club)!