From 7ab06039aba68d8b3e5445692acd4f82fff707a7 Mon Sep 17 00:00:00 2001 From: Tomasz Kramkowski Date: Wed, 21 Dec 2022 13:03:08 +0000 Subject: 21 all-in-one --- 21.py | 8 ++++++-- 1 file changed, 6 insertions(+), 2 deletions(-) diff --git a/21.py b/21.py index a2c0365..d79cf0a 100644 --- a/21.py +++ b/21.py @@ -1,5 +1,6 @@ from functools import cache from utils import open_day +from subprocess import run, PIPE monkeys = {} with open_day(21) as f: @@ -26,7 +27,8 @@ def eval_monkey(m): print(eval_monkey('root')) -with open('21.z3', 'w') as f: +filename = '21.z3' +with open(filename, 'w') as f: f.write(''.join(f'(declare-const {monkey} Int)\n' for monkey in monkeys.keys())) for k, v in monkeys.items(): if k == 'humn': continue @@ -37,4 +39,6 @@ with open('21.z3', 'w') as f: print(f'(assert (= {k} {v}))', file=f) else: print(f'(assert (= {k} ({v[1]} {v[0]} {v[2]})))', file=f) - print('(check-sat)\n(get-model)', 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]) -- cgit v1.2.3-54-g00ecf