如何設置z3py中的核心數

Question

根據http://research.microsoft.com/en-us/um/people/leonardo/z3_doc/parallel.html我可以在z3命令行中設置CC_NUM_THREADS = 4，如果我使用的是.smt文件。

如果我使用z3py api，該怎麼做？

Answer 1

支持引理共享的投資組合解算器不是最新版Z3的一部分。因此這些參數不受支持，並且不支持允許每個參數具有多個值的參數格式（在命令行或通過python）。

也就是說，仍然有一種方法可以利用多個核心，這是一種par-or策略;例如參見Z3 Strategy Tutorial（搜索par-or）。該示例顯示瞭如何通過SMT2輸入語言並行運行多個策略（在本例中使用不同的隨機種子）;在z3py中，我們將使用ParOr function來創建這樣一個並行策略。