Factor out SMT file writing/solver calls

Refactor methods in smt.ml to build formulas internally, and then
calling a common file export interface, instead of directly writing
SMT files.

Also generlize the interface calling the actual solvers, and replace
copy&pasted code by higher-order methods
Build type annotations for nicer editing