from z3 import *

A = DeclareSort('A') # new uninterpreted sort named 'A'
a = Const('a', A) # create constant of sort A
b = Const('b', A) # create another constant of sort A
f = Function('f', A, A) # create unary function of sort A -> A
g = Function('g', A, A, A) # create binary function of sort A x A -> A
p = Function('P', A, BoolSort()) # create unary predicate

s = Solver()
s.add(f(f(a)) == a, f(a) == b, a != b, g(a,b) == g(b,a))
s.add(p(a))

print(s.check()) # sat
m = s.model()
print("interpretation assigned to A:")
print(m[A]) # [A!val!0, A!val!1]
print("interpretations:")
print("f:", m[f]) # [A!val!0 -> A!val!1, A!val!1 -> A!val!0, ...]
print("a:", m[a]) # A!val!0
print("b:", m[b]) # A!val!1
print("p:", m[p])