【发布时间】：2012-09-17 10:18:46
【问题描述】：
目前Z3并行版的重启计划是什么？
【问题讨论】：
标签： z3
【发布时间】：2012-09-17 10:18:46
【问题描述】：
Z3 从未广泛支持并行性。在 2.x 版本中，我们包含了一个实验性功能，允许用户使用不同的配置选项并行执行多个副本。不同的副本还可以共享信息并修剪彼此的搜索空间。此功能有一些限制。例如，它在程序化 API 中不可用。它也与长期的研究目标和方向相冲突。因此，此功能已从最新版本中删除。
话虽如此，在 Z3 4.x API 中，创建多个上下文 (Z3_Context) 并从不同线程同时访问它们是安全的。以前的版本不是线程安全的。在 Z3 4.x 中，我们可以使用并行组合器定义自定义策略。例如，组合器(par-or t1 t2) 并行执行策略t1 和t2。这些组合器可用于编程 API 和 SMT 2.0 前端。以下在线教程包含更多信息：http://rise4fun.com/Z3/tutorial/strategies
以下命令（用于 SMT 2.0 前端）将使用具有不同随机种子的策略 smt 的两个副本来检查断言的公式。
(check-sat-using (par-or (! smt :random-seed 10) (! smt :random-seed 20)))
【讨论】：
-
我们可以期待
par-or的加速吗？该策略是否在两个副本之间共享信息并修剪搜索空间？ -
有点晚了，但仍然：不，目前在 par-or 或 par-and 中没有共享。
-
并行化的分支是从z3中切断的吗？因为我发现了这个research.microsoft.com/en-us/um/people/leonardo/z3_doc/…