tweag / simple-smt

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

`Solver.Process`: set handle options #7

Closed qaristote closed 1 year ago

qaristote commented 1 year ago

The documentation for hPutBuilder says that the handle we use it on should be set to binary mode and use block buffering. This PR implements this for the Process backend, as SMTLib2 commands are sent using hPutBuffer on the process' input handle.

At the time of writing I only enabled binary mode on all of the process handles (not just the input handle). My understanding is that we're using ByeteStrings so character encoding and decoding isn't necessary, and binary mode is faster than text mode. I haven't set the buffering mode to block buffering though as I'm unsure of 1) what that means performance-wise, 2) what the default buffering mode of the handles created by createProcess are, and 3) whether line buffering may be more relevant here as we only read and write full lines anyways. Let me know if you know more about this ! (@facundominguez, any knowledge on that ?)

facundominguez commented 1 year ago

In the absence of calls to hFlush, line buffering causes every line to be sent individually to the external process, while block buffering would wait until the buffer fills. This code is calling hFlush though, so using block buffering might help reducing the overhead of the pipe.