If you need even more precision either tiled hexagon automata or subdivide into K instead of four compass orientations. There is also probably some Pressburger

If you need even more precision either tiled hexagon automata or subdivide into K instead of four compass orientations. There is also probably some Pressburger arithmetic formulation treating it as vectors in 2D you could whack with an SMT solver? I'd have to sleep on that. Might be easier to code than all the finite state automata merging.