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