z3 - Z3 INI 选项的详细文档

Question

有没有关于 Z3 的 INI 选项的详细文档。我必须进行反复试验，才能找出解决 QF_BV 问题的最佳选择。我仍然不确定是否有更多选项可以让我的 z3 运行得更快。如果有人可以指出任何现有的 INI 选项的详细说明，那就太好了。

谢谢。

Answer 1

我们目前正在重组 Z3，并远离这种方法：具有“数千个”参数的求解器。我们正在将 Z3 转变为一种更加模块化和灵活的方法，用于组合求解器和指定策略。您可以在以下草稿中找到有关此新方法的更多信息。

关于 INI 选项，其中一些已被弃用，仅在我们尚未完成向新方法的过渡时才存在。其中一些选项是为特定项目添加的，现在已经过时了。它们的存在只是为了向后兼容。

关于 QF_BV，Z3 3.2 包含两个 QF_BV 求解器：旧的（来自 2.x 的那个）和新的。新的（官方）只有Z3官方输入格式：SMT 2.0。SMT 1.0、Simplify 和 Z3 低级输入格式已过时。Z3 3.x 中的大多数性能改进仅在使用 SMT 2.0 输入格式时可用。

几个月后，Z3 将正式支持策略规范语言。我们将有一个教程和文档来描述如何使用它。同时，我强烈建议您对 QF_BV 等逻辑使用默认配置和 SMT 2.0 输入格式。