21 all-in-one

1 files 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])