Solving/ruining the fun of a hard logic puzzle with Z3

logictest.py

from z3 import *
from typing import List

# Please use this responsibly and not in any remotely competitive environment
class LogicSolver:
    def __init__(self, comparables: List[int]):
        self.comparables = comparables
        self.vars = {}
        self.solver = Solver()
    
    def add_set(self, setVals: str):
        s = self.solver
        addedVals = []
        for val in setVals.split():
            z3obj = Int(val)
            addedVals.append(z3obj)
            self.vars[val] = z3obj
            #s.add(z3obj >= self.min, z3obj <= self.max)
            s.add(Or([z3obj == x for x in self.comparables])) # TODO: there has to be a better way
        s.add(Distinct(addedVals))
    
    def print_results(self):
        print(self.solver.check())
        print(self.solver.model())

# define possibilities
ls = LogicSolver([55, 60, 65, 70, 75, 80, 85])
ls.add_set('al betsy cora donna edwin faith gideon')
ls.add_set('m550 m775 m1250 m1500 m1825 m2000 m2500')
ls.add_set('anthon cromwell philo quasqueton springfield van zwingle')

# helper functions
s = ls.solver
def mixed_pairs(a, b, c, d):
    s.add(Or(And(a == c, b == d), And(a == d, b == c)))
def either_or(a, b, c):
    s.add(Or(a == b, a == c))

# define constraints
# evil global stuff!!!
globals().update(ls.vars)
# Of the tank bought by Donna Drake and the tank bought by Cora Carey,
# one is going to Zwingle and the other cost $2,000.
mixed_pairs(donna, cora, zwingle, m2000)
# Of the tank going to Anthon and the $550 display,
# one was bought by Faith Frisk and the other is 60 gallons.
mixed_pairs(anthon, m550, faith, 60)
# The $2,000 fish tank is somewhat larger than the tank bought by Faith Frisk.
s.add(m2000 > faith)
# The 85 gallon fish tank didn't cost $1,825.
s.add(85 != m1825)
# The fish tank going to Van Wert is somewhat larger than the display bought by Edwin Ellis.
s.add(van > edwin)
# The tank going to Van Wert is 5 gallons smaller than the $775 display.
s.add(van == m775 - 5)
# The seven tanks are the display going to Cromwell, the display bought by Donna Drake,
# the 55 gallon tank, the $1,500 display, the 70 gallon display, the 80 gallon tank and the 65 gallon tank.
s.add(Distinct(cromwell, donna, 55, m1500, 70, 80, 65))
# The display bought by Edwin Ellis isn't 55 gallons.
s.add(edwin != 55)
# The $2,500 display is either the fish tank going to Van Wert or the 80 gallon fish tank.
either_or(m2500, van, 80)
# The tank bought by Faith Frisk is somewhat larger than the display bought by Gideon Gates.
s.add(faith > gideon)
# The fish tank going to Zwingle is 10 gallons larger than the $775 fish tank.
s.add(zwingle == m775 + 10)
# The display bought by Al Ayala is 5 gallons smaller than the display bought by Donna Drake.
s.add(al == donna - 5)
# The $1,500 display is 5 gallons larger than the tank going to Quasqueton.
s.add(m1500 == quasqueton + 5)
# Of the $1,500 fish tank and the display bought by Donna Drake,
# one is going to Springfield and the other is 60 gallons.
mixed_pairs(m1500, donna, springfield, 60)

# go!
ls.print_results()