Open jwaldmann opened 2 years ago
In a similar situation in a different project, I could realize the behaviour by switching from process
(what simple-smt uses) to typed-process
. This is even recommended at the top of https://hackage.haskell.org/package/process.
Snoyberg writes (at https://github.com/fpco/typed-process/#typed-process)
Use proper concurrency (e.g., the async library) in place of the weird lazy I/O tricks for such things as consuming output streams
simple-smt (as of now) needs lazy IO: it does hGetContents on the solver's full output stream, but that stream is built and consumed in many step of "send a command, check the response."
In my fork, I replaced lazy with a S-expression parser that directly works on the stream handle. Super ugly, but at least it makes it clear where an exception could happen (the handle vanishes)
There's a PR #13 that adds support for just killing a solver as opposed to issuing an exit
command. Would that help with your problem here?
Maybe.
You are right - I should state what I want more clearly:
there are (logically) two processes:
my specific problem is: when I kill B (control flow within my application raises AsyncCancelled in the thread) I also need to kill A (so, the exception must be caught, and handled)
I think that lazy IO (as currently used) makes this harder, but I am not really sure - I don't have a clear picture of what happens where and when. Where's a type (scoped effects) system when you need it? Also, I am not sure that the solution (the commit) that I linked above, does indeed work.
The situation is a bit different (and simpler) with SAT solvers in ersatz
, where all activity is behind solveWith s a
. But - this only works since there is actually no interaction (instead it's: 1. write formula, 2. call solver, 3. read result). For my current application, that would be enough for SMT as well. But I understand that there are applications that want to keep the solver running, and query/change its state.
I am starting two solvers concurrently. When one returns with a result, I want to kill the other. Ideally, the following should work
but it does not. yices finds a solution, the program stops, but cvc5 keeps running.