search

tweag / simple-smt

BSD 3-Clause "New" or "Revised" License
0 stars 0 forks source link

Get rid of the response buffer #2

Closed qaristote closed 1 year ago

qaristote commented 1 year ago

I implemented something similar to hGetContentsSizeHint in the Process backend so as to get rid of the response field in Solver.Backend.

I'm not sure of the implementation though, as there is still the problem of ensuring that the full output gets written before it starts being read. It should be ok if the solver always ends its output with an EOF and hGet waits for an EOF. But I'm not sure that hGet is the right function for this, I used it because I wanted to use something provided by the bytestring library.

qaristote commented 1 year ago

I also don't know if using a ByteString builder to concatenate lazy bytestrings is really useful.

qaristote commented 1 year ago

https://github.com/tweag/simple-smt/pull/2/commits/703bf75adaaa60477a95d6bc3f39d7b1e2d0a3ba should be doing the job (it handles every properly-formatted s-expression). I wonder if the parsing could be done more efficiently though, as in the end we're just reading a regular expression from a Handle. Perhaps we could use something like Rtlex ?