Here's a Python program that uses Z3 to find all the solutions to **Puzzle 128**:

from z3 import *
s = Solver()

# Define H(People) = {Alice, Bob, Tyler}
_, (Alice, Bob, Tyler) = H_People, People = EnumSort('H(People)', ('Alice', 'Bob', 'Tyler'))

# Define H(Friend)
H_Friend = Function('H(Friend)', H_People, H_People)
s.add(H_Friend(Alice) == Bob)
s.add(H_Friend(Bob) == Alice)
s.add(H_Friend(Tyler) == Bob)

# Define commutativity constraints on a_Friend
a_Friend = Function('a_Friend', H_People, H_People)
H_person = Const('H_person', H_People)
s.add(ForAll(H_person, H_Friend(a_Friend(H_person)) == a_Friend(H_Friend(H_person))))

# Print all satisfying models
while s.check() == sat:
m = s.model()
print(", ".join("{} -> {}".format(person, m.evaluate(a_Friend(person))) for person in People))
s.add(Exists(H_person, a_Friend(H_person) != m.evaluate(a_Friend(H_person))))

Output:

> Alice -> Alice, Bob -> Bob, Tyler -> Alice

> Alice -> Bob, Bob -> Alice, Tyler -> Bob

> Alice -> Alice, Bob -> Bob, Tyler -> Tyler

If for fun I define \\(H(Friend)\\) to be the identity function, this gives all \\(3^3 = 27\\) functions from \\(H(People)\\) to itself.