day 21 go+python solution

day21/sol.py

@@ -0,0 +1,26 @@
+
+
+import sys
+import z3
+
+x = z3.Int('x')
+def mul(a,b): return a*b
+def div(a,b):
+    quo = a / b
+    return z3.If(z3.Or(a % b == 0, a >= 0),
+                 quo,
+                 z3.If(b >= 0, quo + 1, quo - 1))
+def add(a,b): return a+b
+def sub(a,b): return a-b
+def num(a): return z3.IntVal(a)
+def eql(a,b): return a==b
+
+z = eval(open("expr.py").read())
+
+s = z3.Solver()
+s.add(z)
+print(s.check())
+
+m = s.model()
+print(m)
+