i think you could fairly easily encode the layout/constraint solving portion of that as an SMT problem in nonlinear real arithmetic. which dReal should be able

i think you could fairly easily encode the layout/constraint solving portion of that as an SMT problem in nonlinear real arithmetic. which dReal should be able to solve https://dreal.github.io/ https://dreal.github.io/