Kimmy's "dress the man" puzzle

puzzle.jpg

solve_with_z3.py

from z3 import *

shoes = Int('shoes')
man = Int('man')
glasses = Int('glasses')
glove = Int('glove')

s = Solver()

s.add(3 * shoes == 60)
s.add(shoes + (2 * man) == 30)
s.add((2 * glasses) + man == 9)
s.add(shoes + glove + glasses == 42)

s.check()
m = s.model()

print(m)
shoes_result = m[shoes].as_long()
one_shoe = shoes_result / 2
glasses_result = m[glasses].as_long()
man_result = m[man].as_long()
glove_result = m[glove].as_long()

dressed_man = ( \
        (2 * one_shoe) +
        (2 * glove_result) +
        man_result + glasses_result \
    )
print('Dressed man is worth %d' % dressed_man)
result = one_shoe + dressed_man * glasses_result
print('? is %d' % result)

# output:
# [glove = 20, glasses = 2, man = 5, shoes = 20]
# Dressed man is worth 67
# ? is 144