Add tiny little Z3 examples

README.md

@@ -11,6 +11,10 @@ Install our only Python dependency, [Lark][]:
 
     $ pip install --user lark-parser
 
+Witness the magic of Z3:
+
+    $ python3 ex0.py
+
 Run a simple example to see how to synthesize values, which is stolen from [Aws Albarghouthi][aws]'s [primer][]:
 
     $ python3 ex1.py

ex0.py

@@ -0,0 +1,24 @@
+import z3
+
+
+def ex0():
+    x = z3.Int('x')
+    print(solve(x / 7 == 6))
+
+    y = z3.BitVec('y', 8)
+    print(solve(y << 3 == 336))
+
+    z = z3.Int('z')
+    n = z3.Int('n')
+    print(solve(z3.ForAll([z], z * n == z)))
+
+
+def solve(phi):
+    s = z3.Solver()
+    s.add(phi)
+    s.check()
+    return s.model()
+
+
+if __name__ == '__main__':
+    ex0()