hippos.py

from z3 import *
from itertools import combinations

s = Solver()


h1, h2, h3, h4, l, b1, b2 = Ints("h1 h2 h3 h4 l b1 b2")
hippos = [h1, h2, h3, h4]

for w in [223,235,248,272]:
    s.add(Or([ h1 + h2 == w for (h1, h2) in combinations(hippos, 2) ]))


s.add(Or([ l == h for h in hippos]))

s.add(Or([ b1 == h for h in hippos]))
s.add(Or([ b2 == h for h in hippos]))
s.add(b1 != b2)
s.add(b1 > b2)

s.add( l + b1 + b2 >= 400,
       l <= h1,
       l <= h2,
       l <= h3,
       l <= h4)



#s.add(l == 105)
print(s.check())
print(s.model())