目前Z3平行版重启的计划是什么？
问问题
1522 次
1 回答
7
Z3 从未广泛支持并行性。在 2.x 版本中，我们包含了一项实验性功能，允许用户使用不同的配置选项并行执行多个副本。不同的副本还可以共享信息并修剪彼此的搜索空间。此功能有一些限制。例如，它在程序化 API 中不可用。它也与长期的研究目标和方向相冲突。因此，此功能已从最新版本中删除。
话虽如此，在 Z3 4.x API 中，创建多个上下文 (Z3_Context) 并从不同线程同时访问它们是安全的。以前的版本不是线程安全的。在 Z3 4.x 中，我们可以使用并行组合器定义自定义策略。例如，组合器并行(par-or t1 t2)执行策略。这些组合器可用于编程 API 和 SMT 2.0 前端。以下在线教程包含更多信息：http ://rise4fun.com/Z3/tutorial/strategiest1t2
以下命令（用于 SMT 2.0 前端）将使用smt具有不同随机种子的策略的两个副本来检查断言的公式。
(check-sat-using (par-or (! smt :random-seed 10) (! smt :random-seed 20)))
于 2012-09-17T14:24:23.463 回答