用Z3实现SBV中的并行求解

Question

关于this answer，我尝试使用以下命令从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"运行它，并将bad.smt2提供给z3 (或您使用的任何求解器)，并在z3之外使用相同的参数，以查看是否存在其他错误/警告。