adding solvers which provide bindings to parse SMTLib2

[qaristote]

In Z3's API there is a function Z3_eval_smtlib2_string which can be used to interact with Z3 using SMTLib2 commands. Using such a binding is noticeably faster than launching Z3 as an external process and communicating with it through pipes.

I'm thus considering extending simple-smt to support using specific solvers that have this kind of bindings in their API. I'm thinking of something like having a

class Solver a where
  init :: IO a
  command :: a -> SExpr -> IO SExpr
  stop :: a -> IO ExitCode

with a generic instance Solver ExternalProcess for running solvers as external processes and then some more specific ones such as instance Solver Z3 for using solvers through their SMTLib2-parsing bindings.

If I were to make such a PR here, would it be accepted and actively maintained in the future ? Or I am better off forking this project ?

[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.