adding solvers which provide bindings to parse SMTLib2

[qaristote]

adding solvers which provide bindings to parse SMTLib2

[jwaldmann]

(not answering your question but) this sounds great! Do it, and I'm quite likely to use it. I find managing OS processes for solvers quite error-prone ( #21 )

You'll have to fork anyway, to submit the merge request?

I think the alternative is to make a fully separate package (simple-smt-z3). Probably this would still need some change in the base package. (your class Solver goes into simple-smt, and instances can be separate.)

The ersatz library (for SAT) has a similar approach. This is the interface description (just one method, so there's no class, and we pass the method directly) https://hackage.haskell.org/package/ersatz-0.4.12/docs/Ersatz-Solution.html#t:Solver and there are separate packages https://hackage.haskell.org/package/ersatz-toysat https://github.com/jwaldmann/ersatz-kissatapi https://github.com/jwaldmann/ersatz-minisatapi

The only downside is that such a version of simple-smt would no longer be "simple", then?

[yav]

Hi, there, thanks for the offer! I'd be open to such a pull request with the caveat that we should implement it in such a way that it can be disabled---more precisely, it's important to me that you can build simple-smt without having to build z3 also (or have it installed at all).

I quite like @jwaldmann's suggestion of packing this as a separate package that depends on simple-smt, and I'd be happy to make changes to simple-smt to accommodate a common interface.