【发布时间】：2021-10-03 19:09:21
【问题描述】：
我正在尝试改进 Z3 代码的时间。 我的环境Z3用的是Java，Z3的版本是4.8.10。
要在 C++ 中启用并行模式，您应该设置 set_param ("parallel.enable", true) ;。 在 Java 的情况下，如何将其设置为并行模式？ 如果您愿意，我想索取示例代码。
谢谢。
【问题讨论】：
标签： java parallel-processing z3 solver smt
【发布时间】：2021-10-03 19:09:21
【问题描述】：
Java 绑定中的相应调用称为setParameter。看这里：
https://z3prover.github.io/api/html/classcom_1_1microsoft_1_1z3_1_1_global.html#a38c6a465971f85a3c1826cf985ef3a56
【讨论】：
-
谢谢！换句话说，我应该使用 Global.setParameter("parallel.enable", "true");设置为并行模式？
-
这是一个很好的开始。我自己从未尝试过，所以当然可能还有其他问题。如果您发现问题，请报告。
-
嗨！我尝试了方法 Global.setParameter("parallel.enable", "true");但是，出现了以下警告。 WARNING: invalid parameter, unknown module 'parallel' 参数似乎不正确。
-
我刚刚尝试使用 Z3 版本 4.8.11，它工作正常。并行求解功能相当新，您可能需要升级您的 z3 版本。