From 602c7298e3c462a32c1a782294d51a7d9a52823c Mon Sep 17 00:00:00 2001 From: Tomasz Kramkowski Date: Wed, 21 Dec 2022 14:16:01 +0000 Subject: 21 simplify z3 program --- 21.py | 21 +++++++++++---------- 1 file changed, 11 insertions(+), 10 deletions(-) diff --git a/21.py b/21.py index d79cf0a..aff0b84 100644 --- a/21.py +++ b/21.py @@ -27,18 +27,19 @@ def eval_monkey(m): 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: - f.write(''.join(f'(declare-const {monkey} Int)\n' for monkey in monkeys.keys())) - for k, v in monkeys.items(): - if k == 'humn': continue - if k == 'root': - print(f'(assert (= {v[0]} {v[2]}))', file=f) - continue - if isinstance(v, int): - print(f'(assert (= {k} {v}))', file=f) - else: - print(f'(assert (= {k} ({v[1]} {v[0]} {v[2]})))', file=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]) -- cgit v1.2.3-54-g00ecf