Parallel solving in SBV with Z3

Question

参考这个答案，我正在尝试从SBV并行运行Z3:

runSMTWith z3{extraArgs = ["parallel.true"]} $ do ...

然而，上述情况导致以下异常：

*** Exception: 
*** Data.SBV: fd:21: hGetLine: end of file:
***
***    Sent      : (set-option :print-success true)
***
***    Executable: /usr/local/bin/z3
***    Options   : -nw -in -smt2
***
***    Hint      : Solver process prematurely ended communication.
***                It is likely it was terminated because of a seg-fault.
***                Run with 'transcript=Just "bad.smt2"' option, and feed
***                the generated "bad.smt2" file directly to the solver
***                outside of SBV for further information.

如果我去掉extraArgs并简单地使用默认的东西(即使使用runSMT(，计算也会非常好。

Answer 1

答案中有一个拼写错误。正确的调用是：

runSMTWith z3{extraArgs = ["parallel.enabled=true"]} $ do ..

试着这样做，看看效果是否更好。

请注意，要调试这类事情，SBV推荐的方法是正确的。也就是说，使用transcript=Just "bad.smt2"运行它，并使用Haskell之外的相同参数将bad.smt2馈送到z3(或您使用的任何解算器(，以查看z3是否会出现其他错误/警告。