from z3 import *

foo = Bool('foo') # create variables named 'foo', 'bar', 'qax'
bar = Bool('bar')
qax = Bool('qax')

phi = Or(foo, And(bar, Xor(foo, Not(qax)), True), False)
print(phi) # Or(foo, And(bar, Xor(foo, Not(qax)), True), False)
psi = simplify(phi)
print(psi) # Or(foo, And(bar, foo == qax))

solver = Solver()
solver.add(psi) # assert that psi should be true
solver.add(Implies(foo, qax), Or(bar, foo)) # assert something else

print(solver) # [Or(foo, And(bar, foo == qax)), Implies(foo, qax), Or(bar, foo)]
result = solver.check() # check for satisfiability

if result == z3.sat:
  model = solver.model() # get valuation
  print(model[foo], model[bar], model[qax])# False True False