We now use sympy in an offline setting to ensure correct CNF encodings of gates. There could be potential in merging many sequential gates before generating the CNF. Then we can let sympy spent some time on simplifying CNF expressions and we can reduce the number of time steps (see "large block encoding") potentially supporting longer circuits.
This could be a student assignment.