haskell - 使用 Z3 在 SBV 中并行求解

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 推荐的是正确的方法。也就是说，使用 Haskell 之外的相同参数运行它transcript=Just "bad.smt2"并将其馈送bad.smt2到 z3（或您使用的任何求解器），以查看 z3 是否可能出现其他一些错误/警告。