z3 - Z3并行版什么时候重新激活？

Question

已结束。 这个问题是 off-topic .它目前不接受答案。

---

想要改进这个问题？ Update the question所以它是on-topic堆栈溢出。

关闭 10 年前。

Improve this question

目前Z3并行版的重启计划是什么？

Answer 1

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)))