add a Z3 backend, and more

[qaristote]

As explained in #22, I've been working on the possibility to use other backends (i.e. ways to interact with SMT solvers) than external processes, e.g. using Z3's C API. The point of this PR is not to be merged as is (unless you really like it), but to discuss what I've done and which features you would or would not be ready to merge. Here's a summary of the changes I made.

• The library is now split into several modules: SimpleSMT.SExpr deals with manipulating s-expressions; SimpleSMT.Solver implements the part of the interaction with SMT solvers that is common to all backends; and SimpleSMT.Solver.Process implements the part of the interaction with SMT solvers that is specific to communication using external processes.
• The commands are now sent to the solver as lazy bytestrings and are generated from s-expressions using bytestring builders (this is faster than using strings).
• It is now possible (but only optional) to send commands with no interesting output (i.e. producing only a (success)) lazily and by batches: they are written on a queue that is only flushed when the output is needed. This is faster because less calls are made to the solver, but currently this comes at the cost that these individual commands are not checked for correctness, i.e. we don't check that the solver answers (success) every time.
• I deleted the loadString function because it checks the commands are well-formed by parsing them and thus sends them one-by-one. The new sendSolver can be a faster but not as safe temporary replacement as it does not check that the commands are well-formed and thus sends them all in one go.
• I added a SimpleSMT.Solver.Z3 module that implements a backend using Z3's C API. As suggested, it comes in a separate package located in the Z3/ folder because it has a dependency on Z3.
• I rewrote the Process backend to use the more recent typed-process library, which takes care of releasing resources automatically. I also removed the Logger datatype as most of the logging can be done in the Solver module. The logging interface is not as expressive (I did not implement log levels) but this can easily be changed if needed.

I tried separating these changes into different commits but this is still a big PR so, again, its point is not to necessarily be merged. I could create separate PRs for the different changes you'd be interested in for instance. I also haven't tested this code at all although I'm reusing tested code I wrote for Pirouette. I'll be writing tests next.

At Tweag we'd be interested in using simple-smt in two projects, Pirouette and LiquidFixpoint, if communication is done using bytestrings and the Z3 backend is available. We should also be able to help maintain the library if needed.

[qaristote]

• I also added a basic test-suite for the library, which uncovered some bugs in readSExpr when parsing edge cases.

I think these are all the features I wanted to add to the library. Again the point of this PR is not the be merged as is but to discuss which of these features you'd be interested in.

In our internal discussions we also came to the conclusion that it might make more sense to just create a separate library for communicating with SMT solver backends (using bytestrings), without tying it to any particular way of manipulating s-expressions. So it's likely we'll just create such a library, and you can always plug it in simple-smt if you're still interested in having alternative backends.

[yav]

Hello,

thank you for all this work. It is quite hard to review such a big pull request, you've kind of just rewritten the library :) Nothing wrong with this, but it might be easier to discuss things if the PR was split into multiple smaller PRs, each with a specific topic. Alternatively, I'd just have to find a large enough chunk of time to see what's happening here.

As a general note, I am using this library on a number of projects, so we should consider backward compatibility at least somewhat.

Also, I am not sure what you are planning to do with SMT, but if you are interested in a slightly more full featured library, you may want to have a look at what4 (https://github.com/GaloisInc/what4).

I'll try to find time to look through the PR on the weekend though.

[qaristote]

Yeah this is a big PR, I got carried away, sorry about that ! But a big part of the diff is just splitting the main file into several files, so hopefully the pointers I gave above are enough to get the gist of the features. Feel free to take your time and ask questions, and thanks for giving this a look :) (and thanks for the link to what4, I'll give it a look !)

[qaristote]

In our internal discussions we also came to the conclusion that it might make more sense to just create a separate library for communicating with SMT solver backends (using bytestrings), without tying it to any particular way of manipulating s-expressions.

We ended up doing just that: the library is available here. I'll thus close this PR now, but feel free to take inspiration from it :)