pull_nested_quantifiers 选项是否适用于 Z3 中的简化？

Question

我想将公式中的所有嵌套量词拉到最外层。我希望以下命令可以在 Z3 中使用，但它们不能：

(set-option :pull-nested-quantifiers true)
(simplify (exists ((x Int)) (and (>= x 0) 
                            (forall ((y Int)) (and (>= y 1) (> x y))))))

:pull-nested-quantifiers 的目的是什么？如何使用 SMT-LIB 或 Z3 API 提取嵌套量词？

Answer 1

在 Z3 3.x 中，simplify 命令仅适用于通用本地简化步骤。 “拉嵌套量词”是一个预处理步骤。它将在未来版本中作为战术/策略提供。 Z3 3.2 在 SMT 2.0 前端已经有很多内置的策略/战术。下一个版本将有一套更大的战术。它们也将在 API 中可用。如果您在某些项目中需要此功能，只需给我发送电子邮件，我将为您制作一个非官方（测试版）版本。

最后，我们有了这个预处理步骤，因为如果通用量词没有嵌套（通用）量词，基于模型的量词实例化 MBQI 模块会更好地工作。您的示例没问题，因为 Z3 将消除存在并用新常量替换 x。