Z3 INI选项的详细文档

Question

是否有Z3的INI选项的任何详细文档。我必须做一个试验和错误的方法来找出QF_BV问题的最佳选择。我仍然不确定是否有更多的选项可以让我的z3跑得更快。如果有人能够指出对INI选项的任何现有的详细解释，那将是非常好的。

谢谢。

Answer 1

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

关于INI选项，其中有几个已被弃用，并且只存在，因为我们尚未完成向新方法的转换。 这些选项中有几个是为特定项目添加的，现在已经过时。它们只是为了向后兼容而存在。

关于QF_BV，Z3 3.2包含两个QF_BV求解器：旧的（来自2.x的）和新的。新的（官方）产品仅在Z3官方输入格式中可用：SMT 2.0。 SMT 1.0，简化和Z3低级输入格式已过时。 Z3 3.x的大部分性能改进仅在使用SMT 2.0输入格式时才可用。

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