Got a very minimal constraint solver working that translates S2 expressions directly to the SMT solver.