Process backend: add a function for sending (exit)

[qaristote]

Currently in Queuing mode there is no way to send an (exit) command to a Process backend, as it needs to actually be evaluated immediately but won't make the solver output anything. Using Bck.(send . backend) will thus leave the process hanging while waiting for a response that will never come.

This PR fixes this by adding an exit function in the Process module. It makes sense to keep this inside this module as this is something backend-specific: the (exit) command doesn't have any effect when using the Z3 backend. The implementation uses another function, write, which factors the instructions for writing onto the process' input channel.

I'm not sure whether it is best to keep this exit function on its own or to just merge it with the with function instead. They latter will always be used with the former anyways but it seems SMTLIB-based projects always separate these two functions.
Another thing I'm wondering is whether this function's name could be any better. It might get confusing for the user to have access to exit, wait and close.

[gabrielhdt]

Another thing I'm wondering is whether this function's name could be any better. It might get confusing for the user to have access to exit, wait and close.

I agree, are there cases where the distinction would be important? Does it make sense to exit and wait but you don't want to close the process? Can't you just provide the close function which sends exit and waits for the exit of the solver process? Which will by the way merge exit both with close and with.

My understanding is there are two ways to terminate a process: close and exit >> wait. If I'm correct, I'd say we choose one and name it close.

[qaristote]

I guess I don't see this library as a way of enforcing a good default way to use SMT solvers (here as external processes), but just making it easier to work with them, so it makes sense to provide both wait and close as you might want to ensure the process stops immediately or conversely make sure the solver finishes the evaluation of time-consuming SMTLIB commands before stopping.

So I'm thinking we can replace close with exit >> wait as this is better defaults anyways (it's thread-safer), but keep the old close around and rename it kill. If the user doesn't like that implementation of close, they can always use Process.process to directly manipulate the underlying process. Note that exit >> exit >> wait doesn't hang so it's fine if the user use the new implementation of close after sending an (exit) command themselves.

We can also expose the write function so that it's easier to send (exit) to the solver. Should we also expose the scanParen used to implement toBackend as a read function ?

[qaristote]

Also note that the new version of close (formerly wait) now ensures the process is killed even if there's an error while waiting for it to exit. This should solve #15 so I'll close that issue when we merge this.

[gabrielhdt]

I'm all for your proposition for close, exit &c., for the read thing, I'm just not knowledgeable enough yet. On the other hand, exporting write seems fair.

[facundominguez]

exit >> exit >> wait

Can't the writing to the handle fail in the second exit call if the process has terminated after the first exit call?

[facundominguez]

LGTM!

[gabrielhdt]

LGTM

[gabrielhdt]

Is it really a renaming though? Wouldn't that line be confusing, and make people sed s/wait/close/g, although it seems that they do not do the same operation?

[qaristote]

Is it better with 847f437 ?

[qaristote]

I'll merge this for now, and we can always improve the changelog when we release the next version :)

[qaristote]

Can't the writing to the handle fail in the second exit call if the process has terminated after the first exit call?

exit >> sleep 10 >> exit >> wait still works (with z3 at least). Of course exit >> wait >> exit wouldn't work, but that's probably too much too ask.