dfa_pack.py

from z3 import *

num_states = 9

# unique state->state transitions for all characters
transitions = [
 (0, 8, 8, 8, 8, 8, 8, 8, 8),
 (1, 8, 8, 8, 8, 8, 8, 8, 8),
 (2, 8, 8, 8, 8, 8, 8, 8, 8),
 (3, 8, 8, 8, 8, 8, 8, 8, 8),
 (4, 8, 8, 8, 8, 8, 8, 8, 8),
 (5, 8, 8, 8, 8, 8, 8, 8, 8),
 (6, 8, 8, 8, 8, 8, 8, 8, 8),
 (7, 8, 8, 8, 8, 8, 8, 8, 8),
 (8, 0, 1, 1, 8, 2, 2, 8, 8),
 (8, 0, 1, 8, 1, 2, 2, 8, 8),
 (8, 0, 1, 8, 1, 2, 8, 2, 8),
 (8, 8, 8, 8, 8, 8, 8, 8, 8)
]

s = Solver()

offsets = [BitVec('o%d' % i, 32) for i in range(num_states)]
values = [BitVec('v%d' % i, 32) for i in range(len(transitions))]

# these weren't necessary, but gave slightly nicer numbers
for v in values:
	s.add(v >> 30 == -1)
s.add(offsets[0] == 0)
s.add(offsets[8] == 31)

for i in range(len(offsets)):
	s.add(offsets[i] < 32)
	for j in range(i+1, len(offsets)):
		s.add(offsets[i] != offsets[j])

for vn, targets in enumerate(sorted(transitions)):
	for off, target in enumerate(targets):
		s.add(((values[vn] >> offsets[off]) & 31) == offsets[target])

print(s.check())

offsets = [s.model()[i].as_long() for i in offsets]
print('offsets:', offsets)

values = [s.model()[i].as_long() for i in values]

print('transitions:')
for t, v in zip(transitions, values):
	print(t, format(v, '032b'), hex(v))