need a reliable way to kill a solver process

[jwaldmann]

I am starting two solvers concurrently. When one returns with a result, I want to kill the other. Ideally, the following should work

main = do
  as <- mapM async 
    [ main_with "yices-smt2" [ "--smt2-model-format" ]
    , main_with "cvc5" []
    ]
  (a,r) <- waitAnyCancel as
  print r

main_with :: String ->  [String] -> IO [(SExpr,Value)]
main_with solver opts = do
     l <- newLogger 0
     s <- newSolver solver opts (Just l)
     ...
     print =<< check s
     getExprs s [a,b,c,d]

but it does not. yices finds a solution, the program stops, but cvc5 keeps running.

[jwaldmann]

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)

[yav]

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?

[jwaldmann]

Maybe.

You are right - I should state what I want more clearly:

there are (logically) two processes:

• A: the solver (OS process)
• B: the haskell thread (in my application) that interacts with A

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.