问题描述
重新激活 Z3 并行版本的当前计划是什么?
What are the current plans for reactivating the parallel version of Z3?
推荐答案
Z3 从来没有对并行性提供广泛的支持.在 2.x 版中，我们包含了一项实验性功能，允许用户使用不同的配置选项并行执行多个副本.不同的副本还可以共享信息并相互修剪搜索空间.此功能有一些限制.例如，它在程序化 API 中不可用.它也与长期的研究目标和方向相冲突.因此，此功能已从最近的版本中删除.
Z3 never had extensive support for parallelism. In version 2.x, we included an experimental feature that allowed users to execute several copies in parallel using different configuration options. The different copies could also share information and prune each other search space. This feature had some limitations. For example, it was not available in the programmatic API. It also conflicted with long term research goals and directions. Thus, this feature has been removed from recent versions.
话虽如此，在 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
That being said, in the Z3 4.x API, it is safe to create multiple contexts (Z3_Context) and access them concurrently from different threads. The previous versions were not thread safe. In Z3 4.x we can define custom strategies using parallel combinators. For example, the combinator (par-or t1 t2) executes the strategies t1 and t2 in parallel. These combinators are available in the programmatic API and SMT 2.0 front-end. The following online tutorial contains additional information: http://rise4fun.com/Z3/tutorial/strategies
以下命令(用于 SMT 2.0 前端)将使用具有不同随机种子的策略 smt 的两个副本检查断言的公式.
The following command (for the SMT 2.0 front-end) will check the asserted formulas using two copies of the tactic smt with different random seeds.
(check-sat-using (par-or (! smt :random-seed 10) (! smt :random-seed 20)))
这篇关于Z3并行版本什么时候重新激活?的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持！