3

目前Z3平行版重启的计划是什么?

4

1 回答 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 回答