aoc21-24.py

from z3 import *

with open("input.txt") as f:
	lines = f.readlines()

iters = []

for i in range(14):
	base = i * 18
	print(lines[base + 4], lines[base + 5], lines[base + 15])
	values = [
		int(lines[base + 4].split(" ")[2]),
		int(lines[base + 5].split(" ")[2]),
		int(lines[base + 15].split(" ")[2]),
	]
	iters.append(values)

print(iters)

digits = [Int("d{}".format(i)) for i in range(14)]
inp_count = 0
z = 0

for a, b, c in iters:
	w = digits[inp_count]
	x = (z % 26) + b
	z /= a
	z = If(x != w, 26 * z + w + c, z)
	inp_count += 1

s = Solver()
for d in digits:
	s.add(d >= 1, d <= 9)
s.add(z == 0)
best = ""

while True:
	if s.check() != sat:
		break
	out = s.model()
	ans = ""
	for i in range(14):
		ans += str(out[digits[i]])
	best = ans
	print(best)
	s.add(sum([digits[i] * 10 ** (13 - i) for i in range(14)]) < int(ans))

print(best)