> Naively, the shift-based DFA requires 64-bit integers to encode the transitions, but I recently came across an idea from Dougall Johnson of using the Z3 SMT solver to pack the transitions into 32-bit integers [1]. That halves the size of the transition table for free. I adapted that effort to the existing conventions in v22 and arrived at the attached python script. > [...]
> I'll include something like the attached text file diff in the next patch. Some comments are now outdated, but this is good enough for demonstration.
Attached is v23 incorporating the 32-bit transition table, with the necessary comment adjustments.
