2

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

谢谢。

4

1 回答 1

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 输入格式。

于 2011-09-29T21:51:23.573 回答