【发布时间】：2011-09-29 16:30:40
【问题描述】：
有没有关于 Z3 的 INI 选项的详细文档。我不得不进行反复试验，以找出解决 QF_BV 问题的最佳选择。我仍然不确定是否有更多选项可以让我的 z3 运行得更快。如果有人能指出任何现有的 INI 选项详细说明，那就太好了。
谢谢。
【问题讨论】：
标签： z3
【发布时间】：2011-09-29 16:30:40
【问题描述】：
我们目前正在重组 Z3，并远离这种方法：具有“数千个”参数的求解器。 我们正在将 Z3 转变为一种更加模块化和灵活的方法，用于组合求解器和指定策略。 您可以在以下draft 中找到有关此新方法的更多信息。
关于 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 输入格式。
【讨论】：
-
关于你的句子“Z3 3.x 中的大部分性能改进只有在使用 SMT 2.0 输入格式时才可用。”：原生 C 接口的用户呢？
-
不幸的是，大多数改进尚不适用于本机 C 接口用户。我目前正在努力。我希望在几个月内准备好。