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)