将Z3与SBV并行使用 [英] Using Z3 with parallelization from SBV
问题描述
我想使用多核通过SBV使用Z3.基于此答案我应该能够通过传递 parallel.enable = true 到命令行上的 z3 可执行文件.由于我使用的是SBV，因此我需要通过SBV的界面来连接各种SMTLib求解器，因此，我尝试了以下方法:
I'd like to use Z3 via SBV using multiple cores. Based on this answer I should be able to do that just by passing parallel.enable=true to the z3 executable on the command line. Since I am using SBV, I need to go through SBV's interface to various SMTLib solvers, so here's what I tried:
foo = runSMTWith z3par $ do
...
where
z3par = z3
{ SBV.solver = (SBV.solver z3)
{ SBV.options = \cfg -> SBV.options (SBV.solver z3) cfg ++ ["parallel.enable=true"]
}
}
但是，我没有看到Z3在启用并行化的情况下运行的任何迹象:
However, I am not seeing any signs of Z3 running with parallelization enabled:
- CPU使用率没有超过一个内核
- 与没有此标志的运行相比，没有加速
通过SBV时如何启用Z3并行化?
How do I enable Z3 parallelization, when going via SBV?
推荐答案
实际上，您正在执行的操作是从SBV进行的操作.您可能要增加z3的详细程度，并将诊断输出到文件中以供以后检查.像这样:
What you're doing is essentially how it is done from SBV. You might want to increase verbosity of z3 and output the diagnostics to a file to inspect later. Something like:
import Data.SBV
import Data.SBV.Control
foo :: IO (Word64, Word64)
foo = runSMTWith z3{solver = par} $ do
x <- sWord64 "x"
y <- sWord64 "y"
setOption $ DiagnosticOutputChannel "diagnostic_output"
constrain $ x * y .== 13
constrain $ x .> 1
constrain $ y .> 1
query $ do ensureSat
(,) <$> getValue x <*> getValue y
where par = (solver z3) {options = \cfg -> options (solver z3) cfg ++ extras}
extras = [ "parallel.enable=true"
, "-v:3"
]
在这里，我们不仅要设置z3的并行模式，还要告诉它增加详细程度并将所有诊断信息存储在文件中.(注意:z3 config的并行部分中还有许多其他设置，您可以通过在命令行中发出 z3 -pd 并查看输出来查看它们的含义.您可以设置其他任何设置将参数添加到上面的 extras 变量中).
Here, we're not only setting z3's parallel-mode, but we're also telling it to increase verbosity and put all the diagnostics in a file. (Side note: There are many other settings in the parallel section of z3 config, you can see what they are by issuing z3 -pd in your command line and looking at the output. You can set any other parameters from there by adding it to the extras variable above.)
运行上面的命令时，我得到:
When I run the above, I get:
*Main> foo
(6379316565415788539,3774100875216427415)
但是我还得到了一个在当前目录中创建的名为 diagnostic_output 的文件，其中包括以下几行:
But I also get a file named diagnostic_output created in the current directory, which contains the following lines, amongst others:
(tactic.parallel :progress 0% :open 1)
(tactic.parallel :split-cube 0)
(parallel.tactic simplify-1)
(tactic.parallel :progress 100.00% :status sat :open 0)
因此z3确实处于并行模式，并且事情正在发生.当然，它的确切作用或多或少是一个黑匣子，并且如果不检查z3内部结构就无法解释上述输出.(我认为这些统计信息的含义或并行求解程序的策略都没有得到很好的记录.如果您找到了详细的详细记录，请报告！)
So z3 is indeed in the parallel mode and things are happening. Of course, what exactly it does is more or less a black-box, and it's impossible to interpret the above output without inspecting z3 internals. (I don't think the meaning of these stats nor the strategies for the parallel solver are that well documented. If you find a good documentation on the details, please do report!)
从提交开始，您现在可以简单地说:
As of this commit, you can now simply say:
runSMTWith z3{extraArgs = ["parallel.enable=true"]} $ do ...
进一步简化了编程.
请注意，SBV还具有组合器，可直接从Haskell同时运行事物.查看功能:
Note that SBV also has combinators for running things concurrently directly from Haskell. See the functions:
这些功能与求解器无关，您可以将它们与所选的任何求解器一起使用.当然，它们需要您重组问题并进行手动分解，以利用计算机中的多核功能，并自行将解决方案组合在一起.但是，它们也使您可以完全控制要如何构造昂贵的搜索.
These functions are solver agnostic, you can use them with any solver of your choosing. Of course, they require you to restructure your problem and do a manual decomposition to take advantage of the multiple-cores in your computer and stitch the solutions together yourself. But they also give you full control over how you want to structure your expensive search.
这篇关于将Z3与SBV并行使用的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！
