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
Merge pull request #1 from mmjb/master

Refactoring/Cleanup of smt.ml