34 lines
552 B
Python
34 lines
552 B
Python
|
#!/usr/bin/env python3
|
||
|
|
import json
|
||
|
|
from z3 import *
|
||
|
|
|
||
|
|
with open('circuit.json', 'r') as f:
|
||
|
|
j = json.load(f)
|
||
|
|
|
||
|
|
nq = j['memory']
|
||
|
|
|
||
|
|
system = [Bool(str(i)) for i in range(nq)]
|
||
|
|
|
||
|
|
s = Solver()
|
||
|
|
|
||
|
|
for cs in j['circuit']:
|
||
|
|
term = Or()
|
||
|
|
for c in cs:
|
||
|
|
term = Or(term, system[c[1]] == c[0])
|
||
|
|
s.add(term)
|
||
|
|
|
||
|
|
print(s)
|
||
|
|
print(s.check())
|
||
|
|
|
||
|
|
m = s.model()
|
||
|
|
|
||
|
|
result_arr = [''] * nq
|
||
|
|
|
||
|
|
for d in m.decls():
|
||
|
|
result_arr[int(d.name())] = '1' if m[d] else '0'
|
||
|
|
|
||
|
|
result_arr.reverse()
|
||
|
|
result = "".join(result_arr)
|
||
|
|
|
||
|
|
print(int.to_bytes(int(result, 2), nq//8, 'little'))
|