1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
|
from functools import cache
from utils import open_day
from subprocess import run, PIPE
monkeys = {}
with open_day(21) as f:
for line in f:
target, expr = line.rstrip().split(': ')
expr = expr.split(' ')
if len(expr) == 1:
expr = int(expr[0])
monkeys[target] = expr
ops = {
'+': lambda a, b: a + b,
'-': lambda a, b: a - b,
'*': lambda a, b: a * b,
'/': lambda a, b: a // b,
}
@cache
def eval_monkey(m):
expr = monkeys[m]
if isinstance(expr, int):
return expr
return ops[expr[1]](eval_monkey(expr[0]), eval_monkey(expr[2]))
print(eval_monkey('root'))
@cache
def to_sexp(m):
if m == 'humn': return m
expr = monkeys[m]
if isinstance(expr, int):
return str(expr)
return f'({expr[1]} {to_sexp(expr[0])} {to_sexp(expr[2])})'
filename = '21.z3'
with open(filename, 'w') as f:
print(f'(declare-const humn Int)', file=f)
root = monkeys['root']
print(f'(assert (= {to_sexp(root[0])} {to_sexp(root[2])}))', file=f)
print('(check-sat)\n(get-value (humn))', file=f)
r = run(['z3', filename], stdout=PIPE)
print(r.stdout.splitlines()[1].decode().strip('()').split()[1])
|
